Theorem nnenom 13937

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.)

Assertion

Ref	Expression
nnenom	⊢ ℕ ≈ ω

Proof of Theorem nnenom

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		omex 9559	. . 3 ⊢ ω ∈ V
2		nn0ex 12438	. . 3 ⊢ ℕ0 ∈ V
3		eqid 2741	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
4	3	hashgf1o 13928	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
5		f1oen2g 8909	. . 3 ⊢ ((ω ∈ V ∧ ℕ0 ∈ V ∧ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0) → ω ≈ ℕ0)
6	1, 2, 4, 5	mp3an 1470	. 2 ⊢ ω ≈ ℕ0
7		nn0ennn 13936	. 2 ⊢ ℕ0 ≈ ℕ
8	6, 7	entr2i 8950	1 ⊢ ℕ ≈ ω

Syntax hints:   ∈ wcel 2121  Vcvv 3433   class class class wbr 5074   ↦ cmpt 5155   ↾ cres 5622  –1-1-onto→wf1o 6487  (class class class)co 7359  ωcom 7809  reccrdg 8342   ≈ cen 8884  0cc0 11034  1c1 11035   + caddc 11037  ℕcn 12169  ℕ₀cn0 12432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7681  ax-inf2 9557  ax-cnex 11090  ax-resscn 11091  ax-1cn 11092  ax-icn 11093  ax-addcl 11094  ax-addrcl 11095  ax-mulcl 11096  ax-mulrcl 11097  ax-mulcom 11098  ax-addass 11099  ax-mulass 11100  ax-distr 11101  ax-i2m1 11102  ax-1ne0 11103  ax-1rid 11104  ax-rnegex 11105  ax-rrecex 11106  ax-cnre 11107  ax-pre-lttri 11108  ax-pre-lttrn 11109  ax-pre-ltadd 11110  ax-pre-mulgt0 11111

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3725  df-csb 3833  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3904  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-tr 5182  df-id 5515  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6255  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-riota 7316  df-ov 7362  df-oprab 7363  df-mpo 7364  df-om 7810  df-2nd 7934  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8343  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11177  df-mnf 11178  df-xr 11179  df-ltxr 11180  df-le 11181  df-sub 11375  df-neg 11376  df-nn 12170  df-n0 12433  df-z 12520  df-uz 12784

This theorem is referenced by:  nnct  13938  supcvg  15816  xpnnen  16173  znnen  16174  qnnen  16175  rexpen  16190  aleph1re  16207  aleph1irr  16208  bitsf1  16410  unben  16875  odinf  19532  odhash  19543  cygctb  19861  1stcfb  23431  2ndcredom  23436  1stcelcls  23447  hauspwdom  23487  met1stc  24507  met2ndci  24508  re2ndc  24787  iscmet3  25281  ovolctb2  25480  ovolfi  25482  ovoliunlem3  25492  iunmbl2  25545  uniiccdif  25566  dyadmbl  25588  opnmblALT  25591  mbfimaopnlem  25643  itg2seq  25730  aannenlem3  26317  dirith2  27512  nmounbseqi  30868  nmobndseqi  30870  minvecolem5  30972  padct  32812  f1ocnt  32894  dmvlsiga  34323  sigapildsys  34356  volmeas  34425  omssubadd  34494  carsgclctunlem3  34514  poimirlem30  38030  poimirlem32  38032  mblfinlem1  38037  ovoliunnfl  38042  heiborlem3  38193  heibor  38201  lzenom  43232  fiphp3d  43277  irrapx1  43286  pellex  43293  nnfoctb  45509  zenom  45513  qenom  45818  ioonct  45994  subsaliuncl  46813  caragenunicl  46979  caratheodory  46983  ovnsubaddlem2  47026