seqsfn

Description: The surreal sequence builder is a function. (Contributed by Scott Fenton, 19-Apr-2025)

Step	Hyp	Ref	Expression
1		seqsfn.1	$⊢ φ \to M \in No$
2		seqsfn.2	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), M) [ω]$
3		eqidd	$⊢ φ \to {rec ((y \in V ⟼ y +_{s} 1_{s}), M) ↾}_{ω} = {rec ((y \in V ⟼ y +_{s} 1_{s}), M) ↾}_{ω}$
4		oveq1	$⊢ x = y \to x +_{s} 1_{s} = y +_{s} 1_{s}$
5	4	cbvmptv	$⊢ (x \in V ⟼ x +_{s} 1_{s}) = (y \in V ⟼ y +_{s} 1_{s})$
6		rdgeq1	$⊢ (x \in V ⟼ x +_{s} 1_{s}) = (y \in V ⟼ y +_{s} 1_{s}) \to rec ((x \in V ⟼ x +_{s} 1_{s}), M) = rec ((y \in V ⟼ y +_{s} 1_{s}), M)$
7	5 6	ax-mp	$⊢ rec ((x \in V ⟼ x +_{s} 1_{s}), M) = rec ((y \in V ⟼ y +_{s} 1_{s}), M)$
8	7	imaeq1i	$⊢ rec ((x \in V ⟼ x +_{s} 1_{s}), M) [ω] = rec ((y \in V ⟼ y +_{s} 1_{s}), M) [ω]$
9	2 8	eqtrdi	$⊢ φ \to Z = rec ((y \in V ⟼ y +_{s} 1_{s}), M) [ω]$
10		fvexd	$⊢ φ \to F (M) \in V$
11		eqidd	$⊢ φ \to {rec ((y \in V, z \in V ⟼ ⟨y +_{s} 1_{s}, y (w \in V, t \in V ⟼ t \underset{˙}{+} F (w +_{s} 1_{s})) z⟩), ⟨M, F (M)⟩) ↾}_{ω} = {rec ((y \in V, z \in V ⟼ ⟨y +_{s} 1_{s}, y (w \in V, t \in V ⟼ t \underset{˙}{+} F (w +_{s} 1_{s})) z⟩), ⟨M, F (M)⟩) ↾}_{ω}$
12	11	seqsval	$⊢ φ \to {seq}_{s} M (\underset{˙}{+}, F) = ran ({rec ((y \in V, z \in V ⟼ ⟨y +_{s} 1_{s}, y (w \in V, t \in V ⟼ t \underset{˙}{+} F (w +_{s} 1_{s})) z⟩), ⟨M, F (M)⟩) ↾}_{ω})$
13	1 3 9 10 11 12	noseqrdgfn	$⊢ φ \to {seq}_{s} M (\underset{˙}{+}, F) Fn Z$

Metamath Proof Explorer