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

Metamath Proof Explorer

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 bitrid ⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( 𝑦 E 𝑧 ↔ ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑧 ) ) )
7 6 rgen2 ⊢ ∀ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ( 𝑦 E 𝑧 ↔ ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑧 ) )
8 df-isom ⊢ ( 𝐺 Isom E , < ( ω , ( ℤ≥ ‘ 𝐶 ) ) ↔ ( 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 𝐶 ) ∧ ∀ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ( 𝑦 E 𝑧 ↔ ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑧 ) ) ) )
9 3 7 8 mpbir2an ⊢ 𝐺 Isom E , < ( ω , ( ℤ≥ ‘ 𝐶 ) )