Metamath Proof Explorer


Theorem nfwrecs

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

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 = f | y f Fn y y A z y Pred R A z y z y f z = F f Pred R A z
5 nfv x f Fn y
6 nfcv _ x y
7 6 2 nfss x y A
8 nfcv _ x z
9 1 2 8 nfpred _ x Pred R A z
10 9 6 nfss x Pred R A z y
11 6 10 nfralw x z y Pred R A z y
12 7 11 nfan x y A z y Pred R A z y
13 nfcv _ x f
14 13 9 nfres _ x f Pred R A z
15 3 14 nffv _ x F f Pred R A z
16 15 nfeq2 x f z = F f Pred R A z
17 6 16 nfralw x z y f z = F f Pred R A z
18 5 12 17 nf3an x f Fn y y A z y Pred R A z y z y f z = F f Pred R A z
19 18 nfex x y f Fn y y A z y Pred R A z y z y f z = F f Pred R A z
20 19 nfab _ x f | y f Fn y y A z y Pred R A z y z y f z = F f Pred R A z
21 20 nfuni _ x f | y f Fn y y A z y Pred R A z y z y f z = F f Pred R A z
22 4 21 nfcxfr _ x wrecs R A F