Metamath Proof Explorer

Theorem om2uz0i

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 ∈ ℤ
om2uz.2 ⊢ G = rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω
Assertion om2uz0i ⊢ G ⁡ ∅ = C

Proof

Step Hyp Ref Expression
1 om2uz.1 ⊢ C ∈ ℤ
2 om2uz.2 ⊢ G = rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω
3 2 fveq1i ⊢ G ⁡ ∅ = rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω ⁡ ∅
4 fr0g ⊢ C ∈ ℤ → rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω ⁡ ∅ = C
5 1 4 ax-mp ⊢ rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω ⁡ ∅ = C
6 3 5 eqtri ⊢ G ⁡ ∅ = C