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