Metamath Proof Explorer

Theorem om2noseqiso

Description: G is an isomorphism from the finite ordinals to a surreal sequence. (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 om2noseqiso ⊢ φ → G Isom E , < 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 om2noseqf1o ⊢ φ → G : ω ⟶ 1-1 onto Z
5 epel ⊢ y E z ↔ y ∈ z
6 1 2 3 om2noseqlt2 ⊢ φ ∧ y ∈ ω ∧ z ∈ ω → y ∈ z ↔ G ⁡ y < s G ⁡ z
7 5 6 bitrid ⊢ φ ∧ y ∈ ω ∧ z ∈ ω → y E z ↔ G ⁡ y < s G ⁡ z
8 7 ralrimivva ⊢ φ → ∀ y ∈ ω ∀ z ∈ ω y E z ↔ G ⁡ y < s G ⁡ z
9 df-isom ⊢ G Isom E , < s ω Z ↔ G : ω ⟶ 1-1 onto Z ∧ ∀ y ∈ ω ∀ z ∈ ω y E z ↔ G ⁡ y < s G ⁡ z
10 4 8 9 sylanbrc ⊢ φ → G Isom E , < s ω Z