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 ⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) “ ω ) )
noseq.2 ⊢ ( 𝜑 → 𝐴 ∈ No )
noseqp1.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑍 )
Assertion noseqp1 ( 𝜑 → ( 𝐵 +s 1s ) ∈ 𝑍 )

Proof

Step Hyp Ref Expression
1 noseq.1 ⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) “ ω ) )
2 noseq.2 ⊢ ( 𝜑 → 𝐴 ∈ No )
3 noseqp1.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑍 )
4 3 1 eleqtrd ⊢ ( 𝜑 → 𝐵 ∈ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) “ ω ) )
5 df-ima ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) “ ω ) = ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω )
6 4 5 eleqtrdi ⊢ ( 𝜑 → 𝐵 ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) )
7 frfnom ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) Fn ω
8 fvelrnb ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) Fn ω → ( 𝐵 ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ↔ ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) = 𝐵 ) )
9 7 8 ax-mp ⊢ ( 𝐵 ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ↔ ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) = 𝐵 )
10 6 9 sylib ⊢ ( 𝜑 → ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) = 𝐵 )
11 ovex ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) +s 1s ) ∈ V
12 eqid ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω )
13 oveq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 +s 1s ) = ( 𝑥 +s 1s ) )
14 oveq1 ⊢ ( 𝑧 = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) → ( 𝑧 +s 1s ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) +s 1s ) )
15 12 13 14 frsucmpt2 ⊢ ( ( 𝑦 ∈ ω ∧ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) +s 1s ) ∈ V ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ suc 𝑦 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) +s 1s ) )
16 11 15 mpan2 ⊢ ( 𝑦 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ suc 𝑦 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) +s 1s ) )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ suc 𝑦 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) +s 1s ) )
18 peano2 ⊢ ( 𝑦 ∈ ω → suc 𝑦 ∈ ω )
19 fnfvelrn ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) Fn ω ∧ suc 𝑦 ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ suc 𝑦 ) ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) )
20 7 18 19 sylancr ⊢ ( 𝑦 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ suc 𝑦 ) ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ suc 𝑦 ) ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) )
22 1 5 eqtrdi ⊢ ( 𝜑 → 𝑍 = ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ω ) → 𝑍 = ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) )
24 21 23 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ suc 𝑦 ) ∈ 𝑍 )
25 17 24 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ω ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) +s 1s ) ∈ 𝑍 )
26 oveq1 ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) = 𝐵 → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) +s 1s ) = ( 𝐵 +s 1s ) )
27 26 eleq1d ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) = 𝐵 → ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) +s 1s ) ∈ 𝑍 ↔ ( 𝐵 +s 1s ) ∈ 𝑍 ) )
28 25 27 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ω ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) = 𝐵 → ( 𝐵 +s 1s ) ∈ 𝑍 ) )
29 28 impr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ω ∧ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) ↾ ω ) ‘ 𝑦 ) = 𝐵 ) ) → ( 𝐵 +s 1s ) ∈ 𝑍 )
30 10 29 rexlimddv ⊢ ( 𝜑 → ( 𝐵 +s 1s ) ∈ 𝑍 )