Theorem canthwe

Description: The set of well-orders of a set A strictly dominates A . A stronger form of canth2 . Corollary 1.4(b) of KanamoriPincus p. 417. (Contributed by Mario Carneiro, 31-May-2015)

	Ref	Expression
Hypothesis	canthwe.1	|- O = { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) }
Assertion	canthwe	|- ( A e. V -> A ~< O )

Proof

Step	Hyp	Ref	Expression
1		canthwe.1	|- O = { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) }
2		simp1	|- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> x C_ A )
3		velpw	|- ( x e. ~P A <-> x C_ A )
4	2 3	sylibr	|- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> x e. ~P A )
5		simp2	|- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> r C_ ( x X. x ) )
6		xpss12	|- ( ( x C_ A /\ x C_ A ) -> ( x X. x ) C_ ( A X. A ) )
7	2 2 6	syl2anc	|- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> ( x X. x ) C_ ( A X. A ) )
8	5 7	sstrd	|- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> r C_ ( A X. A ) )
9		velpw	|- ( r e. ~P ( A X. A ) <-> r C_ ( A X. A ) )
10	8 9	sylibr	|- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> r e. ~P ( A X. A ) )
11	4 10	jca	|- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> ( x e. ~P A /\ r e. ~P ( A X. A ) ) )
12	11	ssopab2i	|- { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } C_ { <. x , r >. | ( x e. ~P A /\ r e. ~P ( A X. A ) ) }
13		df-xp	|- ( ~P A X. ~P ( A X. A ) ) = { <. x , r >. | ( x e. ~P A /\ r e. ~P ( A X. A ) ) }
14	12 1 13	3sstr4i	|- O C_ ( ~P A X. ~P ( A X. A ) )
15		pwexg	|- ( A e. V -> ~P A e. _V )
16		sqxpexg	|- ( A e. V -> ( A X. A ) e. _V )
17	16	pwexd	|- ( A e. V -> ~P ( A X. A ) e. _V )
18	15 17	xpexd	|- ( A e. V -> ( ~P A X. ~P ( A X. A ) ) e. _V )
19		ssexg	|- ( ( O C_ ( ~P A X. ~P ( A X. A ) ) /\ ( ~P A X. ~P ( A X. A ) ) e. _V ) -> O e. _V )
20	14 18 19	sylancr	|- ( A e. V -> O e. _V )
21		simpr	|- ( ( A e. V /\ u e. A ) -> u e. A )
22	21	snssd	|- ( ( A e. V /\ u e. A ) -> { u } C_ A )
23		0ss	|- (/) C_ ( { u } X. { u } )
24	23	a1i	|- ( ( A e. V /\ u e. A ) -> (/) C_ ( { u } X. { u } ) )
25		rel0	|- Rel (/)
26		br0	|- -. u (/) u
27		wesn	|- ( Rel (/) -> ( (/) We { u } <-> -. u (/) u ) )
28	26 27	mpbiri	|- ( Rel (/) -> (/) We { u } )
29	25 28	mp1i	|- ( ( A e. V /\ u e. A ) -> (/) We { u } )
30		snex	|- { u } e. _V
31		0ex	|- (/) e. _V
32		simpl	|- ( ( x = { u } /\ r = (/) ) -> x = { u } )
33	32	sseq1d	|- ( ( x = { u } /\ r = (/) ) -> ( x C_ A <-> { u } C_ A ) )
34		simpr	|- ( ( x = { u } /\ r = (/) ) -> r = (/) )
35	32	sqxpeqd	|- ( ( x = { u } /\ r = (/) ) -> ( x X. x ) = ( { u } X. { u } ) )
36	34 35	sseq12d	|- ( ( x = { u } /\ r = (/) ) -> ( r C_ ( x X. x ) <-> (/) C_ ( { u } X. { u } ) ) )
37		weeq2	|- ( x = { u } -> ( r We x <-> r We { u } ) )
38		weeq1	|- ( r = (/) -> ( r We { u } <-> (/) We { u } ) )
39	37 38	sylan9bb	|- ( ( x = { u } /\ r = (/) ) -> ( r We x <-> (/) We { u } ) )
40	33 36 39	3anbi123d	|- ( ( x = { u } /\ r = (/) ) -> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) <-> ( { u } C_ A /\ (/) C_ ( { u } X. { u } ) /\ (/) We { u } ) ) )
41	30 31 40	opelopaba	|- ( <. { u } , (/) >. e. { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } <-> ( { u } C_ A /\ (/) C_ ( { u } X. { u } ) /\ (/) We { u } ) )
42	22 24 29 41	syl3anbrc	|- ( ( A e. V /\ u e. A ) -> <. { u } , (/) >. e. { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } )
43	42 1	eleqtrrdi	|- ( ( A e. V /\ u e. A ) -> <. { u } , (/) >. e. O )
44	43	ex	|- ( A e. V -> ( u e. A -> <. { u } , (/) >. e. O ) )
45		eqid	|- (/) = (/)
46		snex	|- { v } e. _V
47	46 31	opth2	|- ( <. { u } , (/) >. = <. { v } , (/) >. <-> ( { u } = { v } /\ (/) = (/) ) )
48	45 47	mpbiran2	|- ( <. { u } , (/) >. = <. { v } , (/) >. <-> { u } = { v } )
49		sneqbg	|- ( u e. _V -> ( { u } = { v } <-> u = v ) )
50	49	elv	|- ( { u } = { v } <-> u = v )
51	48 50	bitri	|- ( <. { u } , (/) >. = <. { v } , (/) >. <-> u = v )
52	51	2a1i	|- ( A e. V -> ( ( u e. A /\ v e. A ) -> ( <. { u } , (/) >. = <. { v } , (/) >. <-> u = v ) ) )
53	44 52	dom2d	|- ( A e. V -> ( O e. _V -> A ~<_ O ) )
54	20 53	mpd	|- ( A e. V -> A ~<_ O )
55		eqid	|- { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v f ( s i^i ( v X. v ) ) ) = z ) ) } = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v f ( s i^i ( v X. v ) ) ) = z ) ) }
56	55	fpwwe2cbv	|- { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v f ( s i^i ( v X. v ) ) ) = z ) ) } = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / w ]. ( w f ( r i^i ( w X. w ) ) ) = y ) ) }
57		eqid	|- U. dom { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v f ( s i^i ( v X. v ) ) ) = z ) ) } = U. dom { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v f ( s i^i ( v X. v ) ) ) = z ) ) }
58		eqid	|- ( `' ( { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v f ( s i^i ( v X. v ) ) ) = z ) ) } ` U. dom { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v f ( s i^i ( v X. v ) ) ) = z ) ) } ) " { ( U. dom { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v f ( s i^i ( v X. v ) ) ) = z ) ) } f ( { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v f ( s i^i ( v X. v ) ) ) = z ) ) } ` U. dom { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v f ( s i^i ( v X. v ) ) ) = z ) ) } ) ) } ) = ( `' ( { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v f ( s i^i ( v X. v ) ) ) = z ) ) } ` U. dom { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v f ( s i^i ( v X. v ) ) ) = z ) ) } ) " { ( U. dom { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v f ( s i^i ( v X. v ) ) ) = z ) ) } f ( { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v f ( s i^i ( v X. v ) ) ) = z ) ) } ` U. dom { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v f ( s i^i ( v X. v ) ) ) = z ) ) } ) ) } )
59	1 56 57 58	canthwelem	|- ( A e. V -> -. f : O -1-1-> A )
60		f1of1	|- ( f : O -1-1-onto-> A -> f : O -1-1-> A )
61	59 60	nsyl	|- ( A e. V -> -. f : O -1-1-onto-> A )
62	61	nexdv	|- ( A e. V -> -. E. f f : O -1-1-onto-> A )
63		ensym	|- ( A ~~ O -> O ~~ A )
64		bren	|- ( O ~~ A <-> E. f f : O -1-1-onto-> A )
65	63 64	sylib	|- ( A ~~ O -> E. f f : O -1-1-onto-> A )
66	62 65	nsyl	|- ( A e. V -> -. A ~~ O )
67		brsdom	|- ( A ~< O <-> ( A ~<_ O /\ -. A ~~ O ) )
68	54 66 67	sylanbrc	|- ( A e. V -> A ~< O )