This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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ω ( 𝐵 , 𝐷 ) )