Metamath Proof Explorer

Theorem seqsval

Description: The value of the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025)

		Ref	Expression
	Hypothesis	seqsval.1	$⊢ φ \to R = {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)⟩) ↾}_{ω}$
	Assertion	seqsval	$⊢ φ \to {seq}_{s} M (\underset{˙}{+}, F) = ran R$

Proof

Step	Hyp	Ref	Expression
1		seqsval.1	$⊢ φ \to R = {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)⟩) ↾}_{ω}$
2		df-seqs	$⊢ {seq}_{s} M (\underset{˙}{+}, F) = rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩), ⟨M, F (M)⟩) [ω]$
3		eqid	$⊢ V = V$
4		fvoveq1	$⊢ z = x \to F (z +_{s} 1_{s}) = F (x +_{s} 1_{s})$
5	4	oveq2d	$⊢ z = x \to w \underset{˙}{+} F (z +_{s} 1_{s}) = w \underset{˙}{+} F (x +_{s} 1_{s})$
6		oveq1	$⊢ w = y \to w \underset{˙}{+} F (x +_{s} 1_{s}) = y \underset{˙}{+} F (x +_{s} 1_{s})$
7		eqid	$⊢ (z \in V, w \in V ⟼ w \underset{˙}{+} F (z +_{s} 1_{s})) = (z \in V, w \in V ⟼ w \underset{˙}{+} F (z +_{s} 1_{s}))$
8		ovex	$⊢ y \underset{˙}{+} F (x +_{s} 1_{s}) \in V$
9	5 6 7 8	ovmpo	$⊢ (x \in V \land y \in V) \to x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z +_{s} 1_{s})) y = y \underset{˙}{+} F (x +_{s} 1_{s})$
10	9	el2v	$⊢ x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z +_{s} 1_{s})) y = y \underset{˙}{+} F (x +_{s} 1_{s})$
11	10	opeq2i	$⊢ ⟨x +_{s} 1_{s}, x (z \in V, w \in V ⟼ w \underset{˙}{+} F (z +_{s} 1_{s})) y⟩ = ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩$
12	3 3 11	mpoeq123i	$⊢ (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⟩) = (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩)$
13		rdgeq1	$⊢ (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⟩) = (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩) \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}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩), ⟨M, F (M)⟩)$
14	12 13	ax-mp	$⊢ 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}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩), ⟨M, F (M)⟩)$
15	14	imaeq1i	$⊢ 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}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩), ⟨M, F (M)⟩) [ω]$
16		df-ima	$⊢ 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)⟩) [ω] = 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)⟩) ↾}_{ω})$
17	2 15 16	3eqtr2i	$⊢ {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)⟩) ↾}_{ω})$
18	1	rneqd	$⊢ φ \to ran R = 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)⟩) ↾}_{ω})$
19	17 18	eqtr4id	$⊢ φ \to {seq}_{s} M (\underset{˙}{+}, F) = ran R$