Metamath Proof Explorer

Theorem om2noseqsuc

Description: The value of G at a successor. (Contributed by Scott Fenton, 18-Apr-2025)

Ref Expression
Hypotheses om2noseq.1 
|- ( ph -> C e. No )
om2noseq.2 
|- ( ph -> G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
om2noseqsuc.3 
|- ( ph -> A e. _om )
Assertion om2noseqsuc 
|- ( ph -> ( G ` suc A ) = ( ( G ` A ) +s 1s ) )

Proof

Step Hyp Ref Expression
1 om2noseq.1 
 |-  ( ph -> C e. No )
2 om2noseq.2 
 |-  ( ph -> G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
3 om2noseqsuc.3 
 |-  ( ph -> A e. _om )
4 ovex 
 |-  ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) ` A ) +s 1s ) e. _V
5 eqid 
 |-  ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om )
6 oveq1 
 |-  ( y = x -> ( y +s 1s ) = ( x +s 1s ) )
7 oveq1 
 |-  ( y = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) ` A ) -> ( y +s 1s ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) ` A ) +s 1s ) )
8 5 6 7 frsucmpt2 
 |-  ( ( A e. _om /\ ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) ` A ) +s 1s ) e. _V ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) ` suc A ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) ` A ) +s 1s ) )
9 3 4 8 sylancl 
 |-  ( ph -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) ` suc A ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) ` A ) +s 1s ) )
10 2 fveq1d 
 |-  ( ph -> ( G ` suc A ) = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) ` suc A ) )
11 2 fveq1d 
 |-  ( ph -> ( G ` A ) = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) ` A ) )
12 11 oveq1d 
 |-  ( ph -> ( ( G ` A ) +s 1s ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) ` A ) +s 1s ) )
13 9 10 12 3eqtr4d 
 |-  ( ph -> ( G ` suc A ) = ( ( G ` A ) +s 1s ) )