This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ 𝐶 ∈ ℤ
	om2uz.2	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
Assertion	om2uz0i	⊢ ( 𝐺 ‘ ∅ ) = 𝐶

Proof

Step	Hyp	Ref	Expression
1		om2uz.1	⊢ 𝐶 ∈ ℤ
2		om2uz.2	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
3	2	fveq1i	⊢ ( 𝐺 ‘ ∅ ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω ) ‘ ∅ )
4		fr0g	⊢ ( 𝐶 ∈ ℤ → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω ) ‘ ∅ ) = 𝐶 )
5	1 4	ax-mp	⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω ) ‘ ∅ ) = 𝐶
6	3 5	eqtri	⊢ ( 𝐺 ‘ ∅ ) = 𝐶