Step |
Hyp |
Ref |
Expression |
1 |
|
wfr3.1 |
|- R We A |
2 |
|
wfr3.2 |
|- R Se A |
3 |
|
wfr3.3 |
|- F = wrecs ( R , A , G ) |
4 |
1 2
|
pm3.2i |
|- ( R We A /\ R Se A ) |
5 |
1 2 3
|
wfr1 |
|- F Fn A |
6 |
1 2 3
|
wfr2 |
|- ( z e. A -> ( F ` z ) = ( G ` ( F |` Pred ( R , A , z ) ) ) ) |
7 |
6
|
rgen |
|- A. z e. A ( F ` z ) = ( G ` ( F |` Pred ( R , A , z ) ) ) |
8 |
5 7
|
pm3.2i |
|- ( F Fn A /\ A. z e. A ( F ` z ) = ( G ` ( F |` Pred ( R , A , z ) ) ) ) |
9 |
|
wfr3g |
|- ( ( ( R We A /\ R Se A ) /\ ( F Fn A /\ A. z e. A ( F ` z ) = ( G ` ( F |` Pred ( R , A , z ) ) ) ) /\ ( H Fn A /\ A. z e. A ( H ` z ) = ( G ` ( H |` Pred ( R , A , z ) ) ) ) ) -> F = H ) |
10 |
4 8 9
|
mp3an12 |
|- ( ( H Fn A /\ A. z e. A ( H ` z ) = ( G ` ( H |` Pred ( R , A , z ) ) ) ) -> F = H ) |