Theorem nfwrecs

Description: Bound-variable hypothesis builder for the well-founded 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 )