Theorem om2uzisoi

Description: G (see om2uz0i ) is an isomorphism from natural ordinals to upper integers. (Contributed by NM, 9-Oct-2008) (Revised by Mario Carneiro, 13-Sep-2013)

	Ref	Expression
Hypotheses	om2uz.1	⊢ 𝐶 ∈ ℤ
	om2uz.2	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
Assertion	om2uzisoi	⊢ 𝐺 Isom E , < ( ω , ( ℤ≥ ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		om2uz.1	⊢ 𝐶 ∈ ℤ
2		om2uz.2	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
3	1 2	om2uzf1oi	⊢ 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 𝐶 )
4		epel	⊢ ( 𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧 )
5	1 2	om2uzlt2i	⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( 𝑦 ∈ 𝑧 ↔ ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑧 ) ) )
6	4 5	syl5bb	⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( 𝑦 E 𝑧 ↔ ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑧 ) ) )
7	6	rgen2	⊢ ∀ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ( 𝑦 E 𝑧 ↔ ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑧 ) )
8		df-isom	⊢ ( 𝐺 Isom E , < ( ω , ( ℤ≥ ‘ 𝐶 ) ) ↔ ( 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 𝐶 ) ∧ ∀ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ( 𝑦 E 𝑧 ↔ ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑧 ) ) ) )
9	3 7 8	mpbir2an	⊢ 𝐺 Isom E , < ( ω , ( ℤ≥ ‘ 𝐶 ) )