seqeq1

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

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

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

Metamath Proof Explorer