Description: The set of positive integers (as a subset of complex numbers) is equinumerous to omega (the set of finite ordinal numbers). (Contributed by NM, 31-Jul-2004) (Revised by Mario Carneiro, 15-Sep-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nnenom | |- NN ~~ _om |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | omex | |- _om e. _V |
|
| 2 | nn0ex | |- NN0 e. _V |
|
| 3 | eqid | |- ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) |
|
| 4 | 3 | hashgf1o | |- ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) : _om -1-1-onto-> NN0 |
| 5 | f1oen2g | |- ( ( _om e. _V /\ NN0 e. _V /\ ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) : _om -1-1-onto-> NN0 ) -> _om ~~ NN0 ) |
|
| 6 | 1 2 4 5 | mp3an | |- _om ~~ NN0 |
| 7 | nn0ennn | |- NN0 ~~ NN |
|
| 8 | 6 7 | entr2i | |- NN ~~ _om |