This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 vsnex 
 |-  { 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 34 32 weeq12d 
 |-  ( ( x = { u } /\ r = (/) ) -> ( r We x <-> (/) We { u } ) )
38 33 36 37 3anbi123d 
 |-  ( ( x = { u } /\ r = (/) ) -> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) <-> ( { u } C_ A /\ (/) C_ ( { u } X. { u } ) /\ (/) We { u } ) ) )
39 30 31 38 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 } ) )
40 22 24 29 39 syl3anbrc 
 |-  ( ( A e. V /\ u e. A ) -> <. { u } , (/) >. e. { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } )
41 40 1 eleqtrrdi 
 |-  ( ( A e. V /\ u e. A ) -> <. { u } , (/) >. e. O )
42 41 ex 
 |-  ( A e. V -> ( u e. A -> <. { u } , (/) >. e. O ) )
43 eqid 
 |-  (/) = (/)
44 vsnex 
 |-  { v } e. _V
45 44 31 opth2 
 |-  ( <. { u } , (/) >. = <. { v } , (/) >. <-> ( { u } = { v } /\ (/) = (/) ) )
46 43 45 mpbiran2 
 |-  ( <. { u } , (/) >. = <. { v } , (/) >. <-> { u } = { v } )
47 sneqbg 
 |-  ( u e. _V -> ( { u } = { v } <-> u = v ) )
48 47 elv 
 |-  ( { u } = { v } <-> u = v )
49 46 48 bitri 
 |-  ( <. { u } , (/) >. = <. { v } , (/) >. <-> u = v )
50 49 2a1i 
 |-  ( A e. V -> ( ( u e. A /\ v e. A ) -> ( <. { u } , (/) >. = <. { v } , (/) >. <-> u = v ) ) )
51 42 50 dom2d 
 |-  ( A e. V -> ( O e. _V -> A ~<_ O ) )
52 20 51 mpd 
 |-  ( A e. V -> A ~<_ O )
53 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 ) ) }
54 53 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 ) ) }
55 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 ) ) }
56 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 ) ) } ) ) } )
57 1 54 55 56 canthwelem 
 |-  ( A e. V -> -. f : O -1-1-> A )
58 f1of1 
 |-  ( f : O -1-1-onto-> A -> f : O -1-1-> A )
59 57 58 nsyl 
 |-  ( A e. V -> -. f : O -1-1-onto-> A )
60 59 nexdv 
 |-  ( A e. V -> -. E. f f : O -1-1-onto-> A )
61 ensym 
 |-  ( A ~~ O -> O ~~ A )
62 bren 
 |-  ( O ~~ A <-> E. f f : O -1-1-onto-> A )
63 61 62 sylib 
 |-  ( A ~~ O -> E. f f : O -1-1-onto-> A )
64 60 63 nsyl 
 |-  ( A e. V -> -. A ~~ O )
65 brsdom 
 |-  ( A ~< O <-> ( A ~<_ O /\ -. A ~~ O ) )
66 52 64 65 sylanbrc 
 |-  ( A e. V -> A ~< O )