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 ⊢ C ∈ ℤ
om2uz.2 ⊢ G = rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω
Assertion om2uzisoi ⊢ G Isom E , < ω ℤ ≥ C

Proof

Step Hyp Ref Expression
1 om2uz.1 ⊢ C ∈ ℤ
2 om2uz.2 ⊢ G = rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω
3 1 2 om2uzf1oi ⊢ G : ω ⟶ 1-1 onto ℤ ≥ C
4 epel ⊢ y E z ↔ y ∈ z
5 1 2 om2uzlt2i ⊢ y ∈ ω ∧ z ∈ ω → y ∈ z ↔ G ⁡ y < G ⁡ z
6 4 5 bitrid ⊢ y ∈ ω ∧ z ∈ ω → y E z ↔ G ⁡ y < G ⁡ z
7 6 rgen2 ⊢ ∀ y ∈ ω ∀ z ∈ ω y E z ↔ G ⁡ y < G ⁡ z
8 df-isom ⊢ G Isom E , < ω ℤ ≥ C ↔ G : ω ⟶ 1-1 onto ℤ ≥ C ∧ ∀ y ∈ ω ∀ z ∈ ω y E z ↔ G ⁡ y < G ⁡ z
9 3 7 8 mpbir2an ⊢ G Isom E , < ω ℤ ≥ C