Metamath Proof Explorer


Theorem wrecseq123

Description: General equality theorem for the well-ordered recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018) (Proof shortened by Scott Fenton, 17-Nov-2024)

Ref Expression
Assertion wrecseq123 ( ( 𝑅 = 𝑆𝐴 = 𝐵𝐹 = 𝐺 ) → wrecs ( 𝑅 , 𝐴 , 𝐹 ) = wrecs ( 𝑆 , 𝐵 , 𝐺 ) )

Proof

Step Hyp Ref Expression
1 coeq1 ( 𝐹 = 𝐺 → ( 𝐹 ∘ 2nd ) = ( 𝐺 ∘ 2nd ) )
2 frecseq123 ( ( 𝑅 = 𝑆𝐴 = 𝐵 ∧ ( 𝐹 ∘ 2nd ) = ( 𝐺 ∘ 2nd ) ) → frecs ( 𝑅 , 𝐴 , ( 𝐹 ∘ 2nd ) ) = frecs ( 𝑆 , 𝐵 , ( 𝐺 ∘ 2nd ) ) )
3 1 2 syl3an3 ( ( 𝑅 = 𝑆𝐴 = 𝐵𝐹 = 𝐺 ) → frecs ( 𝑅 , 𝐴 , ( 𝐹 ∘ 2nd ) ) = frecs ( 𝑆 , 𝐵 , ( 𝐺 ∘ 2nd ) ) )
4 df-wrecs wrecs ( 𝑅 , 𝐴 , 𝐹 ) = frecs ( 𝑅 , 𝐴 , ( 𝐹 ∘ 2nd ) )
5 df-wrecs wrecs ( 𝑆 , 𝐵 , 𝐺 ) = frecs ( 𝑆 , 𝐵 , ( 𝐺 ∘ 2nd ) )
6 3 4 5 3eqtr4g ( ( 𝑅 = 𝑆𝐴 = 𝐵𝐹 = 𝐺 ) → wrecs ( 𝑅 , 𝐴 , 𝐹 ) = wrecs ( 𝑆 , 𝐵 , 𝐺 ) )