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

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