Metamath Proof Explorer

Theorem seqseq123d

Description: Equality deduction for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025)

		Ref	Expression
	Hypotheses	seqseq123d.1	$⊢ φ \to M = N$
		seqseq123d.2	$⊢ φ \to \underset{˙}{+} = Q$
		seqseq123d.3	$⊢ φ \to F = G$
	Assertion	seqseq123d	$⊢ φ \to {seq}_{s} M (\underset{˙}{+}, F) = {seq}_{s} N (Q, G)$

Proof

Step	Hyp	Ref	Expression
1		seqseq123d.1	$⊢ φ \to M = N$
2		seqseq123d.2	$⊢ φ \to \underset{˙}{+} = Q$
3		seqseq123d.3	$⊢ φ \to F = G$
4	2	oveqd	$⊢ φ \to y \underset{˙}{+} F (x +_{s} 1_{s}) = y Q F (x +_{s} 1_{s})$
5	3	fveq1d	$⊢ φ \to F (x +_{s} 1_{s}) = G (x +_{s} 1_{s})$
6	5	oveq2d	$⊢ φ \to y Q F (x +_{s} 1_{s}) = y Q G (x +_{s} 1_{s})$
7	4 6	eqtrd	$⊢ φ \to y \underset{˙}{+} F (x +_{s} 1_{s}) = y Q G (x +_{s} 1_{s})$
8	7	opeq2d	$⊢ φ \to ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩ = ⟨x +_{s} 1_{s}, y Q G (x +_{s} 1_{s})⟩$
9	8	mpoeq3dv	$⊢ φ \to (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩) = (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y Q G (x +_{s} 1_{s})⟩)$
10	3 1	fveq12d	$⊢ φ \to F (M) = G (N)$
11	1 10	opeq12d	$⊢ φ \to ⟨M, F (M)⟩ = ⟨N, G (N)⟩$
12		rdgeq12	$⊢ ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩) = (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y Q G (x +_{s} 1_{s})⟩) \land ⟨M, F (M)⟩ = ⟨N, G (N)⟩) \to rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩), ⟨M, F (M)⟩) = rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y Q G (x +_{s} 1_{s})⟩), ⟨N, G (N)⟩)$
13	9 11 12	syl2anc	$⊢ φ \to rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩), ⟨M, F (M)⟩) = rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y Q G (x +_{s} 1_{s})⟩), ⟨N, G (N)⟩)$
14	13	imaeq1d	$⊢ φ \to rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩), ⟨M, F (M)⟩) [ω] = rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y Q G (x +_{s} 1_{s})⟩), ⟨N, G (N)⟩) [ω]$
15		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)⟩) [ω]$
16		df-seqs	$⊢ {seq}_{s} N (Q, G) = rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y Q G (x +_{s} 1_{s})⟩), ⟨N, G (N)⟩) [ω]$
17	14 15 16	3eqtr4g	$⊢ φ \to {seq}_{s} M (\underset{˙}{+}, F) = {seq}_{s} N (Q, G)$