Metamath Proof Explorer

Theorem noseq0

Description: The surreal A is a member of the sequence starting at A . (Contributed by Scott Fenton, 18-Apr-2025)

Ref Expression
Hypotheses noseq.1 ⊢ φ → Z = rec ⁡ x ∈ V ⟼ x + s 1 s A ω
noseq.2 ⊢ φ → A ∈ No
Assertion noseq0 ⊢ φ → A ∈ Z

Proof

Step Hyp Ref Expression
1 noseq.1 ⊢ φ → Z = rec ⁡ x ∈ V ⟼ x + s 1 s A ω
2 noseq.2 ⊢ φ → A ∈ No
3 fr0g ⊢ A ∈ No → rec ⁡ x ∈ V ⟼ x + s 1 s A ↾ ω ⁡ ∅ = A
4 2 3 syl ⊢ φ → rec ⁡ x ∈ V ⟼ x + s 1 s A ↾ ω ⁡ ∅ = A
5 frfnom ⊢ rec ⁡ x ∈ V ⟼ x + s 1 s A ↾ ω Fn ω
6 peano1 ⊢ ∅ ∈ ω
7 fnfvelrn ⊢ rec ⁡ x ∈ V ⟼ x + s 1 s A ↾ ω Fn ω ∧ ∅ ∈ ω → rec ⁡ x ∈ V ⟼ x + s 1 s A ↾ ω ⁡ ∅ ∈ ran ⁡ rec ⁡ x ∈ V ⟼ x + s 1 s A ↾ ω
8 5 6 7 mp2an ⊢ rec ⁡ x ∈ V ⟼ x + s 1 s A ↾ ω ⁡ ∅ ∈ ran ⁡ rec ⁡ x ∈ V ⟼ x + s 1 s A ↾ ω
9 4 8 eqeltrrdi ⊢ φ → A ∈ ran ⁡ rec ⁡ x ∈ V ⟼ x + s 1 s A ↾ ω
10 df-ima ⊢ rec ⁡ x ∈ V ⟼ x + s 1 s A ω = ran ⁡ rec ⁡ x ∈ V ⟼ x + s 1 s A ↾ ω
11 1 10 eqtrdi ⊢ φ → Z = ran ⁡ rec ⁡ x ∈ V ⟼ x + s 1 s A ↾ ω
12 9 11 eleqtrrd ⊢ φ → A ∈ Z