| Step |
Hyp |
Ref |
Expression |
| 1 |
|
infpssrlem.a |
|- ( ph -> B C_ A ) |
| 2 |
|
infpssrlem.c |
|- ( ph -> F : B -1-1-onto-> A ) |
| 3 |
|
infpssrlem.d |
|- ( ph -> C e. ( A \ B ) ) |
| 4 |
|
infpssrlem.e |
|- G = ( rec ( `' F , C ) |` _om ) |
| 5 |
|
frsuc |
|- ( M e. _om -> ( ( rec ( `' F , C ) |` _om ) ` suc M ) = ( `' F ` ( ( rec ( `' F , C ) |` _om ) ` M ) ) ) |
| 6 |
4
|
fveq1i |
|- ( G ` suc M ) = ( ( rec ( `' F , C ) |` _om ) ` suc M ) |
| 7 |
4
|
fveq1i |
|- ( G ` M ) = ( ( rec ( `' F , C ) |` _om ) ` M ) |
| 8 |
7
|
fveq2i |
|- ( `' F ` ( G ` M ) ) = ( `' F ` ( ( rec ( `' F , C ) |` _om ) ` M ) ) |
| 9 |
5 6 8
|
3eqtr4g |
|- ( M e. _om -> ( G ` suc M ) = ( `' F ` ( G ` M ) ) ) |