This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )