Metamath Proof Explorer

Theorem om2noseqoi

Description: An alternative definition of G in terms of df-oi . (Contributed by Scott Fenton, 18-Apr-2025)

Ref Expression
Hypotheses om2noseq.1 ⊢ φ → C ∈ No
om2noseq.2 ⊢ φ → G = rec ⁡ x ∈ V ⟼ x + s 1 s C ↾ ω
om2noseq.3 ⊢ φ → Z = rec ⁡ x ∈ V ⟼ x + s 1 s C ω
Assertion om2noseqoi ⊢ φ → G = OrdIso < s Z

Proof

Step Hyp Ref Expression
1 om2noseq.1 ⊢ φ → C ∈ No
2 om2noseq.2 ⊢ φ → G = rec ⁡ x ∈ V ⟼ x + s 1 s C ↾ ω
3 om2noseq.3 ⊢ φ → Z = rec ⁡ x ∈ V ⟼ x + s 1 s C ω
4 1 2 3 om2noseqiso ⊢ φ → G Isom E , < s ω Z
5 ordom ⊢ Ord ⁡ ω
6 4 5 jctil ⊢ φ → Ord ⁡ ω ∧ G Isom E , < s ω Z
7 ordwe ⊢ Ord ⁡ ω → E We ω
8 5 7 ax-mp ⊢ E We ω
9 isowe ⊢ G Isom E , < s ω Z → E We ω ↔ < s We Z
10 4 9 syl ⊢ φ → E We ω ↔ < s We Z
11 8 10 mpbii ⊢ φ → < s We Z
12 3 noseqex ⊢ φ → Z ∈ V
13 exse ⊢ Z ∈ V → < s Se Z
14 12 13 syl ⊢ φ → < s Se Z
15 eqid ⊢ OrdIso < s Z = OrdIso < s Z
16 15 oieu ⊢ < s We Z ∧ < s Se Z → Ord ⁡ ω ∧ G Isom E , < s ω Z ↔ ω = dom ⁡ OrdIso < s Z ∧ G = OrdIso < s Z
17 11 14 16 syl2anc ⊢ φ → Ord ⁡ ω ∧ G Isom E , < s ω Z ↔ ω = dom ⁡ OrdIso < s Z ∧ G = OrdIso < s Z
18 6 17 mpbid ⊢ φ → ω = dom ⁡ OrdIso < s Z ∧ G = OrdIso < s Z
19 18 simprd ⊢ φ → G = OrdIso < s Z