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 ) )