Metamath Proof Explorer


Theorem canthp1

Description: A slightly stronger form of Cantor's theorem: For 1 < n , n + 1 < 2 ^ n . Corollary 1.6 of KanamoriPincus p. 417. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion canthp1
|- ( 1o ~< A -> ( A |_| 1o ) ~< ~P A )

Proof

Step Hyp Ref Expression
1 1sdom2
 |-  1o ~< 2o
2 sdomdom
 |-  ( 1o ~< 2o -> 1o ~<_ 2o )
3 1 2 ax-mp
 |-  1o ~<_ 2o
4 relsdom
 |-  Rel ~<
5 4 brrelex2i
 |-  ( 1o ~< A -> A e. _V )
6 djudom2
 |-  ( ( 1o ~<_ 2o /\ A e. _V ) -> ( A |_| 1o ) ~<_ ( A |_| 2o ) )
7 3 5 6 sylancr
 |-  ( 1o ~< A -> ( A |_| 1o ) ~<_ ( A |_| 2o ) )
8 canthp1lem1
 |-  ( 1o ~< A -> ( A |_| 2o ) ~<_ ~P A )
9 domtr
 |-  ( ( ( A |_| 1o ) ~<_ ( A |_| 2o ) /\ ( A |_| 2o ) ~<_ ~P A ) -> ( A |_| 1o ) ~<_ ~P A )
10 7 8 9 syl2anc
 |-  ( 1o ~< A -> ( A |_| 1o ) ~<_ ~P A )
11 fal
 |-  -. F.
12 ensym
 |-  ( ( A |_| 1o ) ~~ ~P A -> ~P A ~~ ( A |_| 1o ) )
13 bren
 |-  ( ~P A ~~ ( A |_| 1o ) <-> E. f f : ~P A -1-1-onto-> ( A |_| 1o ) )
14 12 13 sylib
 |-  ( ( A |_| 1o ) ~~ ~P A -> E. f f : ~P A -1-1-onto-> ( A |_| 1o ) )
15 f1of
 |-  ( f : ~P A -1-1-onto-> ( A |_| 1o ) -> f : ~P A --> ( A |_| 1o ) )
16 pwidg
 |-  ( A e. _V -> A e. ~P A )
17 5 16 syl
 |-  ( 1o ~< A -> A e. ~P A )
18 ffvelrn
 |-  ( ( f : ~P A --> ( A |_| 1o ) /\ A e. ~P A ) -> ( f ` A ) e. ( A |_| 1o ) )
19 15 17 18 syl2anr
 |-  ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) -> ( f ` A ) e. ( A |_| 1o ) )
20 dju1dif
 |-  ( ( A e. _V /\ ( f ` A ) e. ( A |_| 1o ) ) -> ( ( A |_| 1o ) \ { ( f ` A ) } ) ~~ A )
21 5 19 20 syl2an2r
 |-  ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) -> ( ( A |_| 1o ) \ { ( f ` A ) } ) ~~ A )
22 bren
 |-  ( ( ( A |_| 1o ) \ { ( f ` A ) } ) ~~ A <-> E. g g : ( ( A |_| 1o ) \ { ( f ` A ) } ) -1-1-onto-> A )
23 21 22 sylib
 |-  ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) -> E. g g : ( ( A |_| 1o ) \ { ( f ` A ) } ) -1-1-onto-> A )
24 simpll
 |-  ( ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) /\ g : ( ( A |_| 1o ) \ { ( f ` A ) } ) -1-1-onto-> A ) -> 1o ~< A )
25 simplr
 |-  ( ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) /\ g : ( ( A |_| 1o ) \ { ( f ` A ) } ) -1-1-onto-> A ) -> f : ~P A -1-1-onto-> ( A |_| 1o ) )
26 simpr
 |-  ( ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) /\ g : ( ( A |_| 1o ) \ { ( f ` A ) } ) -1-1-onto-> A ) -> g : ( ( A |_| 1o ) \ { ( f ` A ) } ) -1-1-onto-> A )
27 eqeq1
 |-  ( w = x -> ( w = A <-> x = A ) )
28 id
 |-  ( w = x -> w = x )
29 27 28 ifbieq2d
 |-  ( w = x -> if ( w = A , (/) , w ) = if ( x = A , (/) , x ) )
30 29 cbvmptv
 |-  ( w e. ~P A |-> if ( w = A , (/) , w ) ) = ( x e. ~P A |-> if ( x = A , (/) , x ) )
31 30 coeq2i
 |-  ( ( g o. f ) o. ( w e. ~P A |-> if ( w = A , (/) , w ) ) ) = ( ( g o. f ) o. ( x e. ~P A |-> if ( x = A , (/) , x ) ) )
32 eqid
 |-  { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( ( ( g o. f ) o. ( w e. ~P A |-> if ( w = A , (/) , w ) ) ) ` ( `' s " { z } ) ) = z ) ) } = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( ( ( g o. f ) o. ( w e. ~P A |-> if ( w = A , (/) , w ) ) ) ` ( `' s " { z } ) ) = z ) ) }
33 32 fpwwecbv
 |-  { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( ( ( g o. f ) o. ( w e. ~P A |-> if ( w = A , (/) , w ) ) ) ` ( `' s " { z } ) ) = z ) ) } = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( ( ( g o. f ) o. ( w e. ~P A |-> if ( w = A , (/) , w ) ) ) ` ( `' r " { y } ) ) = y ) ) }
34 eqid
 |-  U. dom { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( ( ( g o. f ) o. ( w e. ~P A |-> if ( w = A , (/) , w ) ) ) ` ( `' s " { z } ) ) = z ) ) } = U. dom { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( ( ( g o. f ) o. ( w e. ~P A |-> if ( w = A , (/) , w ) ) ) ` ( `' s " { z } ) ) = z ) ) }
35 24 25 26 31 33 34 canthp1lem2
 |-  -. ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) /\ g : ( ( A |_| 1o ) \ { ( f ` A ) } ) -1-1-onto-> A )
36 35 pm2.21i
 |-  ( ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) /\ g : ( ( A |_| 1o ) \ { ( f ` A ) } ) -1-1-onto-> A ) -> F. )
37 23 36 exlimddv
 |-  ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) -> F. )
38 37 ex
 |-  ( 1o ~< A -> ( f : ~P A -1-1-onto-> ( A |_| 1o ) -> F. ) )
39 38 exlimdv
 |-  ( 1o ~< A -> ( E. f f : ~P A -1-1-onto-> ( A |_| 1o ) -> F. ) )
40 14 39 syl5
 |-  ( 1o ~< A -> ( ( A |_| 1o ) ~~ ~P A -> F. ) )
41 11 40 mtoi
 |-  ( 1o ~< A -> -. ( A |_| 1o ) ~~ ~P A )
42 brsdom
 |-  ( ( A |_| 1o ) ~< ~P A <-> ( ( A |_| 1o ) ~<_ ~P A /\ -. ( A |_| 1o ) ~~ ~P A ) )
43 10 41 42 sylanbrc
 |-  ( 1o ~< A -> ( A |_| 1o ) ~< ~P A )