Theorem infxpidmlem12 7506

Description: Lemma for infxpidm 7507. Letting x be the range of a maximal bijection g in H, infxpidmlem11 7505 lets us show that assuming x ~<_ (A \ x) leads to the contradiction E.h e. Hg (. h meaning g is not maximal. Thus (A \ x) ~< x. This allows us to show that x is as big as A. Since x is idempotent, and g exists by Zorn's Lemma in infxpidmlem9 7503, A is also idempotent.

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
infxpidmlem12	|- (om ~<_ A -> (A X. A) ~~ A)

Distinct variable group:   t,f,A

Proof of Theorem infxpidmlem12

Step	Hyp	Ref	Expression
1		infxpidmlem.1	. . 3 |- H = {f | (f = (/) \/ E.t((om ~<_ t /\ t (_ A) /\ f:(t X. t)-1-1-onto->t))}
2		infxpidmlem.2	. . 3 |- A e. V
3	1, 2	infxpidmlem9 7503	. 2 |- E.g e. H A.h e. H -. g (. h
4	1, 2	infxpidmlem10 7504	. . . . 5 |- (A.h e. H -. g (. h -> (om ~<_ A -> g =/= (/)))
5		visset 1804	. . . . . . . . 9 |- g e. V
6	1, 5	infxpidmlem2 7496	. . . . . . . 8 |- (g e. H <-> (g = (/) \/ E.x((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x)))
7		neor 1630	. . . . . . . 8 |- ((g = (/) \/ E.x((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x)) <-> (g =/= (/) -> E.x((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x)))
8	6, 7	bitr 173	. . . . . . 7 |- (g e. H <-> (g =/= (/) -> E.x((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x)))
9		entrt 4395	. . . . . . . . . . . . . . . . . . . . 21 |- ((((x X. y) u. ((y X. x) u. (y X. y))) ~~ x /\ x ~~ y) -> ((x X. y) u. ((y X. x) u. (y X. y))) ~~ y)
10		entrt 4395	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x ~~ (x X. x) /\ (x X. x) ~~ (x X. y)) -> x ~~ (x X. y))
11		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- x e. V
12	11	enref 4372	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- x ~~ x
13		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- y e. V
14	11, 11, 11, 13	xpen 4468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x ~~ x /\ x ~~ y) -> (x X. x) ~~ (x X. y))
15	12, 14	mpan 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x ~~ y -> (x X. x) ~~ (x X. y))
16	10, 15	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((x ~~ (x X. x) /\ x ~~ y) -> x ~~ (x X. y))
17	16	adantll 392	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> x ~~ (x X. y))
18		entrt 4395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x ~~ (x X. x) /\ (x X. x) ~~ (y X. x)) -> x ~~ (y X. x))
19	11, 13, 11, 11	xpen 4468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((x ~~ y /\ x ~~ x) -> (x X. x) ~~ (y X. x))
20	12, 19	mpan2 694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x ~~ y -> (x X. x) ~~ (y X. x))
21	18, 20	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x ~~ (x X. x) /\ x ~~ y) -> x ~~ (y X. x))
22		entrt 4395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x ~~ (x X. x) /\ (x X. x) ~~ (y X. y)) -> x ~~ (y X. y))
23	11, 13, 11, 13	xpen 4468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((x ~~ y /\ x ~~ y) -> (x X. x) ~~ (y X. y))
24	23	anidms 434	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x ~~ y -> (x X. x) ~~ (y X. y))
25	22, 24	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x ~~ (x X. x) /\ x ~~ y) -> x ~~ (y X. y))
26	21, 25	jca 288	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x ~~ (x X. x) /\ x ~~ y) -> (x ~~ (y X. x) /\ x ~~ (y X. y)))
27	26	adantll 392	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> (x ~~ (y X. x) /\ x ~~ (y X. y)))
28	13, 11	xpex 3250	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y X. x) e. V
29	13, 13	xpex 3250	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y X. y) e. V
30	28, 29	infxpidmlem1 7495	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((om ~<_ x /\ x ~~ (x X. x)) -> ((x ~~ (y X. x) /\ x ~~ (y X. y)) -> x ~~ ((y X. x) u. (y X. y))))
31	30	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> ((x ~~ (y X. x) /\ x ~~ (y X. y)) -> x ~~ ((y X. x) u. (y X. y))))
32	27, 31	mpd 26	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> x ~~ ((y X. x) u. (y X. y)))
33	11, 13	xpex 3250	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x X. y) e. V
34	28, 29	unex 2863	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y X. x) u. (y X. y)) e. V
35	33, 34	infxpidmlem1 7495	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((om ~<_ x /\ x ~~ (x X. x)) -> ((x ~~ (x X. y) /\ x ~~ ((y X. x) u. (y X. y))) -> x ~~ ((x X. y) u. ((y X. x) u. (y X. y)))))
36	35	adantr 389	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> ((x ~~ (x X. y) /\ x ~~ ((y X. x) u. (y X. y))) -> x ~~ ((x X. y) u. ((y X. x) u. (y X. y)))))
37	17, 32, 36	mp2and 701	. . . . . . . . . . . . . . . . . . . . . 22 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> x ~~ ((x X. y) u. ((y X. x) u. (y X. y))))
38	33, 34	unex 2863	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x X. y) u. ((y X. x) u. (y X. y))) e. V
39	38	ensym 4393	. . . . . . . . . . . . . . . . . . . . . 22 |- (x ~~ ((x X. y) u. ((y X. x) u. (y X. y))) -> ((x X. y) u. ((y X. x) u. (y X. y))) ~~ x)
40	37, 39	syl 10	. . . . . . . . . . . . . . . . . . . . 21 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> ((x X. y) u. ((y X. x) u. (y X. y))) ~~ x)
41		pm3.27 323	. . . . . . . . . . . . . . . . . . . . 21 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> x ~~ y)
42	9, 40, 41	sylanc 471	. . . . . . . . . . . . . . . . . . . 20 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> ((x X. y) u. ((y X. x) u. (y X. y))) ~~ y)
43	11	ensym 4393	. . . . . . . . . . . . . . . . . . . 20 |- ((x X. x) ~~ x -> x ~~ (x X. x))
44	42, 43	sylanl2 461	. . . . . . . . . . . . . . . . . . 19 |- (((om ~<_ x /\ (x X. x) ~~ x) /\ x ~~ y) -> ((x X. y) u. ((y X. x) u. (y X. y))) ~~ y)
45	13	bren 4359	. . . . . . . . . . . . . . . . . . 19 |- (((x X. y) u. ((y X. x) u. (y X. y))) ~~ y <-> E.u u:((x X. y) u. ((y X. x) u. (y X. y)))-1-1-onto->y)
46	44, 45	sylib 198	. . . . . . . . . . . . . . . . . 18 |- (((om ~<_ x /\ (x X. x) ~~ x) /\ x ~~ y) -> E.u u:((x X. y) u. ((y X. x) u. (y X. y)))-1-1-onto->y)
47	11, 11	xpex 3250	. . . . . . . . . . . . . . . . . . . . 21 |- (x X. x) e. V
48	47	f1oen 4379	. . . . . . . . . . . . . . . . . . . 20 |- (g:(x X. x)-1-1-onto->x -> (x X. x) ~~ x)
49	48	anim2i 335	. . . . . . . . . . . . . . . . . . 19 |- ((om ~<_ x /\ g:(x X. x)-1-1-onto->x) -> (om ~<_ x /\ (x X. x) ~~ x))
50	49	adantlr 393	. . . . . . . . . . . . . . . . . 18 |- (((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x) -> (om ~<_ x /\ (x X. x) ~~ x))
51	46, 50	sylan 448	. . . . . . . . . . . . . . . . 17 |- ((((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x) /\ x ~~ y) -> E.u u:((x X. y) u. ((y X. x) u. (y X. y)))-1-1-onto->y)
52	51	adantrr 395	. . . . . . . . . . . . . . . 16 |- ((((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x) /\ (x ~~ y /\ y (_ (A \ x))) -> E.u u:((x X. y) u. ((y X. x) u. (y X. y)))-1-1-onto->y)
53	1, 2	infxpidmlem11 7505	. . . . . . . . . . . . . . . . . 18 |- (((((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)
54	53	ex 373	. . . . . . . . . . . . . . . . 17 |- ((((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))
55	54	19.23adv 1209	. . . . . . . . . . . . . . . 16 |- ((((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x) /\ (x ~~ y /\ y (_ (A \ x))) -> (E.u u:((x X. y) u. ((y X. x) u. (y X. y)))-1-1-onto->y -> E.h e. H g (. h))
56	52, 55	mpd 26	. . . . . . . . . . . . . . 15 |- ((((om ~<_ x /\ x (_ A) /\ g:(x X. x)