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
|- F/_ x R
nfwrecs.2
|- F/_ x A
nfwrecs.3
|- F/_ x F
Assertion nfwrecs
|- F/_ x wrecs ( R , A , F )

Proof

Step Hyp Ref Expression
1 nfwrecs.1
 |-  F/_ x R
2 nfwrecs.2
 |-  F/_ x A
3 nfwrecs.3
 |-  F/_ x F
4 df-wrecs
 |-  wrecs ( R , A , F ) = U. { f | E. y ( f Fn y /\ ( y C_ A /\ A. z e. y Pred ( R , A , z ) C_ y ) /\ A. z e. y ( f ` z ) = ( F ` ( f |` Pred ( R , A , z ) ) ) ) }
5 nfv
 |-  F/ x f Fn y
6 nfcv
 |-  F/_ x y
7 6 2 nfss
 |-  F/ x y C_ A
8 nfcv
 |-  F/_ x z
9 1 2 8 nfpred
 |-  F/_ x Pred ( R , A , z )
10 9 6 nfss
 |-  F/ x Pred ( R , A , z ) C_ y
11 6 10 nfralw
 |-  F/ x A. z e. y Pred ( R , A , z ) C_ y
12 7 11 nfan
 |-  F/ x ( y C_ A /\ A. z e. y Pred ( R , A , z ) C_ y )
13 nfcv
 |-  F/_ x f
14 13 9 nfres
 |-  F/_ x ( f |` Pred ( R , A , z ) )
15 3 14 nffv
 |-  F/_ x ( F ` ( f |` Pred ( R , A , z ) ) )
16 15 nfeq2
 |-  F/ x ( f ` z ) = ( F ` ( f |` Pred ( R , A , z ) ) )
17 6 16 nfralw
 |-  F/ x A. z e. y ( f ` z ) = ( F ` ( f |` Pred ( R , A , z ) ) )
18 5 12 17 nf3an
 |-  F/ x ( f Fn y /\ ( y C_ A /\ A. z e. y Pred ( R , A , z ) C_ y ) /\ A. z e. y ( f ` z ) = ( F ` ( f |` Pred ( R , A , z ) ) ) )
19 18 nfex
 |-  F/ x E. y ( f Fn y /\ ( y C_ A /\ A. z e. y Pred ( R , A , z ) C_ y ) /\ A. z e. y ( f ` z ) = ( F ` ( f |` Pred ( R , A , z ) ) ) )
20 19 nfab
 |-  F/_ x { f | E. y ( f Fn y /\ ( y C_ A /\ A. z e. y Pred ( R , A , z ) C_ y ) /\ A. z e. y ( f ` z ) = ( F ` ( f |` Pred ( R , A , z ) ) ) ) }
21 20 nfuni
 |-  F/_ x U. { f | E. y ( f Fn y /\ ( y C_ A /\ A. z e. y Pred ( R , A , z ) C_ y ) /\ A. z e. y ( f ` z ) = ( F ` ( f |` Pred ( R , A , z ) ) ) ) }
22 4 21 nfcxfr
 |-  F/_ x wrecs ( R , A , F )