Theorem infxpidmlem11 4943

Description: Lemma for infxpidm 4945. We show that the union of a bijection g in H with a disjoint bijection u is a member h of H that is larger than (properly extends) g. Thus if the antecedent is true then g cannot be maximal.

Hypotheses

Ref	Expression
infxpidmlem.1	⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))}
infxpidmlem.2	⊢ A ∈ V

Assertion

Ref	Expression
infxpidmlem11	⊢ (((((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) ∧ (x ≈ y ∧ y ⊆ (A ∖ x))) ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) → ∃h ∈ H g ⊂ h)

Distinct variable group(s):   x,y,f,g,h,u,t,A   x,H,y,u,g,h

Proof of Theorem infxpidmlem11

Step	Hyp	Ref	Expression
1		psseq2 1560	. . . . . 6 ⊢ (h = (g ∪ u) → (g ⊂ h ↔ g ⊂ (g ∪ u)))
2	1	rcla4ev 1403	. . . . 5 ⊢ (((g ∪ u) ∈ H ∧ g ⊂ (g ∪ u)) → ∃h ∈ H g ⊂ h)
3		f1oun 2815	. . . . . . . . . . 11 ⊢ (((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) ∧ (((x × x) ∩ ((x × y) ∪ ((y × x) ∪ (y × y)))) = ∅ ∧ (x ∩ y) = ∅)) → (g ∪ u):((x × x) ∪ ((x × y) ∪ ((y × x) ∪ (y × y))))–1-1-onto→(x ∪ y))
4		xpdisj2 2654	. . . . . . . . . . . . . 14 ⊢ ((x ∩ y) = ∅ → ((x × x) ∩ (x × y)) = ∅)
5		xpdisj1 2653	. . . . . . . . . . . . . . . 16 ⊢ ((x ∩ y) = ∅ → ((x × x) ∩ (y × x)) = ∅)
6		xpdisj1 2653	. . . . . . . . . . . . . . . 16 ⊢ ((x ∩ y) = ∅ → ((x × x) ∩ (y × y)) = ∅)
7	5, 6	jca 236	. . . . . . . . . . . . . . 15 ⊢ ((x ∩ y) = ∅ → (((x × x) ∩ (y × x)) = ∅ ∧ ((x × x) ∩ (y × y)) = ∅))
8		undisj2 1740	. . . . . . . . . . . . . . 15 ⊢ ((((x × x) ∩ (y × x)) = ∅ ∧ ((x × x) ∩ (y × y)) = ∅) ↔ ((x × x) ∩ ((y × x) ∪ (y × y))) = ∅)
9	7, 8	sylib 173	. . . . . . . . . . . . . 14 ⊢ ((x ∩ y) = ∅ → ((x × x) ∩ ((y × x) ∪ (y × y))) = ∅)
10	4, 9	jca 236	. . . . . . . . . . . . 13 ⊢ ((x ∩ y) = ∅ → (((x × x) ∩ (x × y)) = ∅ ∧ ((x × x) ∩ ((y × x) ∪ (y × y))) = ∅))
11		undisj2 1740	. . . . . . . . . . . . 13 ⊢ ((((x × x) ∩ (x × y)) = ∅ ∧ ((x × x) ∩ ((y × x) ∪ (y × y))) = ∅) ↔ ((x × x) ∩ ((x × y) ∪ ((y × x) ∪ (y × y)))) = ∅)
12	10, 11	sylib 173	. . . . . . . . . . . 12 ⊢ ((x ∩ y) = ∅ → ((x × x) ∩ ((x × y) ∪ ((y × x) ∪ (y × y)))) = ∅)
13	12	ancri 245	. . . . . . . . . . 11 ⊢ ((x ∩ y) = ∅ → (((x × x) ∩ ((x × y) ∪ ((y × x) ∪ (y × y)))) = ∅ ∧ (x ∩ y) = ∅))
14	3, 13	sylan2 346	. . . . . . . . . 10 ⊢ (((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) ∧ (x ∩ y) = ∅) → (g ∪ u):((x × x) ∪ ((x × y) ∪ ((y × x) ∪ (y × y))))–1-1-onto→(x ∪ y))
15		xpun 2463	. . . . . . . . . . . 12 ⊢ ((x ∪ y) × (x ∪ y)) = (((x × x) ∪ (x × y)) ∪ ((y × x) ∪ (y × y)))
16		unass 1615	. . . . . . . . . . . 12 ⊢ (((x × x) ∪ (x × y)) ∪ ((y × x) ∪ (y × y))) = ((x × x) ∪ ((x × y) ∪ ((y × x) ∪ (y × y))))
17	15, 16	eqtr 1119	. . . . . . . . . . 11 ⊢ ((x ∪ y) × (x ∪ y)) = ((x × x) ∪ ((x × y) ∪ ((y × x) ∪ (y × y))))
18		f1oeq2 2796	. . . . . . . . . . 11 ⊢ (((x ∪ y) × (x ∪ y)) = ((x × x) ∪ ((x × y) ∪ ((y × x) ∪ (y × y)))) → ((g ∪ u):((x ∪ y) × (x ∪ y))–1-1-onto→(x ∪ y) ↔ (g ∪ u):((x × x) ∪ ((x × y) ∪ ((y × x) ∪ (y × y))))–1-1-onto→(x ∪ y)))
19	17, 18	ax-mp 6	. . . . . . . . . 10 ⊢ ((g ∪ u):((x ∪ y) × (x ∪ y))–1-1-onto→(x ∪ y) ↔ (g ∪ u):((x × x) ∪ ((x × y) ∪ ((y × x) ∪ (y × y))))–1-1-onto→(x ∪ y))
20	14, 19	sylibr 175	. . . . . . . . 9 ⊢ (((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) ∧ (x ∩ y) = ∅) → (g ∪ u):((x ∪ y) × (x ∪ y))–1-1-onto→(x ∪ y))
21		sslin 1662	. . . . . . . . . . 11 ⊢ (y ⊆ (A ∖ x) → (x ∩ y) ⊆ (x ∩ (A ∖ x)))
22		difdisj 1758	. . . . . . . . . . 11 ⊢ (x ∩ (A ∖ x)) = ∅
23	21, 22	syl6ss 1546	. . . . . . . . . 10 ⊢ (y ⊆ (A ∖ x) → (x ∩ y) ⊆ ∅)
24		ss0b 1726	. . . . . . . . . 10 ⊢ ((x ∩ y) ⊆ ∅ ↔ (x ∩ y) = ∅)
25	23, 24	sylib 173	. . . . . . . . 9 ⊢ (y ⊆ (A ∖ x) → (x ∩ y) = ∅)
26	20, 25	sylan2 346	. . . . . . . 8 ⊢ (((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) ∧ y ⊆ (A ∖ x)) → (g ∪ u):((x ∪ y) × (x ∪ y))–1-1-onto→(x ∪ y))
27	26	adantll 309	. . . . . . 7 ⊢ ((((ω ≼ x ∧ x ⊆ A) ∧ (g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y)) ∧ y ⊆ (A ∖ x)) → (g ∪ u):((x ∪ y) × (x ∪ y))–1-1-onto→(x ∪ y))
28		infxpidmlem.1	. . . . . . . . . . 11 ⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))}
29		visset 1350	. . . . . . . . . . . 12 ⊢ g ∈ V
30		visset 1350	. . . . . . . . . . . 12 ⊢ u ∈ V
31	29, 30	unex 1949	. . . . . . . . . . 11 ⊢ (g ∪ u) ∈ V
32		visset 1350	. . . . . . . . . . . 12 ⊢ x ∈ V
33		visset 1350	. . . . . . . . . . . 12 ⊢ y ∈ V
34	32, 33	unex 1949	. . . . . . . . . . 11 ⊢ (x ∪ y) ∈ V
35	28, 31, 34	infxpidmlem3 4935	. . . . . . . . . 10 ⊢ (((ω ≼ (x ∪ y) ∧ (x ∪ y) ⊆ A) ∧ (g ∪ u):((x ∪ y) × (x ∪ y))–1-1-onto→(x ∪ y)) → (g ∪ u) ∈ H)
36		ssun1 1621	. . . . . . . . . . . . . 14 ⊢ x ⊆ (x ∪ y)
37		ssdomg 3311	. . . . . . . . . . . . . 14 ⊢ (x ∈ V → (x ⊆ (x ∪ y) → x ≼ (x ∪ y)))
38	32, 36, 37	mp2 43	. . . . . . . . . . . . 13 ⊢ x ≼ (x ∪ y)
39		domtr 3320	. . . . . . . . . . . . 13 ⊢ ((ω ≼ x ∧ x ≼ (x ∪ y)) → ω ≼ (x ∪ y))
40	38, 39	mpan2 519	. . . . . . . . . . . 12 ⊢ (ω ≼ x → ω ≼ (x ∪ y))
41		difss 1596	. . . . . . . . . . . . . . 15 ⊢ (A ∖ x) ⊆ A
42		sstr 1511	. . . . . . . . . . . . . . 15 ⊢ ((y ⊆ (A ∖ x) ∧ (A ∖ x) ⊆ A) → y ⊆ A)
43	41, 42	mpan2 519	. . . . . . . . . . . . . 14 ⊢ (y ⊆ (A ∖ x) → y ⊆ A)
44	43	anim2i 270	. . . . . . . . . . . . 13 ⊢ ((x ⊆ A ∧ y ⊆ (A ∖ x)) → (x ⊆ A ∧ y ⊆ A))
45		unss 1632	. . . . . . . . . . . . 13 ⊢ ((x ⊆ A ∧ y ⊆ A) ↔ (x ∪ y) ⊆ A)
46	44, 45	sylib 173	. . . . . . . . . . . 12 ⊢ ((x ⊆ A ∧ y ⊆ (A ∖ x)) → (x ∪ y) ⊆ A)
47	40, 46	anim12i 268	. . . . . . . . . . 11 ⊢ ((ω ≼ x ∧ (x ⊆ A ∧ y ⊆ (A ∖ x))) → (ω ≼ (x ∪ y) ∧ (x ∪ y) ⊆ A))
48	47	anassrs 338	. . . . . . . . . 10 ⊢ (((ω ≼ x ∧ x ⊆ A) ∧ y ⊆ (A ∖ x)) → (ω ≼ (x ∪ y) ∧ (x ∪ y) ⊆ A))
49	35, 48	sylan 343	. . . . . . . . 9 ⊢ ((((ω ≼ x ∧ x ⊆ A) ∧ y ⊆ (A ∖ x)) ∧ (g ∪ u):((x ∪ y) × (x ∪ y))–1-1-onto→(x ∪ y)) → (g ∪ u) ∈ H)
50	49	exp 291	. . . . . . . 8 ⊢ (((ω ≼ x ∧ x ⊆ A) ∧ y ⊆ (A ∖ x)) → ((g ∪ u):((x ∪ y) × (x ∪ y))–1-1-onto→(x ∪ y) → (g ∪ u) ∈ H))
51	50	adantlr 310	. . . . . . 7 ⊢ ((((ω ≼ x ∧ x ⊆ A) ∧ (g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y)) ∧ y ⊆ (A ∖ x)) → ((g ∪ u):((x ∪ y) × (x ∪ y))–1-1-onto→(x ∪ y) → (g ∪ u) ∈ H))
52	27, 51	mpd 46	. . . . . 6 ⊢ ((((ω ≼ x ∧ x ⊆ A) ∧ (g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y)) ∧ y ⊆ (A ∖ x)) → (g ∪ u) ∈ H)
53	52	adantrl 311	. . . . 5 ⊢ ((((ω ≼ x ∧ x ⊆ A) ∧ (g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y)) ∧ (x ≈ y ∧ y ⊆ (A ∖ x))) → (g ∪ u) ∈ H)
54		disjpss 1738	. . . . . . . . . . . 12 ⊢ (((g ∩ u) = ∅ ∧ ¬ u = ∅) → g ⊂ (g ∪ u))
55		ineq12 1640	. . . . . . . . . . . . . . . . 17 ⊢ ((ran g = x ∧ ran u = y) → (ran g ∩ ran u) = (x ∩ y))
56	55	cleq1d 1109	. . . . . . . . . . . . . . . 16 ⊢ ((ran g = x ∧ ran u = y) → ((ran g ∩ ran u) = ∅ ↔ (x ∩ y) = ∅))
57		f1ofo 2806	. . . . . . . . . . . . . . . . 17 ⊢ (g:(x × x)–1-1-onto→x → g:(x × x)–onto→x)
58		forn 2789	. . . . . . . . . . . . . . . . 17 ⊢ (g:(x × x)–onto→x → ran g = x)
59	57, 58	syl 12	. . . . . . . . . . . . . . . 16 ⊢ (g:(x × x)–1-1-onto→x → ran g = x)
60		f1ofo 2806	. . . . . . . . . . . . . . . . 17 ⊢ (u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y → u:((x × y) ∪ ((y × x) ∪ (y × y)))–onto→y)
61		forn 2789	. . . . . . . . . . . . . . . . 17 ⊢ (u:((x × y) ∪ ((y × x) ∪ (y × y)))–onto→y → ran u = y)
62	60, 61	syl 12	. . . . . . . . . . . . . . . 16 ⊢ (u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y → ran u = y)
63	56, 59, 62	syl2an 349	. . . . . . . . . . . . . . 15 ⊢ ((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) → ((ran g ∩ ran u) = ∅ ↔ (x ∩ y) = ∅))
64		f1orel 2803	. . . . . . . . . . . . . . . . 17 ⊢ (g:(x × x)–1-1-onto→x → Rel g)
65		relin 2491	. . . . . . . . . . . . . . . . 17 ⊢ (Rel g → Rel (g ∩ u))
66		relrn0 2568	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel (g ∩ u) → ((g ∩ u) = ∅ ↔ ran (g ∩ u) = ∅))
67		rnin 2645	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran (g ∩ u) ⊆ (ran g ∩ ran u)
68		sseq2 1522	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ran g ∩ ran u) = ∅ → (ran (g ∩ u) ⊆ (ran g ∩ ran u) ↔ ran (g ∩ u) ⊆ ∅))
69	67, 68	mpbii 168	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ran g ∩ ran u) = ∅ → ran (g ∩ u) ⊆ ∅)
70		ss0 1727	. . . . . . . . . . . . . . . . . . 19 ⊢ (ran (g ∩ u) ⊆ ∅ → ran (g ∩ u) = ∅)
71	69, 70	syl 12	. . . . . . . . . . . . . . . . . 18 ⊢ ((ran g ∩ ran u) = ∅ → ran (g ∩ u) = ∅)
72	66, 71	syl5bir 184	. . . . . . . . . . . . . . . . 17 ⊢ (Rel (g ∩ u) → ((ran g ∩ ran u) = ∅ → (g ∩ u) = ∅))
73	64, 65, 72	3syl 21	. . . . . . . . . . . . . . . 16 ⊢ (g:(x × x)–1-1-onto→x → ((ran g ∩ ran u) = ∅ → (g ∩ u) = ∅))
74	73	adantr 306	. . . . . . . . . . . . . . 15 ⊢ ((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) → ((ran g ∩ ran u) = ∅ → (g ∩ u) = ∅))
75	63, 74	sylbird 180	. . . . . . . . . . . . . 14 ⊢ ((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) → ((x ∩ y) = ∅ → (g ∩ u) = ∅))
76	75	imp 277	. . . . . . . . . . . . 13 ⊢ (((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) ∧ (x ∩ y) = ∅) → (g ∩ u) = ∅)
77	76	adantr 306	. . . . . . . . . . . 12 ⊢ ((((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) ∧ (x ∩ y) = ∅) ∧ (ω ≼ x ∧ x ≈ y)) → (g ∩ u) = ∅)
78		f1orel 2803	. . . . . . . . . . . . . . . . . . . 20 ⊢ (u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y → Rel u)
79		relrn0 2568	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Rel u → (u = ∅ ↔ ran u = ∅))
80	78, 79	syl 12	. . . . . . . . . . . . . . . . . . 19 ⊢ (u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y → (u = ∅ ↔ ran u = ∅))
81	62	cleq1d 1109	. . . . . . . . . . . . . . . . . . 19 ⊢ (u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y → (ran u = ∅ ↔ y = ∅))
82	80, 81	bitrd 406	. . . . . . . . . . . . . . . . . 18 ⊢ (u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y → (u = ∅ ↔ y = ∅))
83	82	negbid 463	. . . . . . . . . . . . . . . . 17 ⊢ (u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y → (¬ u = ∅ ↔ ¬ y = ∅))
84	33	infn0 3427	. . . . . . . . . . . . . . . . 17 ⊢ (ω ≼ y → ¬ y = ∅)
85	83, 84	syl5bir 184	. . . . . . . . . . . . . . . 16 ⊢ (u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y → (ω ≼ y → ¬ u = ∅))
86		domentr 3326	. . . . . . . . . . . . . . . 16 ⊢ ((ω ≼ x ∧ x ≈ y) → ω ≼ y)
87	85, 86	syl5 22	. . . . . . . . . . . . . . 15 ⊢ (u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y → ((ω ≼ x ∧ x ≈ y) → ¬ u = ∅))
88	87	imp 277	. . . . . . . . . . . . . 14 ⊢ ((u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y ∧ (ω ≼ x ∧ x ≈ y)) → ¬ u = ∅)
89	88	adantll 309	. . . . . . . . . . . . 13 ⊢ (((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) ∧ (ω ≼ x ∧ x ≈ y)) → ¬ u = ∅)
90	89	adantlr 310	. . . . . . . . . . . 12 ⊢ ((((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) ∧ (x ∩ y) = ∅) ∧ (ω ≼ x ∧ x ≈ y)) → ¬ u = ∅)
91	54, 77, 90	sylanc 361	. . . . . . . . . . 11 ⊢ ((((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) ∧ (x ∩ y) = ∅) ∧ (ω ≼ x ∧ x ≈ y)) → g ⊂ (g ∪ u))
92	91	exp43 301	. . . . . . . . . 10 ⊢ ((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) → ((x ∩ y) = ∅ → (ω ≼ x → (x ≈ y → g ⊂ (g ∪ u)))))
93	92, 25	syl5 22	. . . . . . . . 9 ⊢ ((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) → (y ⊆ (A ∖ x) → (ω ≼ x → (x ≈ y → g ⊂ (g ∪ u)))))
94	93	com4t 40	. . . . . . . 8 ⊢ (ω ≼ x → (x ≈ y → ((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) → (y ⊆ (A ∖ x) → g ⊂ (g ∪ u)))))
95	94	com23 32	. . . . . . 7 ⊢ (ω ≼ x → ((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) → (x ≈ y → (y ⊆ (A ∖ x) → g ⊂ (g ∪ u)))))
96	95	adantr 306	. . . . . 6 ⊢ ((ω ≼ x ∧ x ⊆ A) → ((g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) → (x ≈ y → (y ⊆ (A ∖ x) → g ⊂ (g ∪ u)))))
97	96	imp43 288	. . . . 5 ⊢ ((((ω ≼ x ∧ x ⊆ A) ∧ (g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y)) ∧ (x ≈ y ∧ y ⊆ (A ∖ x))) → g ⊂ (g ∪ u))
98	2, 53, 97	sylanc 361	. . . 4 ⊢ ((((ω ≼ x ∧ x ⊆ A) ∧ (g:(x × x)–1-1-onto→x ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y)) ∧ (x ≈ y ∧ y ⊆ (A ∖ x))) → ∃h ∈ H g ⊂ h)
99	98	exp42 300	. . 3 ⊢ ((ω ≼ x ∧ x ⊆ A) → (g:(x × x)–1-1-onto→x → (u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y → ((x ≈ y ∧ y ⊆ (A ∖ x)) → ∃h ∈ H g ⊂ h))))
100	99	com34 36	. 2 ⊢ ((ω ≼ x ∧ x ⊆ A) → (g:(x × x)–1-1-onto→x → ((x ≈ y ∧ y ⊆ (A ∖ x)) → (u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y → ∃h ∈ H g ⊂ h))))
101	100	imp41 286	1 ⊢ (((((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) ∧ (x ≈ y ∧ y ⊆ (A ∖ x))) ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) → ∃h ∈ H g ⊂ h)

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∨ wo 195   ∧ wa 196  ∃wex 678  {cab 1090   = wceq 1091   ∈ wcel 1092  ∃wrex 1202  Vcvv 1348   ∖ cdif 1484   ∪ cun 1485   ∩ cin 1486   ⊆ wss 1487   ⊂ wpss 1488  ∅c0 1707   class class class wbr 2054  ωcom 2372   × cxp 2408  ran crn 2411  Rel wrel 2415  –onto→wfo 2420  –1-1-onto→wf1o 2421   ≈ cen 3271   ≼ cdom 3272

This theorem is referenced by:  infxpidmlem12 4944

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-er 3200  df-en 3274  df-dom 3275  df-sdom 3276

metamath.org