Theorem canthwe 9025

Description: The set of well-orders of a set A strictly dominates A. A stronger form of canth2 7667. 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 996	. . . . . . . 8 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> x C_ A )
2		selpw 4017	. . . . . . . 8 |- ( x e. ~P A <-> x C_ A )
3	1, 2	sylibr 212	. . . . . . 7 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> x e. ~P A )
4		simp2 997	. . . . . . . . 9 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> r C_ ( x X. x ) )
5		xpss12 5106	. . . . . . . . . 10 |- ( ( x C_ A /\ x C_ A ) -> ( x X. x ) C_ ( A X. A ) )
6	1, 1, 5	syl2anc 661	. . . . . . . . 9 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> ( x X. x ) C_ ( A X. A ) )
7	4, 6	sstrd 3514	. . . . . . . 8 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> r C_ ( A X. A ) )
8		selpw 4017	. . . . . . . 8 |- ( r e. ~P ( A X. A ) <-> r C_ ( A X. A ) )
9	7, 8	sylibr 212	. . . . . . 7 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> r e. ~P ( A X. A ) )
10	3, 9	jca 532	. . . . . 6 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> ( x e. ~P A /\ r e. ~P ( A X. A ) ) )
11	10	ssopab2i 4775	. . . . 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 ) ) }
12		canthwe.1	. . . . 5 |- O = { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) }
13		df-xp 5005	. . . . 5 |- ( ~P A X. ~P ( A X. A ) ) = { <. x , r >. | ( x e. ~P A /\ r e. ~P ( A X. A ) ) }
14	11, 12, 13	3sstr4i 3543	. . . 4 |- O C_ ( ~P A X. ~P ( A X. A ) )
15		pwexg 4631	. . . . 5 |- ( A e. V -> ~P A e. _V )
16		xpexg 6709	. . . . . . 7 |- ( ( A e. V /\ A e. V ) -> ( A X. A ) e. _V )
17	16	anidms 645	. . . . . 6 |- ( A e. V -> ( A X. A ) e. _V )
18		pwexg 4631	. . . . . 6 |- ( ( A X. A ) e. _V -> ~P ( A X. A ) e. _V )
19	17, 18	syl 16	. . . . 5 |- ( A e. V -> ~P ( A X. A ) e. _V )
20		xpexg 6709	. . . . 5 |- ( ( ~P A e. _V /\ ~P ( A X. A ) e. _V ) -> ( ~P A X. ~P ( A X. A ) ) e. _V )
21	15, 19, 20	syl2anc 661	. . . 4 |- ( A e. V -> ( ~P A X. ~P ( A X. A ) ) e. _V )
22		ssexg 4593	. . . 4 |- ( ( O C_ ( ~P A X. ~P ( A X. A ) ) /\ ( ~P A X. ~P ( A X. A ) ) e. _V ) -> O e. _V )
23	14, 21, 22	sylancr 663	. . 3 |- ( A e. V -> O e. _V )
24		simpr 461	. . . . . . . 8 |- ( ( A e. V /\ u e. A ) -> u e. A )
25	24	snssd 4172	. . . . . . 7 |- ( ( A e. V /\ u e. A ) -> { u } C_ A )
26		0ss 3814	. . . . . . . 8 |- (/) C_ ( { u } X. { u } )
27	26	a1i 11	. . . . . . 7 |- ( ( A e. V /\ u e. A ) -> (/) C_ ( { u } X. { u } ) )
28		rel0 5125	. . . . . . . 8 |- Rel (/)
29		noel 3789	. . . . . . . . . 10 |- -. <. u , u >. e. (/)
30		df-br 4448	. . . . . . . . . 10 |- ( u (/) u <-> <. u , u >. e. (/) )
31	29, 30	mtbir 299	. . . . . . . . 9 |- -. u (/) u
32		wesn 5070	. . . . . . . . 9 |- ( Rel (/) -> ( (/) We { u } <-> -. u (/) u ) )
33	31, 32	mpbiri 233	. . . . . . . 8 |- ( Rel (/) -> (/) We { u } )
34	28, 33	mp1i 12	. . . . . . 7 |- ( ( A e. V /\ u e. A ) -> (/) We { u } )
35		snex 4688	. . . . . . . 8 |- { u } e. _V
36		0ex 4577	. . . . . . . 8 |- (/) e. _V
37		simpl 457	. . . . . . . . . 10 |- ( ( x = { u } /\ r = (/) ) -> x = { u } )
38	37	sseq1d 3531	. . . . . . . . 9 |- ( ( x = { u } /\ r = (/) ) -> ( x C_ A <-> { u } C_ A ) )
39		simpr 461	. . . . . . . . . 10 |- ( ( x = { u } /\ r = (/) ) -> r = (/) )
40	37, 37	xpeq12d 5024	. . . . . . . . . 10 |- ( ( x = { u } /\ r = (/) ) -> ( x X. x ) = ( { u } X. { u } ) )
41	39, 40	sseq12d 3533	. . . . . . . . 9 |- ( ( x = { u } /\ r = (/) ) -> ( r C_ ( x X. x ) <-> (/) C_ ( { u } X. { u } ) ) )
42		weeq2 4868	. . . . . . . . . 10 |- ( x = { u } -> ( r We x <-> r We { u } ) )
43		weeq1 4867	. . . . . . . . . 10 |- ( r = (/) -> ( r We { u } <-> (/) We { u } ) )
44	42, 43	sylan9bb 699	. . . . . . . . 9 |- ( ( x = { u } /\ r = (/) ) -> ( r We x <-> (/) We { u } ) )
45	38, 41, 44	3anbi123d 1299	. . . . . . . 8 |- ( ( x = { u } /\ r = (/) ) -> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) <-> ( { u } C_ A /\ (/) C_ ( { u } X. { u } ) /\ (/) We { u } ) ) )
46	35, 36, 45	opelopaba 4763	. . . . . . 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 } ) )
47	25, 27, 34, 46	syl3anbrc 1180	. . . . . 6 |- ( ( A e. V /\ u e. A ) -> <. { u } , (/) >. e. { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } )
48	47, 12	syl6eleqr 2566	. . . . 5 |- ( ( A e. V /\ u e. A ) -> <. { u } , (/) >. e. O )
49	48	ex 434	. . . 4 |- ( A e. V -> ( u e. A -> <. { u } , (/) >. e. O ) )
50		eqid 2467	. . . . . . 7 |- (/) = (/)
51		snex 4688	. . . . . . . 8 |- { v } e. _V
52	51, 36	opth2 4725	. . . . . . 7 |- ( <. { u } , (/) >. = <. { v } , (/) >. <-> ( { u } = { v } /\ (/) = (/) ) )
53	50, 52	mpbiran2 917	. . . . . 6 |- ( <. { u } , (/) >. = <. { v } , (/) >. <-> { u } = { v } )
54		vex 3116	. . . . . . 7 |- u e. _V
55		sneqbg 4197	. . . . . . 7 |- ( u e. _V -> ( { u } = { v } <-> u = v ) )
56	54, 55	ax-mp 5	. . . . . 6 |- ( { u } = { v } <-> u = v )
57	53, 56	bitri 249	. . . . 5 |- ( <. { u } , (/) >. = <. { v } , (/) >. <-> u = v )
58	57	a1ii 27	. . . 4 |- ( A e. V -> ( ( u e. A /\ v e. A ) -> ( <. { u } , (/) >. = <. { v } , (/) >. <-> u = v ) ) )
59	49, 58	dom2d 7553	. . 3 |- ( A e. V -> ( O e. _V -> A ~<_ O ) )
60	23, 59	mpd 15	. 2 |- ( A e. V -> A ~<_ O )
61		eqid 2467	. . . . . . 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 ) ) }
62	61	fpwwe2cbv 9004	. . . . . 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 ) ) }
63		eqid 2467	. . . . . 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 ) ) }
64		eqid 2467	. . . . . 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 ) ) } ) ) } )
65	12, 62, 63, 64	canthwelem 9024	. . . . 5 |- ( A e. V -> -. f : O -1-1-> A )
66		f1of1 5813	. . . . 5 |- ( f : O -1-1-onto-> A -> f : O -1-1-> A )
67	65, 66	nsyl 121	. . . 4 |- ( A e. V -> -. f : O -1-1-onto-> A )
68	67	nexdv 1832	. . 3 |- ( A e. V -> -. E. f f : O -1-1-onto-> A )
69		ensym 7561	. . . 4 |- ( A ~~ O -> O ~~ A )
70		bren 7522	. . . 4 |- ( O ~~ A <-> E. f f : O -1-1-onto-> A )
71	69, 70	sylib 196	. . 3 |- ( A ~~ O -> E. f f : O -1-1-onto-> A )
72	68, 71	nsyl 121	. 2 |- ( A e. V -> -. A ~~ O )
73		brsdom 7535	. 2 |- ( A ~< O <-> ( A ~<_ O /\ -. A ~~ O ) )
74	60, 72, 73	sylanbrc 664	1 |- ( A e. V -> A ~< O )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   = wceq 1379   E.wex 1596   e. wcel 1767   A.wral 2814   _Vcvv 3113   [.wsbc 3331   i^i cin 3475   C_ wss 3476   (/)c0 3785   ~Pcpw 4010   {csn 4027   <.cop 4033   U.cuni 4245   class class class wbr 4447   {copab 4504   We wwe 4837   X. cxp 4997   `'ccnv 4998   dom cdm 4999   "cima 5002   Rel wrel 5004   -1-1->wf1 5583   -1-1-onto->wf1o 5585   ` cfv 5586  (class class class)co 6282   ~~ cen 7510   ~<_ cdom 7511   ~< csdm 7512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-isom 5595  df-riota 6243  df-ov 6285  df-recs 7039  df-er 7308  df-en 7514  df-dom 7515  df-sdom 7516  df-oi 7931

This theorem is referenced by: (None)