Theorem canthwe 8482

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

Hypothesis

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

Assertion

Ref	Expression
canthwe	|- ( A e. V -> A ~< O )

Distinct variable groups:   x, r, O   V, r, x   A, r, x

Proof of Theorem canthwe

Dummy variables u y f v w a s z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp1 957	. . . . . . . 8 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> x C_ A )
2		vex 2919	. . . . . . . . 9 |- x e. _V
3	2	elpw 3765	. . . . . . . 8 |- ( x e. ~P A <-> x C_ A )
4	1, 3	sylibr 204	. . . . . . 7 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> x e. ~P A )
5		simp2 958	. . . . . . . . 9 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> r C_ ( x X. x ) )
6		xpss12 4940	. . . . . . . . . 10 |- ( ( x C_ A /\ x C_ A ) -> ( x X. x ) C_ ( A X. A ) )
7	1, 1, 6	syl2anc 643	. . . . . . . . 9 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> ( x X. x ) C_ ( A X. A ) )
8	5, 7	sstrd 3318	. . . . . . . 8 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> r C_ ( A X. A ) )
9		vex 2919	. . . . . . . . 9 |- r e. _V
10	9	elpw 3765	. . . . . . . 8 |- ( r e. ~P ( A X. A ) <-> r C_ ( A X. A ) )
11	8, 10	sylibr 204	. . . . . . 7 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> r e. ~P ( A X. A ) )
12	4, 11	jca 519	. . . . . 6 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> ( x e. ~P A /\ r e. ~P ( A X. A ) ) )
13	12	ssopab2i 4442	. . . . 5 |- { <. 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 ) ) }
14		canthwe.1	. . . . 5 |- O = { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) }
15		df-xp 4843	. . . . 5 |- ( ~P A X. ~P ( A X. A ) ) = { <. x , r >. | ( x e. ~P A /\ r e. ~P ( A X. A ) ) }
16	13, 14, 15	3sstr4i 3347	. . . 4 |- O C_ ( ~P A X. ~P ( A X. A ) )
17		pwexg 4343	. . . . 5 |- ( A e. V -> ~P A e. _V )
18		xpexg 4948	. . . . . . 7 |- ( ( A e. V /\ A e. V ) -> ( A X. A ) e. _V )
19	18	anidms 627	. . . . . 6 |- ( A e. V -> ( A X. A ) e. _V )
20		pwexg 4343	. . . . . 6 |- ( ( A X. A ) e. _V -> ~P ( A X. A ) e. _V )
21	19, 20	syl 16	. . . . 5 |- ( A e. V -> ~P ( A X. A ) e. _V )
22		xpexg 4948	. . . . 5 |- ( ( ~P A e. _V /\ ~P ( A X. A ) e. _V ) -> ( ~P A X. ~P ( A X. A ) ) e. _V )
23	17, 21, 22	syl2anc 643	. . . 4 |- ( A e. V -> ( ~P A X. ~P ( A X. A ) ) e. _V )
24		ssexg 4309	. . . 4 |- ( ( O C_ ( ~P A X. ~P ( A X. A ) ) /\ ( ~P A X. ~P ( A X. A ) ) e. _V ) -> O e. _V )
25	16, 23, 24	sylancr 645	. . 3 |- ( A e. V -> O e. _V )
26		simpr 448	. . . . . . . 8 |- ( ( A e. V /\ u e. A ) -> u e. A )
27	26	snssd 3903	. . . . . . 7 |- ( ( A e. V /\ u e. A ) -> { u } C_ A )
28		0ss 3616	. . . . . . . 8 |- (/) C_ ( { u } X. { u } )
29	28	a1i 11	. . . . . . 7 |- ( ( A e. V /\ u e. A ) -> (/) C_ ( { u } X. { u } ) )
30		rel0 4958	. . . . . . . 8 |- Rel (/)
31		noel 3592	. . . . . . . . . 10 |- -. <. u , u >. e. (/)
32		df-br 4173	. . . . . . . . . 10 |- ( u (/) u <-> <. u , u >. e. (/) )
33	31, 32	mtbir 291	. . . . . . . . 9 |- -. u (/) u
34		wesn 4908	. . . . . . . . 9 |- ( Rel (/) -> ( (/) We { u } <-> -. u (/) u ) )
35	33, 34	mpbiri 225	. . . . . . . 8 |- ( Rel (/) -> (/) We { u } )
36	30, 35	mp1i 12	. . . . . . 7 |- ( ( A e. V /\ u e. A ) -> (/) We { u } )
37		snex 4365	. . . . . . . 8 |- { u } e. _V
38		0ex 4299	. . . . . . . 8 |- (/) e. _V
39		simpl 444	. . . . . . . . . 10 |- ( ( x = { u } /\ r = (/) ) -> x = { u } )
40	39	sseq1d 3335	. . . . . . . . 9 |- ( ( x = { u } /\ r = (/) ) -> ( x C_ A <-> { u } C_ A ) )
41		simpr 448	. . . . . . . . . 10 |- ( ( x = { u } /\ r = (/) ) -> r = (/) )
42	39, 39	xpeq12d 4862	. . . . . . . . . 10 |- ( ( x = { u } /\ r = (/) ) -> ( x X. x ) = ( { u } X. { u } ) )
43	41, 42	sseq12d 3337	. . . . . . . . 9 |- ( ( x = { u } /\ r = (/) ) -> ( r C_ ( x X. x ) <-> (/) C_ ( { u } X. { u } ) ) )
44		weeq2 4531	. . . . . . . . . 10 |- ( x = { u } -> ( r We x <-> r We { u } ) )
45		weeq1 4530	. . . . . . . . . 10 |- ( r = (/) -> ( r We { u } <-> (/) We { u } ) )
46	44, 45	sylan9bb 681	. . . . . . . . 9 |- ( ( x = { u } /\ r = (/) ) -> ( r We x <-> (/) We { u } ) )
47	40, 43, 46	3anbi123d 1254	. . . . . . . 8 |- ( ( x = { u } /\ r = (/) ) -> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) <-> ( { u } C_ A /\ (/) C_ ( { u } X. { u } ) /\ (/) We { u } ) ) )
48	37, 38, 47	opelopaba 4431	. . . . . . 7 |- ( <. { u } , (/) >. e. { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } <-> ( { u } C_ A /\ (/) C_ ( { u } X. { u } ) /\ (/) We { u } ) )
49	27, 29, 36, 48	syl3anbrc 1138	. . . . . 6 |- ( ( A e. V /\ u e. A ) -> <. { u } , (/) >. e. { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } )
50	49, 14	syl6eleqr 2495	. . . . 5 |- ( ( A e. V /\ u e. A ) -> <. { u } , (/) >. e. O )
51	50	ex 424	. . . 4 |- ( A e. V -> ( u e. A -> <. { u } , (/) >. e. O ) )
52		eqid 2404	. . . . . . 7 |- (/) = (/)
53		snex 4365	. . . . . . . 8 |- { v } e. _V
54	53, 38	opth2 4398	. . . . . . 7 |- ( <. { u } , (/) >. = <. { v } , (/) >. <-> ( { u } = { v } /\ (/) = (/) ) )
55	52, 54	mpbiran2 886	. . . . . 6 |- ( <. { u } , (/) >. = <. { v } , (/) >. <-> { u } = { v } )
56		vex 2919	. . . . . . 7 |- u e. _V
57		sneqbg 3929	. . . . . . 7 |- ( u e. _V -> ( { u } = { v } <-> u = v ) )
58	56, 57	ax-mp 8	. . . . . 6 |- ( { u } = { v } <-> u = v )
59	55, 58	bitri 241	. . . . 5 |- ( <. { u } , (/) >. = <. { v } , (/) >. <-> u = v )
60	59	a1ii 25	. . . 4 |- ( A e. V -> ( ( u e. A /\ v e. A ) -> ( <. { u } , (/) >. = <. { v } , (/) >. <-> u = v ) ) )
61	51, 60	dom2d 7107	. . 3 |- ( A e. V -> ( O e. _V -> A ~<_ O ) )
62	25, 61	mpd 15	. 2 |- ( A e. V -> A ~<_ O )
63		eqid 2404	. . . . . . 7 |- { <. 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 ) ) }
64	63	fpwwe2cbv 8461	. . . . . 6 |- { <. 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 ) ) }
65		eqid 2404	. . . . . 6 |- 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 ) ) }
66		eqid 2404	. . . . . 6 |- ( `' ( { <. 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 ) ) } ) ) } )
67	14, 64, 65, 66	canthwelem 8481	. . . . 5 |- ( A e. V -> -. f : O -1-1-> A )
68		f1of1 5632	. . . . 5 |- ( f : O -1-1-onto-> A -> f : O -1-1-> A )
69	67, 68	nsyl 115	. . . 4 |- ( A e. V -> -. f : O -1-1-onto-> A )
70	69	nexdv 1937	. . 3 |- ( A e. V -> -. E. f f : O -1-1-onto-> A )
71		ensym 7115	. . . 4 |- ( A ~~ O -> O ~~ A )
72		bren 7076	. . . 4 |- ( O ~~ A <-> E. f f : O -1-1-onto-> A )
73	71, 72	sylib 189	. . 3 |- ( A ~~ O -> E. f f : O -1-1-onto-> A )
74	70, 73	nsyl 115	. 2 |- ( A e. V -> -. A ~~ O )
75		brsdom 7089	. 2 |- ( A ~< O <-> ( A ~<_ O /\ -. A ~~ O ) )
76	62, 74, 75	sylanbrc 646	1 |- ( A e. V -> A ~< O )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   E.wex 1547   = wceq 1649   e. wcel 1721   A.wral 2666   _Vcvv 2916   [.wsbc 3121   i^i cin 3279   C_ wss 3280   (/)c0 3588   ~Pcpw 3759   {csn 3774   <.cop 3777   U.cuni 3975   class class class wbr 4172   {copab 4225   We wwe 4500   X. cxp 4835   `'ccnv 4836   dom cdm 4837   "cima 4840   Rel wrel 4842   -1-1->wf1 5410   -1-1-onto->wf1o 5412   ` cfv 5413  (class class class)co 6040   ~~ cen 7065   ~<_ cdom 7066   ~< csdm 7067

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-riota 6508  df-recs 6592  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-oi 7435