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 ) |