Metamath Proof Explorer

Theorem csbwrecsg

Description: Move class substitution in and out of the well-founded recursive function generator. (Contributed by ML, 25-Oct-2020) (Revised by Scott Fenton, 18-Nov-2024)

		Ref	Expression
	Assertion	csbwrecsg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ wrecs ( 𝑅 , 𝐷 , 𝐹 ) = wrecs ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		csbfrecsg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ frecs ( 𝑅 , 𝐷 , ( 𝐹 ∘ 2^nd ) ) = frecs ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ∘ 2^nd ) ) )
2		eqid	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 = ⦋ 𝐴 / 𝑥 ⦌ 𝑅
3		eqid	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 = ⦋ 𝐴 / 𝑥 ⦌ 𝐷
4		csbcog	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ∘ 2^nd ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ ⦋ 𝐴 / 𝑥 ⦌ 2^nd ) )
5		csbconstg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 2^nd = 2^nd )
6	5	coeq2d	⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ ⦋ 𝐴 / 𝑥 ⦌ 2^nd ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ 2^nd ) )
7	4 6	eqtrd	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ∘ 2^nd ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ 2^nd ) )
8		frecseq123	⊢ ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 = ⦋ 𝐴 / 𝑥 ⦌ 𝑅 ∧ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 = ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ∘ 2^nd ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ 2^nd ) ) → frecs ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ∘ 2^nd ) ) = frecs ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ 2^nd ) ) )
9	2 3 7 8	mp3an12i	⊢ ( 𝐴 ∈ 𝑉 → frecs ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ∘ 2^nd ) ) = frecs ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ 2^nd ) ) )
10	1 9	eqtrd	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ frecs ( 𝑅 , 𝐷 , ( 𝐹 ∘ 2^nd ) ) = frecs ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ 2^nd ) ) )
11		df-wrecs	⊢ wrecs ( 𝑅 , 𝐷 , 𝐹 ) = frecs ( 𝑅 , 𝐷 , ( 𝐹 ∘ 2^nd ) )
12	11	csbeq2i	⊢ ⦋ 𝐴 / 𝑥 ⦌ wrecs ( 𝑅 , 𝐷 , 𝐹 ) = ⦋ 𝐴 / 𝑥 ⦌ frecs ( 𝑅 , 𝐷 , ( 𝐹 ∘ 2^nd ) )
13		df-wrecs	⊢ wrecs ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) = frecs ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ∘ 2^nd ) )
14	10 12 13	3eqtr4g	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ wrecs ( 𝑅 , 𝐷 , 𝐹 ) = wrecs ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )