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 = (/) \/ E.t((om ~<_ t /\ t (_ A) /\ f:(t X. t)-1-1-onto->t))}
infxpidmlem.2	|- A e. V

Assertion

Ref	Expression
infxpidmlem11	|- (((((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x) /\ (x ~~ y /\ y (_ (A \ x))) /\ u:((x X. y) u. ((y X. x) u. (y X. y)))-1-1-onto->y) -> E.h e. 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. u) -> (g (. h <-> g (. (g u. u)))
2	1	rcla4ev 1403	. . . . 5 |- (((g u. u) e. H /\ g (. (g u. u)) -> E.h e. H g (. h)
3		f1oun 2815	. . . . . . . . . . 11 |- (((g:(x X. x)-1-1-onto->x /\ u:((x X. y) u. ((y X. x) u. (y X. y)))-1-1-onto->y) /\ (((x X. x) i^i ((x X. y) u. ((y X. x) u. (y X. y)))) = (/) /\ (x i^i y) = (/))) -> (g u. u):((x X. x) u. ((x X. y) u. ((y X. x) u. (y X. y))))-1-1-onto->(x u. y))
4		xpdisj2 2654	. . . . . . . . . . . . . 14 |- ((x i^i y) = (/) -> ((x X. x) i^i (x X. y)) = (/))
5		xpdisj1 2653	. . . . . . . . . . . . . . . 16 |- ((x i^i y) = (/) -> ((x X. x) i^i (y X. x)) = (/))
6		xpdisj1 2653	. . . . . . . . . . . . . . . 16 |- ((x i^i y) = (/) -> ((x X. x) i^i (y X. y)) = (/))
7	5, 6	jca 236	. . . . . . . . . . . . . . 15 |- ((x i^i y) = (/) -> (((x X. x) i^i (y X. x)) = (/) /\ ((x X. x) i^i (y X. y)) = (/)))
8		undisj2 1740	. . . . . . . . . . . . . . 15 |- ((((x X. x) i^i (y X. x)) = (/) /\ ((x X. x) i^i (y X. y)) = (/)) <-> ((x X. x) i^i ((y X. x) u. (y X. y))) = (/))
9	7, 8	sylib 173	. . . . . . . . . . . . . 14 |- ((x i^i y) = (/) -> ((x X. x) i^i ((y X. x) u. (y X. y))) = (/))
10	4, 9	jca 236	. . . . . . . . . . . . 13 |- ((x i^i y) = (/) -> (((x X. x) i^i (x X. y)) = (/) /\ ((x X. x) i^i ((y X. x) u. (y X. y))) = (/)))
11		undisj2 1740	. . . . . . . . . . . . 13 |- ((((x X. x) i^i (x X. y)) = (/) /\ ((x X. x) i^i ((y X. x) u. (y X. y))) = (/)) <-> ((x X. x) i^i ((x X. y) u. ((y X. x) u. (y X. y)))) = (/))
12	10, 11	sylib 173	. . . . . . . . . . . 12 |- ((x i^i y) = (/) -> ((x X. x) i^i ((x X. y) u. ((y X. x) u. (y X. y)))) = (/))
13	12	ancri 245	. . . . . . . . . . 11 |- ((x i^i y) = (/) -> (((x X. x) i^i ((x X. y) u. ((y X. x) u. (y X. y)))) = (/) /\ (x i^i y) = (/)))
14	3, 13	sylan2 346	. . . . . . . . . 10 |- (((g:(x X. x)-1-1-onto->x /\ u:((x X. y) u. ((y X. x) u. (y X. y)))-1-1-onto->y) /\ (x i^i y) = (/)) -> (g u. u):((x X. x) u. ((x X. y) u. ((y X. x) u. (y X. y))))-1-1-onto->(x u. y))
15		xpun 2463	. . . . . . . . . . . 12 |- ((x u. y) X. (x u. y)) = (((x X. x) u. (x X. y)) u. ((y X. x) u. (y X. y)))
16		unass 1615	. . . . . . . . . . . 12 |- (((x X. x) u. (x X. y)) u. ((y X. x) u. (y X. y))) = ((x X. x) u. ((x X. y) u. ((y X. x) u. (y X. y))))
17	15, 16	eqtr 1119	. . . . . . . . . . 11 |- ((x u. y) X. (x u. y)) = ((x X. x) u. ((x X. y) u. ((y X. x) u. (y X. y))))
18		f1oeq2 2796	. . . . . . . . . . 11 |- (((x u. y) X. (x u. y)) = ((x X. x) u. ((x X. y) u. ((y X. x) u. (y X. y)))) -> ((g u. u):((x u. y) X. (x u. y))-1-1-onto->(x u. y) <-> (g u. u):((x X. x) u. ((x X. y) u. ((y X. x) u. (y X. y))))-1-1-onto->(x u. y)))
19	17, 18	ax-mp 6	. . . . . . . . . 10 |- ((g u. u):((x u. y) X. (x u. y))-1-1-onto->(x u. y) <-> (g u. u):((x X. x) u. ((x X. y) u. ((y X. x) u. (y X. y))))-1-1-onto->(x u. y))
20	14, 19	sylibr 175	. . . . . . . . 9 |- (((g:(x X. x)-1-1-onto->x /\ u:((x X. y) u. ((y X. x) u. (y X. y)))-1-1-onto->y) /\ (x i^i y) = (/)) -> (g u. u):((x u. y) X. (x u. y))-1-1-onto->(x u. y))
21		sslin 1662	. . . . . . . . . . 11 |- (y (_ (A \ x) -> (x i^i y) (_ (x i^i (A \ x)))
22		difdisj 1758	. . . . . . . . . . 11 |- (x i^i (A \ x)) = (/)
23	21, 22	syl6ss 1546	. . . . . . . . . 10 |- (y (_ (A \ x) -> (x i^i y) (_ (/))
24		ss0b 1726	. . . . . . . . . 10 |- ((x i^i y) (_ (/) <-> (x i^i y) = (/))
25	23, 24	sylib 173	. . . . . . . . 9 |- (y (_ (A \ x) -> (x i^i y) = (/))
26	20, 25	sylan2 346	. . . . . . . 8 |- (((g:(x X. x)-1-1-onto->x /\ u:((x X. y) u. ((y X. x) u. (y X. y)))-1-1-onto->y) /\ y (_ (A \ x)) -> (g u. u):((x u. y) X. (x u. y))-1-1-onto->(x u. y))
27	26	adantll 309	. . . . . . 7 |- ((((om ~<_ x /\ x (_ A) /\ (g:(x X. x)-1-1-onto->x /\ u:((x X. y) u. ((y X. x) u. (y X. y)))-1-1-onto->y)) /\ y (_ (A \ x)) -> (g u. u):((x u. y) X. (x u. y))-1-1-onto->(x u. y))
28		infxpidmlem.1	. . . . . . . . . . 11 |- H = {f | (f = (/) \/ E.t((om ~<_ t /\ t (_ A) /\ f:(t X. t)-1-1-onto->t))}
29		visset 1350	. . . . . . . . . . . 12 |- g e. V
30		visset 1350	. . . . . . . . . . . 12 |- u e. V
31	29, 30	unex 1949	. . . . . . . . . . 11 |- (g u. u) e. V
32		visset 1350	. . . . . . . . . . . 12 |- x e. V
33		visset 1350	. . . . . . . . . . . 12 |- y e. V
34	32, 33	unex 1949	. . . . . . . . . . 11 |- (x u. y) e. V
35	28, 31, 34	infxpidmlem3 4935	. . . . . . . . . 10 |- (((om ~<_ (x u. y) /\ (x u. y) (_ A) /\ (g u. u):((x u. y) X. (x u. y))-1-1-onto->(x u. y)) -> (g u. u) e. H)
36		ssun1 1621	. . . . . . . . . . . . . 14 |- x (_ (x u. y)
37		ssdomg 3311	. . . . . . . . . . . . . 14 |- (x e. V -> (x (_ (x u. y) -> x ~<_ (x u. y)))
38	32, 36, 37	mp2 43	. . . . . . . . . . . . 13 |- x ~<_ (x u. y)
39		domtr 3320	. . . . . . . . . . . . 13 |- ((om ~<_ x /\ x ~<_ (x u. y)) -> om ~<_ (x u. y))
40	38, 39	mpan2 519	. . . . . . . . . . . 12 |- (om ~<_ x -> om ~<_ (x u. 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 u. y) (_ A)
46	44, 45	sylib 173	. . . . . . . . . . . 12 |- ((x (_ A /\ y (_ (A \ x)) -> (x u. y) (_ A)
47	40, 46	anim12i 268	. . . . . . . . . . 11 |- ((om ~<_ x /\ (x (_ A /\ y (_ (A \ x))) -> (om ~<_ (x u. y) /\ (x u. y) (_ A))
48	47	anassrs 338	. . . . . . . . . 10 |- (((om ~<_ x /\ x (_ A) /\ y (_ (A \ x)) -> (om ~<_ (x u. y) /\ (x u. y) (_ A))
49	35, 48	sylan 343	. . . . . . . . 9 |- ((((om ~<_ x /\ x (_ A) /\ y (_ (A \ x)) /\ (g u. u):((x u. y) X. (x u. y))-1-1-onto->(x u. y)) -> (g u. u) e. H)
50	49	exp 291	. . . . . . . 8 |- (((om ~<_ x /\ x (_ A) /\ y (_ (A \ x)) -> ((g u. u):((x u. y) X. (x u. y))-1-1-onto->(x u. y) -> (g u. u) e. H))
51	50	adantlr 310	. . . . . . 7 |- ((((om ~<_ x /\ x (_ A) /\ (g:(x X. x)-1-1-onto->x /\ u:((x X. y) u. ((y X. x) u. (y X. y)))-1-1-onto->y)) /\ y (_ (A \ x)) ->