Description: The mapping G is a one-to-one mapping from _om onto upper
integers that will be used to construct a recursive definition
generator. Ordinal natural number 0 maps to complex number C
(normally 0 for the upper integers NN0 or 1 for the upper integers
NN ), 1 maps to C + 1, etc. This theorem shows the value of
G at ordinal natural number zero. (This series of theorems
generalizes an earlier series for NN0 contributed by Raph Levien,
10-Apr-2004.) (Contributed by NM, 3-Oct-2004)(Revised by Mario
Carneiro, 13-Sep-2013)
Ref
Expression
Hypotheses
om2uz.1
|- C e. ZZ
om2uz.2
|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om )