Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  om2uz0i Unicode version

Theorem om2uz0i 11228
 Description: The mapping is a one-to-one mapping from onto upper integers that will be used to construct a recursive definition generator. Ordinal natural number 0 maps to complex number (normally 0 for the upper integers or 1 for the upper integers ), 1 maps to + 1, etc. This theorem shows the value of at ordinal natural number zero. (This series of theorems generalizes an earlier series for contributed by Raph Levien, 10-Apr-2004.) (Contributed by NM, 3-Oct-2004.) (Revised by Mario Carneiro, 13-Sep-2013.)
Hypotheses
Ref Expression
om2uz.1
om2uz.2
Assertion
Ref Expression
om2uz0i
Distinct variable group:   ,
Allowed substitution hint:   ()

Proof of Theorem om2uz0i
StepHypRef Expression
1 om2uz.2 . . 3
21fveq1i 5683 . 2
3 om2uz.1 . . 3
4 fr0g 6643 . . 3
53, 4ax-mp 8 . 2
62, 5eqtri 2421 1
 Colors of variables: wff set class Syntax hints:   wceq 1649   wcel 1721  cvv 2913  c0 3585   cmpt 4221  com 4799   cres 4834  cfv 5408  (class class class)co 6034  crdg 6617  c1 8938   caddc 8940  cz 10228 This theorem is referenced by:  om2uzuzi  11230  om2uzrani  11233  om2uzrdg  11237  uzrdgxfr  11247  fzennn  11248  axdc4uzlem  11262  hashgadd  11592 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-ral 2668  df-rex 2669  df-reu 2670  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-iun 4051  df-br 4168  df-opab 4222  df-mpt 4223  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-recs 6583  df-rdg 6618
 Copyright terms: Public domain W3C validator