Theorem seqomeq12

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

	Ref	Expression
Assertion	seqomeq12	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) → seqω ( 𝐴 , 𝐶 ) = seqω ( 𝐵 , 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq	⊢ ( 𝐴 = 𝐵 → ( 𝑎 𝐴 𝑏 ) = ( 𝑎 𝐵 𝑏 ) )
2	1	opeq2d	⊢ ( 𝐴 = 𝐵 → ⟨ suc 𝑎 , ( 𝑎 𝐴 𝑏 ) ⟩ = ⟨ suc 𝑎 , ( 𝑎 𝐵 𝑏 ) ⟩ )
3	2	mpoeq3dv	⊢ ( 𝐴 = 𝐵 → ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐴 𝑏 ) ⟩ ) = ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐵 𝑏 ) ⟩ ) )
4		fveq2	⊢ ( 𝐶 = 𝐷 → ( I ‘ 𝐶 ) = ( I ‘ 𝐷 ) )
5	4	opeq2d	⊢ ( 𝐶 = 𝐷 → ⟨ ∅ , ( I ‘ 𝐶 ) ⟩ = ⟨ ∅ , ( I ‘ 𝐷 ) ⟩ )
6		rdgeq12	⊢ ( ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐴 𝑏 ) ⟩ ) = ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐵 𝑏 ) ⟩ ) ∧ ⟨ ∅ , ( I ‘ 𝐶 ) ⟩ = ⟨ ∅ , ( I ‘ 𝐷 ) ⟩ ) → rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐴 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐶 ) ⟩ ) = rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐵 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐷 ) ⟩ ) )
7	3 5 6	syl2an	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) → rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐴 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐶 ) ⟩ ) = rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐵 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐷 ) ⟩ ) )
8	7	imaeq1d	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) → ( rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐴 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐶 ) ⟩ ) “ ω ) = ( rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐵 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐷 ) ⟩ ) “ ω ) )
9		df-seqom	⊢ seqω ( 𝐴 , 𝐶 ) = ( rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐴 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐶 ) ⟩ ) “ ω )
10		df-seqom	⊢ seqω ( 𝐵 , 𝐷 ) = ( rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐵 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐷 ) ⟩ ) “ ω )
11	8 9 10	3eqtr4g	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) → seqω ( 𝐴 , 𝐶 ) = seqω ( 𝐵 , 𝐷 ) )