Theorem infxpidmlem12 7564

Description: Lemma for infxpidm 7565. Letting x be the range of a maximal bijection g in H, infxpidmlem11 7563 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 7561, 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 7561	. 2 |- E.g e. H A.h e. H -. g (. h
4	1, 2	infxpidmlem10 7562	. . . . 5 |- (A.h e. H -. g (. h -> (om ~<_ A -> g =/= (/)))
5		visset 1816	. . . . . . . . 9 |- g e. V
6	1, 5	infxpidmlem2 7554	. . . . . . . 8 |- (g e. H <-> (g = (/) \/ E.x((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x)))
7		neor 1641	. . . . . . . 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 4420	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x ~~ (x X. x) /\ (x X. x) ~~ (x X. y)) -> x ~~ (x X. y))
10		visset 1816	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- x e. V
11	10	enref 4397	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- x ~~ x
12		visset 1816	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- y e. V
13	10, 10, 10, 12	xpen 4494	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x ~~ x /\ x ~~ y) -> (x X. x) ~~ (x X. y))
14	11, 13	mpan 697	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x ~~ y -> (x X. x) ~~ (x X. y))
15	9, 14	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((x ~~ (x X. x) /\ x ~~ y) -> x ~~ (x X. y))
16	15	adantll 394	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> x ~~ (x X. y))
17		entrt 4420	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x ~~ (x X. x) /\ (x X. x) ~~ (y X. x)) -> x ~~ (y X. x))
18	10, 12, 10, 10	xpen 4494	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((x ~~ y /\ x ~~ x) -> (x X. x) ~~ (y X. x))
19	11, 18	mpan2 698	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x ~~ y -> (x X. x) ~~ (y X. x))
20	17, 19	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x ~~ (x X. x) /\ x ~~ y) -> x ~~ (y X. x))
21		entrt 4420	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x ~~ (x X. x) /\ (x X. x) ~~ (y X. y)) -> x ~~ (y X. y))
22	10, 12, 10, 12	xpen 4494	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((x ~~ y /\ x ~~ y) -> (x X. x) ~~ (y X. y))
23	22	anidms 436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x ~~ y -> (x X. x) ~~ (y X. y))
24	21, 23	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x ~~ (x X. x) /\ x ~~ y) -> x ~~ (y X. y))
25	20, 24	jca 288	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x ~~ (x X. x) /\ x ~~ y) -> (x ~~ (y X. x) /\ x ~~ (y X. y)))
26	25	adantll 394	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> (x ~~ (y X. x) /\ x ~~ (y X. y)))
27	12, 10	xpex 3266	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y X. x) e. V
28	12, 12	xpex 3266	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y X. y) e. V
29	27, 28	infxpidmlem1 7553	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((om ~<_ x /\ x ~~ (x X. x)) -> ((x ~~ (y X. x) /\ x ~~ (y X. y)) -> x ~~ ((y X. x) u. (y X. y))))
30	29	adantr 391	. . . . . . . . . . . . . . . . . . . . . . . 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))))
31	26, 30	mpd 26	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> x ~~ ((y X. x) u. (y X. y)))
32	10, 12	xpex 3266	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x X. y) e. V
33	27, 28	unex 2878	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y X. x) u. (y X. y)) e. V
34	32, 33	infxpidmlem1 7553	. . . . . . . . . . . . . . . . . . . . . . . 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)))))
35	34	adantr 391	. . . . . . . . . . . . . . . . . . . . . . 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)))))
36	16, 31, 35	mp2and 705	. . . . . . . . . . . . . . . . . . . . . 22 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> x ~~ ((x X. y) u. ((y X. x) u. (y X. y))))
37	32, 33	unex 2878	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x X. y) u. ((y X. x) u. (y X. y))) e. V
38	37	ensym 4418	. . . . . . . . . . . . . . . . . . . . . 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)
39	36, 38	syl 10	. . . . . . . . . . . . . . . . . . . . 21 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> ((x X. y) u. ((y X. x) u. (y X. y))) ~~ x)
40		entrt 4420	. . . . . . . . . . . . . . . . . . . . 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)
41	39, 40	sylancom 477	. . . . . . . . . . . . . . . . . . . 20 |- (((om ~<_ x /\ x ~~ (x X. x)) /\ x ~~ y) -> ((x X. y) u. ((y X. x) u. (y X. y))) ~~ y)
42	10	ensym 4418	. . . . . . . . . . . . . . . . . . . 20 |- ((x X. x) ~~ x -> x ~~ (x X. x))
43	41, 42	sylanl2 463	. . . . . . . . . . . . . . . . . . 19 |- (((om ~<_ x /\ (x X. x) ~~ x) /\ x ~~ y) -> ((x X. y) u. ((y X. x) u. (y X. y))) ~~ y)
44	12	bren 4383	. . . . . . . . . . . . . . . . . . 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)
45	43, 44	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)
46	10, 10	xpex 3266	. . . . . . . . . . . . . . . . . . . . 21 |- (x X. x) e. V
47	46	f1oen 4404	. . . . . . . . . . . . . . . . . . . 20 |- (g:(x X. x)-1-1-onto->x -> (x X. x) ~~ x)
48	47	anim2i 335	. . . . . . . . . . . . . . . . . . 19 |- ((om ~<_ x /\ g:(x X. x)-1-1-onto->x) -> (om ~<_ x /\ (x X. x) ~~ x))
49	48	adantlr 395	. . . . . . . . . . . . . . . . . 18 |- (((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x) -> (om ~<_ x /\ (x X. x) ~~ x))
50	45, 49	sylan 450	. . . . . . . . . . . . . . . . 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)
51	50	adantrr 397	. . . . . . . . . . . . . . . 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)
52	1, 2	infxpidmlem11 7563	. . . . . . . . . . . . . . . . . 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)
53	52	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))
54	53	19.23adv 1216	. . . . . . . . . . . . . . . 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))
55	51, 54	mpd 26	. . . . . . . . . . . . . . 15 |- ((((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x) /\ (x ~~ y /\ y (_ (A \ x))) -> E.h e. H g (. h)
56	55	ex 373</