seqs1

Description: The value of the surreal sequence builder function at its initial value. (Contributed by Scott Fenton, 19-Apr-2025)

		Ref	Expression
	Hypothesis	seqs1.1	$⊢ φ \to M \in No$
	Assertion	seqs1	$⊢ φ \to {seq}_{s} M (\underset{˙}{+}, F) (M) = F (M)$

Step	Hyp	Ref	Expression
1		seqs1.1	$⊢ φ \to M \in No$
2		eqidd	$⊢ φ \to {rec ((x \in V ⟼ x +_{s} 1_{s}), M) ↾}_{ω} = {rec ((x \in V ⟼ x +_{s} 1_{s}), M) ↾}_{ω}$
3		eqidd	$⊢ φ \to rec ((x \in V ⟼ x +_{s} 1_{s}), M) [ω] = rec ((x \in V ⟼ x +_{s} 1_{s}), M) [ω]$
4		fvexd	$⊢ φ \to F (M) \in V$
5		eqidd	$⊢ φ \to {rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z +_{s} 1_{s})) y⟩), ⟨M, F (M)⟩) ↾}_{ω} = {rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z +_{s} 1_{s})) y⟩), ⟨M, F (M)⟩) ↾}_{ω}$
6	5	seqsval	$⊢ φ \to {seq}_{s} M (\underset{˙}{+}, F) = ran ({rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z +_{s} 1_{s})) y⟩), ⟨M, F (M)⟩) ↾}_{ω})$
7	1 2 3 4 5 6	noseqrdg0	$⊢ φ \to {seq}_{s} M (\underset{˙}{+}, F) (M) = F (M)$

Metamath Proof Explorer