Step |
Hyp |
Ref |
Expression |
1 |
|
tfrALT.1 |
|- F = recs ( G ) |
2 |
|
epweon |
|- _E We On |
3 |
|
epse |
|- _E Se On |
4 |
|
df-recs |
|- recs ( G ) = wrecs ( _E , On , G ) |
5 |
1 4
|
eqtri |
|- F = wrecs ( _E , On , G ) |
6 |
2 3 5
|
wfr2 |
|- ( A e. On -> ( F ` A ) = ( G ` ( F |` Pred ( _E , On , A ) ) ) ) |
7 |
|
predon |
|- ( A e. On -> Pred ( _E , On , A ) = A ) |
8 |
7
|
reseq2d |
|- ( A e. On -> ( F |` Pred ( _E , On , A ) ) = ( F |` A ) ) |
9 |
8
|
fveq2d |
|- ( A e. On -> ( G ` ( F |` Pred ( _E , On , A ) ) ) = ( G ` ( F |` A ) ) ) |
10 |
6 9
|
eqtrd |
|- ( A e. On -> ( F ` A ) = ( G ` ( F |` A ) ) ) |