seqomeq12

Description: Equality theorem for seqom . (Contributed by Stefan O'Rear, 1-Nov-2014)

		Ref	Expression
	Assertion	seqomeq12	$⊢ (A = B \land C = D) \to {seq}_{ω} (A, C) = {seq}_{ω} (B, D)$

Step	Hyp	Ref	Expression
1		oveq	$⊢ A = B \to a A b = a B b$
2	1	opeq2d	$⊢ A = B \to ⟨suc a, a A b⟩ = ⟨suc a, a B b⟩$
3	2	mpoeq3dv	$⊢ A = B \to (a \in ω, b \in V ⟼ ⟨suc a, a A b⟩) = (a \in ω, b \in V ⟼ ⟨suc a, a B b⟩)$
4		fveq2	$⊢ C = D \to I (C) = I (D)$
5	4	opeq2d	$⊢ C = D \to ⟨\emptyset, I (C)⟩ = ⟨\emptyset, I (D)⟩$
6		rdgeq12	$⊢ ((a \in ω, b \in V ⟼ ⟨suc a, a A b⟩) = (a \in ω, b \in V ⟼ ⟨suc a, a B b⟩) \land ⟨\emptyset, I (C)⟩ = ⟨\emptyset, I (D)⟩) \to rec ((a \in ω, b \in V ⟼ ⟨suc a, a A b⟩), ⟨\emptyset, I (C)⟩) = rec ((a \in ω, b \in V ⟼ ⟨suc a, a B b⟩), ⟨\emptyset, I (D)⟩)$
7	3 5 6	syl2an	$⊢ (A = B \land C = D) \to rec ((a \in ω, b \in V ⟼ ⟨suc a, a A b⟩), ⟨\emptyset, I (C)⟩) = rec ((a \in ω, b \in V ⟼ ⟨suc a, a B b⟩), ⟨\emptyset, I (D)⟩)$
8	7	imaeq1d	$⊢ (A = B \land C = D) \to rec ((a \in ω, b \in V ⟼ ⟨suc a, a A b⟩), ⟨\emptyset, I (C)⟩) [ω] = rec ((a \in ω, b \in V ⟼ ⟨suc a, a B b⟩), ⟨\emptyset, I (D)⟩) [ω]$
9		df-seqom	$⊢ {seq}_{ω} (A, C) = rec ((a \in ω, b \in V ⟼ ⟨suc a, a A b⟩), ⟨\emptyset, I (C)⟩) [ω]$
10		df-seqom	$⊢ {seq}_{ω} (B, D) = rec ((a \in ω, b \in V ⟼ ⟨suc a, a B b⟩), ⟨\emptyset, I (D)⟩) [ω]$
11	8 9 10	3eqtr4g	$⊢ (A = B \land C = D) \to {seq}_{ω} (A, C) = {seq}_{ω} (B, D)$

Metamath Proof Explorer