Metamath Proof Explorer


Theorem infpssrlem1

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 )

Proof

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 )