Theorem nffrecs

Description: Bound-variable hypothesis builder for the well-founded recursion generator. (Contributed by Scott Fenton, 23-Dec-2021)

	Ref	Expression
Hypotheses	nffrecs.1	|- F/_ x R
	nffrecs.2	|- F/_ x A
	nffrecs.3	|- F/_ x F
Assertion	nffrecs	|- F/_ x frecs ( R , A , F )

Proof

Step	Hyp	Ref	Expression
1		nffrecs.1	|- F/_ x R
2		nffrecs.2	|- F/_ x A
3		nffrecs.3	|- F/_ x F
4		df-frecs	|- frecs ( 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 ) = ( 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	8 3 14	nfov	|- F/_ x ( z F ( f |` Pred ( R , A , z ) ) )
16	15	nfeq2	|- F/ x ( f ` z ) = ( z F ( f |` Pred ( R , A , z ) ) )
17	6 16	nfralw	|- F/ x A. z e. y ( f ` z ) = ( 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 ) = ( 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 ) = ( 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 ) = ( 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 ) = ( z F ( f |` Pred ( R , A , z ) ) ) ) }
22	4 21	nfcxfr	|- F/_ x frecs ( R , A , F )