Metamath Proof Explorer

Theorem pwfseq

Description: The powerset of a Dedekind-infinite set does not inject into the set of finite sequences. The proof is due to Halbeisen and Shelah. Proposition 1.7 of KanamoriPincus p. 418. (Contributed by Mario Carneiro, 31-May-2015)

Ref Expression
Assertion pwfseq 
|- ( _om ~<_ A -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) )

Proof

Step Hyp Ref Expression
1 reldom 
 |-  Rel ~<_
2 1 brrelex2i 
 |-  ( _om ~<_ A -> A e. _V )
3 domeng 
 |-  ( A e. _V -> ( _om ~<_ A <-> E. t ( _om ~~ t /\ t C_ A ) ) )
4 bren 
 |-  ( _om ~~ t <-> E. h h : _om -1-1-onto-> t )
5 harcl 
 |-  ( har ` ~P A ) e. On
6 infxpenc2 
 |-  ( ( har ` ~P A ) e. On -> E. m A. b e. ( har ` ~P A ) ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b ) )
7 5 6 ax-mp 
 |-  E. m A. b e. ( har ` ~P A ) ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b )
8 simpr 
 |-  ( ( ( ( h : _om -1-1-onto-> t /\ t C_ A ) /\ A. b e. ( har ` ~P A ) ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b ) ) /\ g : ~P A -1-1-> U_ n e. _om ( A ^m n ) ) -> g : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
9 oveq2 
 |-  ( n = k -> ( A ^m n ) = ( A ^m k ) )
10 9 cbviunv 
 |-  U_ n e. _om ( A ^m n ) = U_ k e. _om ( A ^m k )
11 f1eq3 
 |-  ( U_ n e. _om ( A ^m n ) = U_ k e. _om ( A ^m k ) -> ( g : ~P A -1-1-> U_ n e. _om ( A ^m n ) <-> g : ~P A -1-1-> U_ k e. _om ( A ^m k ) ) )
12 10 11 ax-mp 
 |-  ( g : ~P A -1-1-> U_ n e. _om ( A ^m n ) <-> g : ~P A -1-1-> U_ k e. _om ( A ^m k ) )
13 8 12 sylib 
 |-  ( ( ( ( h : _om -1-1-onto-> t /\ t C_ A ) /\ A. b e. ( har ` ~P A ) ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b ) ) /\ g : ~P A -1-1-> U_ n e. _om ( A ^m n ) ) -> g : ~P A -1-1-> U_ k e. _om ( A ^m k ) )
14 simpllr 
 |-  ( ( ( ( h : _om -1-1-onto-> t /\ t C_ A ) /\ A. b e. ( har ` ~P A ) ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b ) ) /\ g : ~P A -1-1-> U_ n e. _om ( A ^m n ) ) -> t C_ A )
15 simplll 
 |-  ( ( ( ( h : _om -1-1-onto-> t /\ t C_ A ) /\ A. b e. ( har ` ~P A ) ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b ) ) /\ g : ~P A -1-1-> U_ n e. _om ( A ^m n ) ) -> h : _om -1-1-onto-> t )
16 biid 
 |-  ( ( ( u C_ A /\ r C_ ( u X. u ) /\ r We u ) /\ _om ~<_ u ) <-> ( ( u C_ A /\ r C_ ( u X. u ) /\ r We u ) /\ _om ~<_ u ) )
17 simplr 
 |-  ( ( ( ( h : _om -1-1-onto-> t /\ t C_ A ) /\ A. b e. ( har ` ~P A ) ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b ) ) /\ g : ~P A -1-1-> U_ n e. _om ( A ^m n ) ) -> A. b e. ( har ` ~P A ) ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b ) )
18 sseq2 
 |-  ( b = w -> ( _om C_ b <-> _om C_ w ) )
19 fveq2 
 |-  ( b = w -> ( m ` b ) = ( m ` w ) )
20 f1oeq1 
 |-  ( ( m ` b ) = ( m ` w ) -> ( ( m ` b ) : ( b X. b ) -1-1-onto-> b <-> ( m ` w ) : ( b X. b ) -1-1-onto-> b ) )
21 19 20 syl 
 |-  ( b = w -> ( ( m ` b ) : ( b X. b ) -1-1-onto-> b <-> ( m ` w ) : ( b X. b ) -1-1-onto-> b ) )
22 xpeq12 
 |-  ( ( b = w /\ b = w ) -> ( b X. b ) = ( w X. w ) )
23 22 anidms 
 |-  ( b = w -> ( b X. b ) = ( w X. w ) )
24 23 f1oeq2d 
 |-  ( b = w -> ( ( m ` w ) : ( b X. b ) -1-1-onto-> b <-> ( m ` w ) : ( w X. w ) -1-1-onto-> b ) )
25 f1oeq3 
 |-  ( b = w -> ( ( m ` w ) : ( w X. w ) -1-1-onto-> b <-> ( m ` w ) : ( w X. w ) -1-1-onto-> w ) )
26 21 24 25 3bitrd 
 |-  ( b = w -> ( ( m ` b ) : ( b X. b ) -1-1-onto-> b <-> ( m ` w ) : ( w X. w ) -1-1-onto-> w ) )
27 18 26 imbi12d 
 |-  ( b = w -> ( ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b ) <-> ( _om C_ w -> ( m ` w ) : ( w X. w ) -1-1-onto-> w ) ) )
28 27 cbvralvw 
 |-  ( A. b e. ( har ` ~P A ) ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b ) <-> A. w e. ( har ` ~P A ) ( _om C_ w -> ( m ` w ) : ( w X. w ) -1-1-onto-> w ) )
