Metamath Proof Explorer


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