Metamath Proof Explorer

Theorem noseqp1

Description: One plus an element of Z is an element of Z . (Contributed by Scott Fenton, 18-Apr-2025)

Ref Expression
Hypotheses noseq.1 
|- ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) " _om ) )
noseq.2 
|- ( ph -> A e. No )
noseqp1.3 
|- ( ph -> B e. Z )
Assertion noseqp1 
|- ( ph -> ( B +s 1s ) e. Z )

Proof

Step Hyp Ref Expression
1 noseq.1 
 |-  ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) " _om ) )
2 noseq.2 
 |-  ( ph -> A e. No )
3 noseqp1.3 
 |-  ( ph -> B e. Z )
4 3 1 eleqtrd 
 |-  ( ph -> B e. ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) " _om ) )
5 df-ima 
 |-  ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) " _om ) = ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om )
6 4 5 eleqtrdi 
 |-  ( ph -> B e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) )
7 frfnom 
 |-  ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) Fn _om
8 fvelrnb 
 |-  ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) Fn _om -> ( B e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) <-> E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) = B ) )
9 7 8 ax-mp 
 |-  ( B e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) <-> E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) = B )
10 6 9 sylib 
 |-  ( ph -> E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) = B )
11 ovex 
 |-  ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) +s 1s ) e. _V
12 eqid 
 |-  ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om )
13 oveq1 
 |-  ( z = x -> ( z +s 1s ) = ( x +s 1s ) )
14 oveq1 
 |-  ( z = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) -> ( z +s 1s ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) +s 1s ) )
15 12 13 14 frsucmpt2 
 |-  ( ( y e. _om /\ ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) +s 1s ) e. _V ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` suc y ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) +s 1s ) )
16 11 15 mpan2 
 |-  ( y e. _om -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` suc y ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) +s 1s ) )
17 16 adantl 
 |-  ( ( ph /\ y e. _om ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` suc y ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) +s 1s ) )
18 peano2 
 |-  ( y e. _om -> suc y e. _om )
19 fnfvelrn 
 |-  ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) Fn _om /\ suc y e. _om ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` suc y ) e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) )
20 7 18 19 sylancr 
 |-  ( y e. _om -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` suc y ) e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) )
21 20 adantl 
 |-  ( ( ph /\ y e. _om ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` suc y ) e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) )
22 1 5 eqtrdi 
 |-  ( ph -> Z = ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) )
23 22 adantr 
 |-  ( ( ph /\ y e. _om ) -> Z = ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) )
24 21 23 eleqtrrd 
 |-  ( ( ph /\ y e. _om ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` suc y ) e. Z )
25 17 24 eqeltrrd 
 |-  ( ( ph /\ y e. _om ) -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) +s 1s ) e. Z )
26 oveq1 
 |-  ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) = B -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) +s 1s ) = ( B +s 1s ) )
27 26 eleq1d 
 |-  ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) = B -> ( ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) +s 1s ) e. Z <-> ( B +s 1s ) e. Z ) )
28 25 27 syl5ibcom 
 |-  ( ( ph /\ y e. _om ) -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) = B -> ( B +s 1s ) e. Z ) )
29 28 impr 
 |-  ( ( ph /\ ( y e. _om /\ ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) |` _om ) ` y ) = B ) ) -> ( B +s 1s ) e. Z )
30 10 29 rexlimddv 
 |-  ( ph -> ( B +s 1s ) e. Z )