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	syl5eq	|- ( ph -> ( G ` (/) ) = C )