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 oveq2 
 |-  ( n = k -> ( A ^m n ) = ( A ^m k ) )
9 8 cbviunv 
 |-  U_ n e. _om ( A ^m n ) = U_ k e. _om ( A ^m k )
10 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 ) ) )
11 9 10 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 ) )
12 11 bilani 
 |-  ( ( ( ( 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 ) )
13 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 )
14 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 )
15 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 ) )
16 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 ) )
17 sseq2 
 |-  ( b = w -> ( _om C_ b <-> _om C_ w ) )
18 fveq2 
 |-  ( b = w -> ( m ` b ) = ( m ` w ) )
19 18 f1oeq1d 
 |-  ( b = w -> ( ( m ` b ) : ( b X. b ) -1-1-onto-> b <-> ( m ` w ) : ( b X. b ) -1-1-onto-> b ) )
20 xpeq12 
 |-  ( ( b = w /\ b = w ) -> ( b X. b ) = ( w X. w ) )
21 20 anidms 
 |-  ( b = w -> ( b X. b ) = ( w X. w ) )
22 21 f1oeq2d 
 |-  ( b = w -> ( ( m ` w ) : ( b X. b ) -1-1-onto-> b <-> ( m ` w ) : ( w X. w ) -1-1-onto-> b ) )
23 f1oeq3 
 |-  ( b = w -> ( ( m ` w ) : ( w X. w ) -1-1-onto-> b <-> ( m ` w ) : ( w X. w ) -1-1-onto-> w ) )
24 19 22 23 3bitrd 
 |-  ( b = w -> ( ( m ` b ) : ( b X. b ) -1-1-onto-> b <-> ( m ` w ) : ( w X. w ) -1-1-onto-> w ) )
25 17 24 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 ) ) )
26 25 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 ) )
27 16 26 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 ) )
28 eqid 
 |-  OrdIso ( r , u ) = OrdIso ( r , u )
29 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 ) >. )
30 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 ) >. ) )
31 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 ) ` (/) ) >. } )
32 oveq2 
 |-  ( n = k -> ( u ^m n ) = ( u ^m k ) )
33 32 cbviunv 
 |-  U_ n e. _om ( u ^m n ) = U_ k e. _om ( u ^m k )
34 33 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 ) >. )
35 eqid 
 |-  ( x e. _om , y e. u |-> <. ( OrdIso ( r , u ) ` x ) , y >. ) = ( x e. _om , y e. u |-> <. ( OrdIso ( r , u ) ` x ) , y >. )
36 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 ) >. ) )
37 12 13 14 15 27 28 29 30 31 34 35 36 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 ) )
38 37 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 ) )
39 38 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 ) )
40 brdomi 
 |-  ( ~P A ~<_ U_ n e. _om ( A ^m n ) -> E. g g : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
41 39 40 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 ) )
42 41 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 ) ) )
43 42 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 ) ) )
44 7 43 mpi 
 |-  ( ( h : _om -1-1-onto-> t /\ t C_ A ) -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) )
45 44 ex 
 |-  ( h : _om -1-1-onto-> t -> ( t C_ A -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) ) )
46 45 exlimiv 
 |-  ( E. h h : _om -1-1-onto-> t -> ( t C_ A -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) ) )
47 4 46 sylbi 
 |-  ( _om ~~ t -> ( t C_ A -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) ) )
48 47 imp 
 |-  ( ( _om ~~ t /\ t C_ A ) -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) )
49 48 exlimiv 
 |-  ( E. t ( _om ~~ t /\ t C_ A ) -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) )
50 3 49 biimtrdi 
 |-  ( A e. _V -> ( _om ~<_ A -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) ) )
51 2 50 mpcom 
 |-  ( _om ~<_ A -> -. ~P A ~<_ U_ n e. _om ( A ^m n ) )