Metamath Proof Explorer

Theorem seqeq3

Description: Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013)

		Ref	Expression
	Assertion	seqeq3	$⊢ F = G \to seq M (\underset{˙}{+}, F) = seq M (\underset{˙}{+}, G)$

Proof

Step	Hyp	Ref	Expression
1		fveq1	$⊢ F = G \to F (x + 1) = G (x + 1)$
2	1	oveq2d	$⊢ F = G \to y \underset{˙}{+} F (x + 1) = y \underset{˙}{+} G (x + 1)$
3	2	opeq2d	$⊢ F = G \to ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩ = ⟨x + 1, y \underset{˙}{+} G (x + 1)⟩$
4	3	mpoeq3dv	$⊢ F = G \to (x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩) = (x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} G (x + 1)⟩)$
5		fveq1	$⊢ F = G \to F (M) = G (M)$
6	5	opeq2d	$⊢ F = G \to ⟨M, F (M)⟩ = ⟨M, G (M)⟩$
7		rdgeq12	$⊢ ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩) = (x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} G (x + 1)⟩) \land ⟨M, F (M)⟩ = ⟨M, G (M)⟩) \to rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩) = rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} G (x + 1)⟩), ⟨M, G (M)⟩)$
8	4 6 7	syl2anc	$⊢ F = G \to rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩) = rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} G (x + 1)⟩), ⟨M, G (M)⟩)$
9	8	imaeq1d	$⊢ F = G \to rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩) [ω] = rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} G (x + 1)⟩), ⟨M, G (M)⟩) [ω]$
10		df-seq	$⊢ seq M (\underset{˙}{+}, F) = rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩) [ω]$
11		df-seq	$⊢ seq M (\underset{˙}{+}, G) = rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} G (x + 1)⟩), ⟨M, G (M)⟩) [ω]$
12	9 10 11	3eqtr4g	$⊢ F = G \to seq M (\underset{˙}{+}, F) = seq M (\underset{˙}{+}, G)$