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

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

Proof

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