Metamath Proof Explorer


Theorem nfwrecs

Description: Bound-variable hypothesis builder for the well-ordered recursive function generator. (Contributed by Scott Fenton, 9-Jun-2018) (Proof shortened by Scott Fenton, 17-Nov-2024)

Ref Expression
Hypotheses nfwrecs.1 𝑥 𝑅
nfwrecs.2 𝑥 𝐴
nfwrecs.3 𝑥 𝐹
Assertion nfwrecs 𝑥 wrecs ( 𝑅 , 𝐴 , 𝐹 )

Proof

Step Hyp Ref Expression
1 nfwrecs.1 𝑥 𝑅
2 nfwrecs.2 𝑥 𝐴
3 nfwrecs.3 𝑥 𝐹
4 df-wrecs wrecs ( 𝑅 , 𝐴 , 𝐹 ) = frecs ( 𝑅 , 𝐴 , ( 𝐹 ∘ 2nd ) )
5 nfcv 𝑥 2nd
6 3 5 nfco 𝑥 ( 𝐹 ∘ 2nd )
7 1 2 6 nffrecs 𝑥 frecs ( 𝑅 , 𝐴 , ( 𝐹 ∘ 2nd ) )
8 4 7 nfcxfr 𝑥 wrecs ( 𝑅 , 𝐴 , 𝐹 )