Metamath Proof Explorer

Theorem om2uzoi

Description: An alternative definition of G in terms of df-oi . (Contributed by Mario Carneiro, 2-Jun-2015)

Ref Expression
Hypotheses om2uz.1 ⊢ C ∈ ℤ
om2uz.2 ⊢ G = rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω
Assertion om2uzoi ⊢ G = OrdIso < ℤ ≥ C

Proof

Step Hyp Ref Expression
1 om2uz.1 ⊢ C ∈ ℤ
2 om2uz.2 ⊢ G = rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω
3 ordom ⊢ Ord ⁡ ω
4 1 2 om2uzisoi ⊢ G Isom E , < ω ℤ ≥ C
5 3 4 pm3.2i ⊢ Ord ⁡ ω ∧ G Isom E , < ω ℤ ≥ C
6 ordwe ⊢ Ord ⁡ ω → E We ω
7 3 6 ax-mp ⊢ E We ω
8 isowe ⊢ G Isom E , < ω ℤ ≥ C → E We ω ↔ < We ℤ ≥ C
9 4 8 ax-mp ⊢ E We ω ↔ < We ℤ ≥ C
10 7 9 mpbi ⊢ < We ℤ ≥ C
11 fvex ⊢ ℤ ≥ C ∈ V
12 exse ⊢ ℤ ≥ C ∈ V → < Se ℤ ≥ C
13 11 12 ax-mp ⊢ < Se ℤ ≥ C
14 eqid ⊢ OrdIso < ℤ ≥ C = OrdIso < ℤ ≥ C
15 14 oieu ⊢ < We ℤ ≥ C ∧ < Se ℤ ≥ C → Ord ⁡ ω ∧ G Isom E , < ω ℤ ≥ C ↔ ω = dom ⁡ OrdIso < ℤ ≥ C ∧ G = OrdIso < ℤ ≥ C
16 10 13 15 mp2an ⊢ Ord ⁡ ω ∧ G Isom E , < ω ℤ ≥ C ↔ ω = dom ⁡ OrdIso < ℤ ≥ C ∧ G = OrdIso < ℤ ≥ C
17 5 16 mpbi ⊢ ω = dom ⁡ OrdIso < ℤ ≥ C ∧ G = OrdIso < ℤ ≥ C
18 17 simpri ⊢ G = OrdIso < ℤ ≥ C