Theorem infxpidmlem12 4944

Description: Lemma for infxpidm 4945. Letting x be the range of a maximal bijection g in H, infxpidmlem11 4943 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 4941, 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(s):   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 4941	. 2 |- E.g e. H A.h e. H -. g (. h
4	1, 2	infxpidmlem10 4942	. . . . 5 |- (A.h e. H -. g (. h -> (om ~<_ A -> -. g = (/)))
5		visset 1350	. . . . . . . . 9 |- g e. V
6	1, 5	infxpidmlem2 4934	. . . . . . . 8 |- (g e. H <-> (g = (/) \/ E.x((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x)))
7		df-or 197	. . . . . . . 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 151	. . . . . . 7 |- (g e. H <-> (-. g = (/) -> E.x((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x)))
9		entrt 3319	. . . . . . . . . . . . . . . . . . . . 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 3319	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x ~~ (x X. x) /\ (x X. x) ~~ (x X. y)) -> x ~~ (x X. y))
11		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- x e. V
12	11	enref 3295	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- x ~~ x
13		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- y e. V
14	11, 11, 11, 13	xpen 3383	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x ~~ x /\ x ~~ y) -> (x X. x) ~~ (x X. y))
15	12, 14	mpan 518	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x ~~ y -> (x X. x) ~~ (x X. y))
16	10, 15	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((x ~~ (x X. x) /\ x ~~ y) -> x ~~ (x X. y))
17	16	adantll 309	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> x ~~ (x X. y))
18		entrt 3319	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x ~~ (x X. x) /\ (x X. x) ~~ (y X. x)) -> x ~~ (y X. x))
19	11, 13, 11, 11	xpen 3383	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((x ~~ y /\ x ~~ x) -> (x X. x) ~~ (y X. x))
20	12, 19	mpan2 519	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x ~~ y -> (x X. x) ~~ (y X. x))
21	18, 20	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x ~~ (x X. x) /\ x ~~ y) -> x ~~ (y X. x))
22		entrt 3319	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x ~~ (x X. x) /\ (x X. x) ~~ (y X. y)) -> x ~~ (y X. y))
23	11, 13, 11, 13	xpen 3383	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((x ~~ y /\ x ~~ y) -> (x X. x) ~~ (y X. y))
24	23	anidms 332	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x ~~ y -> (x X. x) ~~ (y X. y))
25	22, 24	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x ~~ (x X. x) /\ x ~~ y) -> x ~~ (y X. y))
26	21, 25	jca 236	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x ~~ (x X. x) /\ x ~~ y) -> (x ~~ (y X. x) /\ x ~~ (y X. y)))
27	26	adantll 309	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> (x ~~ (y X. x) /\ x ~~ (y X. y)))
28	13, 11	xpex 2488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y X. x) e. V
29	13, 13	xpex 2488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y X. y) e. V
30	28, 29	infxpidmlem1 4933	. . . . . . . . . . . . . . . . . . . . . . . . 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 306	. . . . . . . . . . . . . . . . . . . . . . . 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 46	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> x ~~ ((y X. x) u. (y X. y)))
33	11, 13	xpex 2488	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x X. y) e. V
34	28, 29	unex 1949	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y X. x) u. (y X. y)) e. V
35	33, 34	infxpidmlem1 4933	. . . . . . . . . . . . . . . . . . . . . . . 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 306	. . . . . . . . . . . . . . . . . . . . . . 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 526	. . . . . . . . . . . . . . . . . . . . . 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 1949	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x X. y) u. ((y X. x) u. (y X. y))) e. V
39	38	ensym 3317	. . . . . . . . . . . . . . . . . . . . . 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 12	. . . . . . . . . . . . . . . . . . . . 21 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> ((x X. y) u. ((y X. x) u. (y X. y))) ~~ x)
41		pm3.27 260	. . . . . . . . . . . . . . . . . . . . 21 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> x ~~ y)
42	9, 40, 41	sylanc 361	. . . . . . . . . . . . . . . . . . . 20 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> ((x X. y) u. ((y X. x) u. (y X. y))) ~~ y)
43	11	ensym 3317	. . . . . . . . . . . . . . . . . . . 20 |- ((x X. x) ~~ x -> x ~~ (x X. x))
44	42, 43	sylan12 355	. . . . . . . . . . . . . . . . . . 19 |- (((om ~<_ x /\ (x X. x) ~~ x) /\ x ~~ y) -> ((x X. y) u. ((y X. x) u. (y X. y))) ~~ y)
45	13	bren 3282	. . . . . . . . . . . . . . . . . . 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 173	. . . . . . . . . . . . . . . . . 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 2488	. . . . . . . . . . . . . . . . . . . . 21 |- (x X. x) e. V
48	47	f1oen 3301	. . . . . . . . . . . . . . . . . . . 20 |- (g:(x X. x)-1-1-onto->x -> (x X. x) ~~ x)
49	48	anim2i 270	. . . . . . . . . . . . . . . . . . 19 |- ((om ~<_ x /\ g:(x X. x)-1-1-onto->x) -> (om ~<_ x /\ (x X. x) ~~ x))
50	49	adantlr 310	. . . . . . . . . . . . . . . . . 18 |- (((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x) -> (om ~<_ x /\ (x X. x) ~~ x))
51	46, 50	sylan 343	. . . . . . . . . . . . . . . . 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 312	. . . . . . . . . . . . . . . 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 4943	. . . . . . . . . . . . . . . . . 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	exp 291	. . . . . . . . . . . . . . . . 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 954	. . . . . . . . . . . . . . . 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 46	. . . . . . . . . . . . . . 15 |- ((((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x) /\ (x ~~ y /\ y (_ (A \ x))) -> E.h e. H g (. h)
57	56	exp 291	. . . . . . . . . . . . . 14 |- (((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x) -> ((x ~~ y /\ y