Theorem infpssrlem2

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	infpssrlem2	|- ( M e. _om -> ( G ` suc M ) = ( `' F ` ( G ` M ) ) )

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