seqeq2

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

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

Step	Hyp	Ref	Expression
1		oveq	$⊢ \underset{˙}{+} = Q \to y \underset{˙}{+} F (x + 1) = y Q F (x + 1)$
2	1	opeq2d	$⊢ \underset{˙}{+} = Q \to ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩ = ⟨x + 1, y Q F (x + 1)⟩$
3	2	mpoeq3dv	$⊢ \underset{˙}{+} = Q \to (x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩) = (x \in V, y \in V ⟼ ⟨x + 1, y Q F (x + 1)⟩)$
4		rdgeq1	$⊢ (x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩) = (x \in V, y \in V ⟼ ⟨x + 1, y Q F (x + 1)⟩) \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 Q F (x + 1)⟩), ⟨M, F (M)⟩)$
5	3 4	syl	$⊢ \underset{˙}{+} = Q \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 Q F (x + 1)⟩), ⟨M, F (M)⟩)$
6	5	imaeq1d	$⊢ \underset{˙}{+} = Q \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 Q F (x + 1)⟩), ⟨M, F (M)⟩) [ω]$
7		df-seq	$⊢ seq M (\underset{˙}{+}, F) = rec ((x \in V, y \in V ⟼ ⟨x + 1, y \underset{˙}{+} F (x + 1)⟩), ⟨M, F (M)⟩) [ω]$
8		df-seq	$⊢ seq M (Q, F) = rec ((x \in V, y \in V ⟼ ⟨x + 1, y Q F (x + 1)⟩), ⟨M, F (M)⟩) [ω]$
9	6 7 8	3eqtr4g	$⊢ \underset{˙}{+} = Q \to seq M (\underset{˙}{+}, F) = seq M (Q, F)$

Metamath Proof Explorer