Description: Lemma for infpssr . (Contributed by Stefan O'Rear, 30-Oct-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | infpssrlem.a | |- ( ph -> B C_ A ) |
|
infpssrlem.c | |- ( ph -> F : B -1-1-onto-> A ) |
||
infpssrlem.d | |- ( ph -> C e. ( A \ B ) ) |
||
infpssrlem.e | |- G = ( rec ( `' F , C ) |` _om ) |
||
Assertion | infpssrlem1 | |- ( ph -> ( G ` (/) ) = C ) |
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 | 4 | fveq1i | |- ( G ` (/) ) = ( ( rec ( `' F , C ) |` _om ) ` (/) ) |
6 | fr0g | |- ( C e. ( A \ B ) -> ( ( rec ( `' F , C ) |` _om ) ` (/) ) = C ) |
|
7 | 3 6 | syl | |- ( ph -> ( ( rec ( `' F , C ) |` _om ) ` (/) ) = C ) |
8 | 5 7 | eqtrid | |- ( ph -> ( G ` (/) ) = C ) |