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

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	⊢ ( 𝐹 = 𝐺 → ( 𝐹 ∘ 2^nd ) = ( 𝐺 ∘ 2^nd ) )
2		frecseq123	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ ( 𝐹 ∘ 2^nd ) = ( 𝐺 ∘ 2^nd ) ) → frecs ( 𝑅 , 𝐴 , ( 𝐹 ∘ 2^nd ) ) = frecs ( 𝑆 , 𝐵 , ( 𝐺 ∘ 2^nd ) ) )
3	1 2	syl3an3	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → frecs ( 𝑅 , 𝐴 , ( 𝐹 ∘ 2^nd ) ) = frecs ( 𝑆 , 𝐵 , ( 𝐺 ∘ 2^nd ) ) )
4		df-wrecs	⊢ wrecs ( 𝑅 , 𝐴 , 𝐹 ) = frecs ( 𝑅 , 𝐴 , ( 𝐹 ∘ 2^nd ) )
5		df-wrecs	⊢ wrecs ( 𝑆 , 𝐵 , 𝐺 ) = frecs ( 𝑆 , 𝐵 , ( 𝐺 ∘ 2^nd ) )
6	3 4 5	3eqtr4g	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → wrecs ( 𝑅 , 𝐴 , 𝐹 ) = wrecs ( 𝑆 , 𝐵 , 𝐺 ) )