29 17 28 sylib 
 |-  ( ( ( ( h : _om -1-1-onto-> t /\ t C_ A ) /\ A. b e. ( har ` ~P A ) ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b ) ) /\ g : ~P A -1-1-> U_ n e. _om ( A ^m n ) ) -> A. w e. ( har ` ~P A ) ( _om C_ w -> ( m ` w ) : ( w X. w ) -1-1-onto-> w ) )
30 eqid 
 |-  OrdIso ( r , u ) = OrdIso ( r , u )
31 eqid 
 |-  ( s e. dom OrdIso ( r , u ) , z e. dom OrdIso ( r , u ) |-> <. ( OrdIso ( r , u ) ` s ) , ( OrdIso ( r , u ) ` z ) >. ) = ( s e. dom OrdIso ( r , u ) , z e. dom OrdIso ( r , u ) |-> <. ( OrdIso ( r , u ) ` s ) , ( OrdIso ( r , u ) ` z ) >. )
32 eqid 
 |-  ( ( OrdIso ( r , u ) o. ( m ` dom OrdIso ( r , u ) ) ) o. `' ( s e. dom OrdIso ( r , u ) , z e. dom OrdIso ( r , u ) |-> <. ( OrdIso ( r , u ) ` s ) , ( OrdIso ( r , u ) ` z ) >. ) ) = ( ( OrdIso ( r , u ) o. ( m ` dom OrdIso ( r , u ) ) ) o. `' ( s e. dom OrdIso ( r , u ) , z e. dom OrdIso ( r , u ) |-> <. ( OrdIso ( r , u ) ` s ) , ( OrdIso ( r , u ) ` z ) >. ) )
33 eqid 
 |-  seqom ( ( p e. _V , f e. _V |-> ( x e. ( u ^m suc p ) |-> ( ( f ` ( x |` p ) ) ( ( OrdIso ( r , u ) o. ( m ` dom OrdIso ( r , u ) ) ) o. `' ( s e. dom OrdIso ( r , u ) , z e. dom OrdIso ( r , u ) |-> <. ( OrdIso ( r , u ) ` s ) , ( OrdIso ( r , u ) ` z ) >. ) ) ( x ` p ) ) ) ) , { <. (/) , ( OrdIso ( r , u ) ` (/) ) >. } ) = seqom ( ( p e. _V , f e. _V |-> ( x e. ( u ^m suc p ) |-> ( ( f ` ( x |` p ) ) ( ( OrdIso ( r , u ) o. ( m ` dom OrdIso ( r , u ) ) ) o. `' ( s e. dom OrdIso ( r , u ) , z e. dom OrdIso ( r , u ) |-> <. ( OrdIso ( r , u ) ` s ) , ( OrdIso ( r , u ) ` z ) >. ) ) ( x ` p ) ) ) ) , { <. (/) , ( OrdIso ( r , u ) ` (/) ) >. } )
34 oveq2 
 |-  ( n = k -> ( u ^m n ) = ( u ^m k ) )
35 34 cbviunv 
 |-  U_ n e. _om ( u ^m n ) = U_ k e. _om ( u ^m k )
36 35 mpteq1i 
 |-  ( y e. U_ n e. _om ( u ^m n ) |-> <. dom y , ( ( seqom ( ( p e. _V , f e. _V |-> ( x e. ( u ^m suc p ) |-> ( ( f ` ( x |` p ) ) ( ( OrdIso ( r , u ) o. ( m ` dom OrdIso ( r , u ) ) ) o. `' ( s e. dom OrdIso ( r , u ) , z e. dom OrdIso ( r , u ) |-> <. ( OrdIso ( r , u ) ` s ) , ( OrdIso ( r , u ) ` z ) >. ) ) ( x ` p ) ) ) ) , { <. (/) , ( OrdIso ( r , u ) ` (/) ) >. } ) ` dom y ) ` y ) >. ) = ( y e. U_ k e. _om ( u ^m k ) |-> <. dom y , ( ( seqom ( ( p e. _V , f e. _V |-> ( x e. ( u ^m suc p ) |-> ( ( f ` ( x |` p ) ) ( ( OrdIso ( r , u ) o. ( m ` dom OrdIso ( r , u ) ) ) o. `' ( s e. dom OrdIso ( r , u ) , z e. dom OrdIso ( r , u ) |-> <. ( OrdIso ( r , u ) ` s ) , ( OrdIso ( r , u ) ` z ) >. ) ) ( x ` p ) ) ) ) , { <. (/) , ( OrdIso ( r , u ) ` (/) ) >. } ) ` dom y ) ` y ) >. )
37 eqid 
 |-  ( x e. _om , y e. u |-> <. ( OrdIso ( r , u ) ` x ) , y >. ) = ( x e. _om , y e. u |-> <. ( OrdIso ( r , u ) ` x ) , y >. )
38 eqid 
 |-  ( ( ( ( OrdIso ( r , u ) o. ( m ` dom OrdIso ( r , u ) ) ) o. `' ( s e. dom OrdIso ( r , u ) , z e. dom OrdIso ( r , u ) |-> <. ( OrdIso ( r , u ) ` s ) , ( OrdIso ( r , u ) ` z ) >. ) ) o. ( x e. _om , y e. u |-> <. ( OrdIso ( r , u ) ` x ) , y >. ) ) o. ( y e. U_ n e. _om ( u ^m n ) |-> <. dom y , ( ( seqom ( ( p e. _V , f e. _V |-> ( x e. ( u ^m suc p ) |-> ( ( f ` ( x |` p ) ) ( ( OrdIso ( r , u ) o. ( m ` dom OrdIso ( r , u ) ) ) o. `' ( s e. dom OrdIso ( r , u ) , z e. dom OrdIso ( r , u ) |-> <. ( OrdIso ( r , u ) ` s ) , ( OrdIso ( r , u ) ` z ) >. ) ) ( x ` p ) ) ) ) , { <. (/) , ( OrdIso ( r , u ) ` (/) ) >. } ) ` dom y ) ` y ) >. ) ) = ( ( ( ( OrdIso ( r , u ) o. ( m ` dom OrdIso ( r , u ) ) ) o. `' ( s e. dom OrdIso ( r , u ) , z e. dom OrdIso ( r , u ) |-> <. ( OrdIso ( r , u ) ` s ) , ( OrdIso ( r , u ) ` z ) >. ) ) o. ( x e. _om , y e. u |-> <. ( OrdIso ( r , u ) ` x ) , y >. ) ) o. ( y e. U_ n e. _om ( u ^m n ) |-> <. dom y , ( ( seqom ( ( p e. _V , f e. _V |-> ( x e. ( u ^m suc p ) |-> ( ( f ` ( x |` p ) ) ( ( OrdIso ( r , u ) o. ( m ` dom OrdIso ( r , u ) ) ) o. `' ( s e. dom OrdIso ( r , u ) , z e. dom OrdIso ( r , u ) |-> <. ( OrdIso ( r , u ) ` s ) , ( OrdIso ( r , u ) ` z ) >. ) ) ( x ` p ) ) ) ) , { <. (/) , ( OrdIso ( r , u ) ` (/) ) >. } ) ` dom y ) ` y ) >. ) )
39 13 14 15 16 29 30 31 32 33 36 37 38 pwfseqlem5 
 |-  -. ( ( ( h : _om -1-1-onto-> t /\ t C_ A ) /\ A. b e. ( har ` ~P A ) ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b ) ) /\ g : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
40 39 imnani 
 |-  ( ( ( h : _om -1-1-onto-> t /\ t C_ A ) /\ A. b e. ( har ` ~P A ) ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b ) ) -> -. g : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
41 40 nexdv 
 |-  ( ( ( h : _om -1-1-onto-> t /\ t C_ A ) /\ A. b e. ( har ` ~P A ) ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b ) ) -> -. E. g g : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
42 brdomi 
 |-  ( ~P A ~<_ U_ n e. _om ( A ^m n ) -> E. g g : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
43 41 42 nsyl 
 |-  ( ( ( h : _om -1-1-onto-> t /\ t C_ A ) /\ A. b e. ( har ` ~P A ) ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b ) ) -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) )
44 43 ex 
 |-  ( ( h : _om -1-1-onto-> t /\ t C_ A ) -> ( A. b e. ( har ` ~P A ) ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b ) -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) ) )
45 44 exlimdv 
 |-  ( ( h : _om -1-1-onto-> t /\ t C_ A ) -> ( E. m A. b e. ( har ` ~P A ) ( _om C_ b -> ( m ` b ) : ( b X. b ) -1-1-onto-> b ) -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) ) )
46 7 45 mpi 
 |-  ( ( h : _om -1-1-onto-> t /\ t C_ A ) -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) )
47 46 ex 
 |-  ( h : _om -1-1-onto-> t -> ( t C_ A -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) ) )
48 47 exlimiv 
 |-  ( E. h h : _om -1-1-onto-> t -> ( t C_ A -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) ) )
49 4 48 sylbi 
 |-  ( _om ~~ t -> ( t C_ A -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) ) )
50 49 imp 
 |-  ( ( _om ~~ t /\ t C_ A ) -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) )
51 50 exlimiv 
 |-  ( E. t ( _om ~~ t /\ t C_ A ) -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) )
52 3 51 syl6bi 
 |-  ( A e. _V -> ( _om ~<_ A -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) ) )
53 2 52 mpcom 
 |-  ( _om ~<_ A -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) )