Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Well-ordered recursion
nfwrecs
Metamath Proof Explorer
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
⊢ Ⅎ _ x R
nfwrecs.2
⊢ Ⅎ _ x A
nfwrecs.3
⊢ Ⅎ _ x F
Assertion
nfwrecs
⊢ Ⅎ _ x wrecs ⁡ R A F
Proof
Step
Hyp
Ref
Expression
1
nfwrecs.1
⊢ Ⅎ _ x R
2
nfwrecs.2
⊢ Ⅎ _ x A
3
nfwrecs.3
⊢ Ⅎ _ x F
4
df-wrecs
⊢ wrecs ⁡ R A F = frecs ⁡ R A F ∘ 2 nd
5
nfcv
⊢ Ⅎ _ x 2 nd
6
3 5
nfco
⊢ Ⅎ _ x F ∘ 2 nd
7
1 2 6
nffrecs
⊢ Ⅎ _ x frecs ⁡ R A F ∘ 2 nd
8
4 7
nfcxfr
⊢ Ⅎ _ x wrecs ⁡ R A F