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 )