Metamath Proof Explorer

Theorem canthnum

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

Ref Expression
Assertion canthnum 
|- ( A e. V -> A ~< ( ~P A i^i dom card ) )

Proof

Step Hyp Ref Expression
1 pwexg 
 |-  ( A e. V -> ~P A e. _V )
2 inex1g 
 |-  ( ~P A e. _V -> ( ~P A i^i Fin ) e. _V )
3 infpwfidom 
 |-  ( ( ~P A i^i Fin ) e. _V -> A ~<_ ( ~P A i^i Fin ) )
4 1 2 3 3syl 
 |-  ( A e. V -> A ~<_ ( ~P A i^i Fin ) )
5 inex1g 
 |-  ( ~P A e. _V -> ( ~P A i^i dom card ) e. _V )
6 1 5 syl 
 |-  ( A e. V -> ( ~P A i^i dom card ) e. _V )
7 finnum 
 |-  ( x e. Fin -> x e. dom card )
8 7 ssriv 
 |-  Fin C_ dom card
9 sslin 
 |-  ( Fin C_ dom card -> ( ~P A i^i Fin ) C_ ( ~P A i^i dom card ) )
10 8 9 ax-mp 
 |-  ( ~P A i^i Fin ) C_ ( ~P A i^i dom card )
11 ssdomg 
 |-  ( ( ~P A i^i dom card ) e. _V -> ( ( ~P A i^i Fin ) C_ ( ~P A i^i dom card ) -> ( ~P A i^i Fin ) ~<_ ( ~P A i^i dom card ) ) )
12 6 10 11 mpisyl 
 |-  ( A e. V -> ( ~P A i^i Fin ) ~<_ ( ~P A i^i dom card ) )
13 domtr 
 |-  ( ( A ~<_ ( ~P A i^i Fin ) /\ ( ~P A i^i Fin ) ~<_ ( ~P A i^i dom card ) ) -> A ~<_ ( ~P A i^i dom card ) )
14 4 12 13 syl2anc 
 |-  ( A e. V -> A ~<_ ( ~P A i^i dom card ) )
15 eqid 
 |-  { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) }
16 15 fpwwecbv 
 |-  { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( f ` ( `' s " { z } ) ) = z ) ) }
17 eqid 
 |-  U. dom { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } = U. dom { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) }
18 eqid 
 |-  ( `' ( { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } ` U. dom { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } ) " { ( f ` U. dom { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } ) } ) = ( `' ( { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } ` U. dom { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } ) " { ( f ` U. dom { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } ) } )
19 16 17 18 canthnumlem 
 |-  ( A e. V -> -. f : ( ~P A i^i dom card ) -1-1-> A )
20 f1of1 
 |-  ( f : ( ~P A i^i dom card ) -1-1-onto-> A -> f : ( ~P A i^i dom card ) -1-1-> A )
21 19 20 nsyl 
 |-  ( A e. V -> -. f : ( ~P A i^i dom card ) -1-1-onto-> A )
22 21 nexdv 
 |-  ( A e. V -> -. E. f f : ( ~P A i^i dom card ) -1-1-onto-> A )
23 ensym 
 |-  ( A ~~ ( ~P A i^i dom card ) -> ( ~P A i^i dom card ) ~~ A )
24 bren 
 |-  ( ( ~P A i^i dom card ) ~~ A <-> E. f f : ( ~P A i^i dom card ) -1-1-onto-> A )
25 23 24 sylib 
 |-  ( A ~~ ( ~P A i^i dom card ) -> E. f f : ( ~P A i^i dom card ) -1-1-onto-> A )
26 22 25 nsyl 
 |-  ( A e. V -> -. A ~~ ( ~P A i^i dom card ) )
27 brsdom 
 |-  ( A ~< ( ~P A i^i dom card ) <-> ( A ~<_ ( ~P A i^i dom card ) /\ -. A ~~ ( ~P A i^i dom card ) ) )
28 14 26 27 sylanbrc 
 |-  ( A e. V -> A ~< ( ~P A i^i dom card ) )