Users' Mathboxes Mathbox for Jim Kingdon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  nnsf GIF version

Theorem nnsf 11364
Description: Domain and range of 𝑆. Part of Definition 3.3 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 30-Jul-2022.)
Hypothesis
Ref Expression
nns.s 𝑆 = (𝑝 ∈ ℕ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖))))
Assertion
Ref Expression
nnsf 𝑆:ℕ⟶ℕ
Distinct variable group:   𝑖,𝑝
Allowed substitution hints:   𝑆(𝑖,𝑝)

Proof of Theorem nnsf
Dummy variables 𝑓 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nns.s . 2 𝑆 = (𝑝 ∈ ℕ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖))))
2 1lt2o 11355 . . . . . . 7 1𝑜 ∈ 2𝑜
32a1i 9 . . . . . 6 ((𝑝 ∈ ℕ𝑖 ∈ ω) → 1𝑜 ∈ 2𝑜)
4 nninff 11363 . . . . . . . 8 (𝑝 ∈ ℕ𝑝:ω⟶2𝑜)
54adantr 270 . . . . . . 7 ((𝑝 ∈ ℕ𝑖 ∈ ω) → 𝑝:ω⟶2𝑜)
6 nnpredcl 11359 . . . . . . . 8 (𝑖 ∈ ω → 𝑖 ∈ ω)
76adantl 271 . . . . . . 7 ((𝑝 ∈ ℕ𝑖 ∈ ω) → 𝑖 ∈ ω)
85, 7ffvelrnd 5400 . . . . . 6 ((𝑝 ∈ ℕ𝑖 ∈ ω) → (𝑝 𝑖) ∈ 2𝑜)
9 nndceq0 4406 . . . . . . 7 (𝑖 ∈ ω → DECID 𝑖 = ∅)
109adantl 271 . . . . . 6 ((𝑝 ∈ ℕ𝑖 ∈ ω) → DECID 𝑖 = ∅)
113, 8, 10ifcldcd 3412 . . . . 5 ((𝑝 ∈ ℕ𝑖 ∈ ω) → if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)) ∈ 2𝑜)
12 eqid 2085 . . . . 5 (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖))) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))
1311, 12fmptd 5417 . . . 4 (𝑝 ∈ ℕ → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖))):ω⟶2𝑜)
14 2onn 6234 . . . . 5 2𝑜 ∈ ω
15 omex 4383 . . . . 5 ω ∈ V
16 elmapg 6372 . . . . 5 ((2𝑜 ∈ ω ∧ ω ∈ V) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖))) ∈ (2𝑜𝑚 ω) ↔ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖))):ω⟶2𝑜))
1714, 15, 16mp2an 417 . . . 4 ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖))) ∈ (2𝑜𝑚 ω) ↔ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖))):ω⟶2𝑜)
1813, 17sylibr 132 . . 3 (𝑝 ∈ ℕ → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖))) ∈ (2𝑜𝑚 ω))
19 1on 6144 . . . . . . . . 9 1𝑜 ∈ On
2019ontrci 4230 . . . . . . . 8 Tr 1𝑜
212a1i 9 . . . . . . . . . . 11 ((𝑝 ∈ ℕ𝑗 ∈ ω) → 1𝑜 ∈ 2𝑜)
224adantr 270 . . . . . . . . . . . 12 ((𝑝 ∈ ℕ𝑗 ∈ ω) → 𝑝:ω⟶2𝑜)
23 peano2 4385 . . . . . . . . . . . . . 14 (𝑗 ∈ ω → suc 𝑗 ∈ ω)
2423adantl 271 . . . . . . . . . . . . 13 ((𝑝 ∈ ℕ𝑗 ∈ ω) → suc 𝑗 ∈ ω)
25 nnpredcl 11359 . . . . . . . . . . . . 13 (suc 𝑗 ∈ ω → suc 𝑗 ∈ ω)
2624, 25syl 14 . . . . . . . . . . . 12 ((𝑝 ∈ ℕ𝑗 ∈ ω) → suc 𝑗 ∈ ω)
2722, 26ffvelrnd 5400 . . . . . . . . . . 11 ((𝑝 ∈ ℕ𝑗 ∈ ω) → (𝑝 suc 𝑗) ∈ 2𝑜)
28 nndceq0 4406 . . . . . . . . . . . 12 (suc 𝑗 ∈ ω → DECID suc 𝑗 = ∅)
2924, 28syl 14 . . . . . . . . . . 11 ((𝑝 ∈ ℕ𝑗 ∈ ω) → DECID suc 𝑗 = ∅)
3021, 27, 29ifcldcd 3412 . . . . . . . . . 10 ((𝑝 ∈ ℕ𝑗 ∈ ω) → if(suc 𝑗 = ∅, 1𝑜, (𝑝 suc 𝑗)) ∈ 2𝑜)
3130adantr 270 . . . . . . . . 9 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1𝑜, (𝑝 suc 𝑗)) ∈ 2𝑜)
32 df-2o 6138 . . . . . . . . 9 2𝑜 = suc 1𝑜
3331, 32syl6eleq 2177 . . . . . . . 8 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1𝑜, (𝑝 suc 𝑗)) ∈ suc 1𝑜)
34 trsucss 4226 . . . . . . . 8 (Tr 1𝑜 → (if(suc 𝑗 = ∅, 1𝑜, (𝑝 suc 𝑗)) ∈ suc 1𝑜 → if(suc 𝑗 = ∅, 1𝑜, (𝑝 suc 𝑗)) ⊆ 1𝑜))
3520, 33, 34mpsyl 64 . . . . . . 7 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1𝑜, (𝑝 suc 𝑗)) ⊆ 1𝑜)
36 iftrue 3384 . . . . . . . 8 (𝑗 = ∅ → if(𝑗 = ∅, 1𝑜, (𝑝 𝑗)) = 1𝑜)
3736adantl 271 . . . . . . 7 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(𝑗 = ∅, 1𝑜, (𝑝 𝑗)) = 1𝑜)
3835, 37sseqtr4d 3052 . . . . . 6 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1𝑜, (𝑝 suc 𝑗)) ⊆ if(𝑗 = ∅, 1𝑜, (𝑝 𝑗)))
39 simpr 108 . . . . . . . . . . . 12 ((𝑝 ∈ ℕ𝑗 ∈ ω) → 𝑗 ∈ ω)
4039adantr 270 . . . . . . . . . . 11 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → 𝑗 ∈ ω)
41 nnord 4401 . . . . . . . . . . 11 (𝑗 ∈ ω → Ord 𝑗)
42 ordtr 4181 . . . . . . . . . . 11 (Ord 𝑗 → Tr 𝑗)
4340, 41, 423syl 17 . . . . . . . . . 10 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → Tr 𝑗)
44 unisucg 4217 . . . . . . . . . . 11 (𝑗 ∈ ω → (Tr 𝑗 suc 𝑗 = 𝑗))
4540, 44syl 14 . . . . . . . . . 10 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (Tr 𝑗 suc 𝑗 = 𝑗))
4643, 45mpbid 145 . . . . . . . . 9 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → suc 𝑗 = 𝑗)
4746fveq2d 5274 . . . . . . . 8 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝 suc 𝑗) = (𝑝𝑗))
48 simpr 108 . . . . . . . . . . . 12 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → ¬ 𝑗 = ∅)
4948neqned 2258 . . . . . . . . . . 11 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → 𝑗 ≠ ∅)
50 nnsucpred 11360 . . . . . . . . . . 11 ((𝑗 ∈ ω ∧ 𝑗 ≠ ∅) → suc 𝑗 = 𝑗)
5140, 49, 50syl2anc 403 . . . . . . . . . 10 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → suc 𝑗 = 𝑗)
5251fveq2d 5274 . . . . . . . . 9 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝‘suc 𝑗) = (𝑝𝑗))
53 suceq 4205 . . . . . . . . . . . 12 (𝑘 = 𝑗 → suc 𝑘 = suc 𝑗)
5453fveq2d 5274 . . . . . . . . . . 11 (𝑘 = 𝑗 → (𝑝‘suc 𝑘) = (𝑝‘suc 𝑗))
55 fveq2 5270 . . . . . . . . . . 11 (𝑘 = 𝑗 → (𝑝𝑘) = (𝑝 𝑗))
5654, 55sseq12d 3044 . . . . . . . . . 10 (𝑘 = 𝑗 → ((𝑝‘suc 𝑘) ⊆ (𝑝𝑘) ↔ (𝑝‘suc 𝑗) ⊆ (𝑝 𝑗)))
57 fveq1 5269 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑝 → (𝑓‘suc 𝑗) = (𝑝‘suc 𝑗))
58 fveq1 5269 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑝 → (𝑓𝑗) = (𝑝𝑗))
5957, 58sseq12d 3044 . . . . . . . . . . . . . . 15 (𝑓 = 𝑝 → ((𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ (𝑝‘suc 𝑗) ⊆ (𝑝𝑗)))
6059ralbidv 2376 . . . . . . . . . . . . . 14 (𝑓 = 𝑝 → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ∀𝑗 ∈ ω (𝑝‘suc 𝑗) ⊆ (𝑝𝑗)))
61 df-nninf 6738 . . . . . . . . . . . . . 14 = {𝑓 ∈ (2𝑜𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗)}
6260, 61elrab2 2765 . . . . . . . . . . . . 13 (𝑝 ∈ ℕ ↔ (𝑝 ∈ (2𝑜𝑚 ω) ∧ ∀𝑗 ∈ ω (𝑝‘suc 𝑗) ⊆ (𝑝𝑗)))
6362simprbi 269 . . . . . . . . . . . 12 (𝑝 ∈ ℕ → ∀𝑗 ∈ ω (𝑝‘suc 𝑗) ⊆ (𝑝𝑗))
64 suceq 4205 . . . . . . . . . . . . . . 15 (𝑗 = 𝑘 → suc 𝑗 = suc 𝑘)
6564fveq2d 5274 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → (𝑝‘suc 𝑗) = (𝑝‘suc 𝑘))
66 fveq2 5270 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → (𝑝𝑗) = (𝑝𝑘))
6765, 66sseq12d 3044 . . . . . . . . . . . . 13 (𝑗 = 𝑘 → ((𝑝‘suc 𝑗) ⊆ (𝑝𝑗) ↔ (𝑝‘suc 𝑘) ⊆ (𝑝𝑘)))
6867cbvralv 2586 . . . . . . . . . . . 12 (∀𝑗 ∈ ω (𝑝‘suc 𝑗) ⊆ (𝑝𝑗) ↔ ∀𝑘 ∈ ω (𝑝‘suc 𝑘) ⊆ (𝑝𝑘))
6963, 68sylib 120 . . . . . . . . . . 11 (𝑝 ∈ ℕ → ∀𝑘 ∈ ω (𝑝‘suc 𝑘) ⊆ (𝑝𝑘))
7069ad2antrr 472 . . . . . . . . . 10 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → ∀𝑘 ∈ ω (𝑝‘suc 𝑘) ⊆ (𝑝𝑘))
71 nnpredcl 11359 . . . . . . . . . . . 12 (𝑗 ∈ ω → 𝑗 ∈ ω)
7271adantl 271 . . . . . . . . . . 11 ((𝑝 ∈ ℕ𝑗 ∈ ω) → 𝑗 ∈ ω)
7372adantr 270 . . . . . . . . . 10 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → 𝑗 ∈ ω)
7456, 70, 73rspcdva 2720 . . . . . . . . 9 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝‘suc 𝑗) ⊆ (𝑝 𝑗))
7552, 74eqsstr3d 3050 . . . . . . . 8 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝𝑗) ⊆ (𝑝 𝑗))
7647, 75eqsstrd 3049 . . . . . . 7 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝 suc 𝑗) ⊆ (𝑝 𝑗))
77 peano3 4386 . . . . . . . . . 10 (𝑗 ∈ ω → suc 𝑗 ≠ ∅)
7877neneqd 2272 . . . . . . . . 9 (𝑗 ∈ ω → ¬ suc 𝑗 = ∅)
7978ad2antlr 473 . . . . . . . 8 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → ¬ suc 𝑗 = ∅)
8079iffalsed 3389 . . . . . . 7 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1𝑜, (𝑝 suc 𝑗)) = (𝑝 suc 𝑗))
8148iffalsed 3389 . . . . . . 7 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → if(𝑗 = ∅, 1𝑜, (𝑝 𝑗)) = (𝑝 𝑗))
8276, 80, 813sstr4d 3058 . . . . . 6 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1𝑜, (𝑝 suc 𝑗)) ⊆ if(𝑗 = ∅, 1𝑜, (𝑝 𝑗)))
83 nndceq0 4406 . . . . . . . 8 (𝑗 ∈ ω → DECID 𝑗 = ∅)
8483adantl 271 . . . . . . 7 ((𝑝 ∈ ℕ𝑗 ∈ ω) → DECID 𝑗 = ∅)
85 exmiddc 780 . . . . . . 7 (DECID 𝑗 = ∅ → (𝑗 = ∅ ∨ ¬ 𝑗 = ∅))
8684, 85syl 14 . . . . . 6 ((𝑝 ∈ ℕ𝑗 ∈ ω) → (𝑗 = ∅ ∨ ¬ 𝑗 = ∅))
8738, 82, 86mpjaodan 745 . . . . 5 ((𝑝 ∈ ℕ𝑗 ∈ ω) → if(suc 𝑗 = ∅, 1𝑜, (𝑝 suc 𝑗)) ⊆ if(𝑗 = ∅, 1𝑜, (𝑝 𝑗)))
88 eqeq1 2091 . . . . . . . 8 (𝑖 = suc 𝑗 → (𝑖 = ∅ ↔ suc 𝑗 = ∅))
89 unieq 3647 . . . . . . . . 9 (𝑖 = suc 𝑗 𝑖 = suc 𝑗)
9089fveq2d 5274 . . . . . . . 8 (𝑖 = suc 𝑗 → (𝑝 𝑖) = (𝑝 suc 𝑗))
9188, 90ifbieq2d 3401 . . . . . . 7 (𝑖 = suc 𝑗 → if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)) = if(suc 𝑗 = ∅, 1𝑜, (𝑝 suc 𝑗)))
9291, 12fvmptg 5345 . . . . . 6 ((suc 𝑗 ∈ ω ∧ if(suc 𝑗 = ∅, 1𝑜, (𝑝 suc 𝑗)) ∈ 2𝑜) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))‘suc 𝑗) = if(suc 𝑗 = ∅, 1𝑜, (𝑝 suc 𝑗)))
9324, 30, 92syl2anc 403 . . . . 5 ((𝑝 ∈ ℕ𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))‘suc 𝑗) = if(suc 𝑗 = ∅, 1𝑜, (𝑝 suc 𝑗)))
9422, 72ffvelrnd 5400 . . . . . . 7 ((𝑝 ∈ ℕ𝑗 ∈ ω) → (𝑝 𝑗) ∈ 2𝑜)
9521, 94, 84ifcldcd 3412 . . . . . 6 ((𝑝 ∈ ℕ𝑗 ∈ ω) → if(𝑗 = ∅, 1𝑜, (𝑝 𝑗)) ∈ 2𝑜)
96 eqeq1 2091 . . . . . . . 8 (𝑖 = 𝑗 → (𝑖 = ∅ ↔ 𝑗 = ∅))
97 unieq 3647 . . . . . . . . 9 (𝑖 = 𝑗 𝑖 = 𝑗)
9897fveq2d 5274 . . . . . . . 8 (𝑖 = 𝑗 → (𝑝 𝑖) = (𝑝 𝑗))
9996, 98ifbieq2d 3401 . . . . . . 7 (𝑖 = 𝑗 → if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)) = if(𝑗 = ∅, 1𝑜, (𝑝 𝑗)))
10099, 12fvmptg 5345 . . . . . 6 ((𝑗 ∈ ω ∧ if(𝑗 = ∅, 1𝑜, (𝑝 𝑗)) ∈ 2𝑜) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))‘𝑗) = if(𝑗 = ∅, 1𝑜, (𝑝 𝑗)))
10139, 95, 100syl2anc 403 . . . . 5 ((𝑝 ∈ ℕ𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))‘𝑗) = if(𝑗 = ∅, 1𝑜, (𝑝 𝑗)))
10287, 93, 1013sstr4d 3058 . . . 4 ((𝑝 ∈ ℕ𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))‘𝑗))
103102ralrimiva 2442 . . 3 (𝑝 ∈ ℕ → ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))‘𝑗))
104 fveq1 5269 . . . . . 6 (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖))) → (𝑓‘suc 𝑗) = ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))‘suc 𝑗))
105 fveq1 5269 . . . . . 6 (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖))) → (𝑓𝑗) = ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))‘𝑗))
106104, 105sseq12d 3044 . . . . 5 (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖))) → ((𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))‘𝑗)))
107106ralbidv 2376 . . . 4 (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖))) → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))‘𝑗)))
108107, 61elrab2 2765 . . 3 ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖))) ∈ ℕ ↔ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖))) ∈ (2𝑜𝑚 ω) ∧ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖)))‘𝑗)))
10918, 103, 108sylanbrc 408 . 2 (𝑝 ∈ ℕ → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1𝑜, (𝑝 𝑖))) ∈ ℕ)
1101, 109fmpti 5416 1 𝑆:ℕ⟶ℕ
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wa 102  wb 103  wo 662  DECID wdc 778   = wceq 1287  wcel 1436  wne 2251  wral 2355  Vcvv 2615  wss 2988  c0 3275  ifcif 3379   cuni 3638  cmpt 3876  Tr wtr 3913  Ord word 4165  suc csuc 4168  ωcom 4380  wf 4979  cfv 4983  (class class class)co 5615  1𝑜c1o 6130  2𝑜c2o 6131  𝑚 cmap 6359  xnninf 6736
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3934  ax-nul 3942  ax-pow 3986  ax-pr 4012  ax-un 4236  ax-setind 4328  ax-iinf 4378
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-rab 2364  df-v 2617  df-sbc 2830  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-if 3380  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-int 3674  df-br 3823  df-opab 3877  df-mpt 3878  df-tr 3914  df-id 4096  df-iord 4169  df-on 4171  df-suc 4174  df-iom 4381  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-rn 4424  df-res 4425  df-ima 4426  df-iota 4948  df-fun 4985  df-fn 4986  df-f 4987  df-fv 4991  df-ov 5618  df-oprab 5619  df-mpt2 5620  df-1o 6137  df-2o 6138  df-map 6361  df-nninf 6738
This theorem is referenced by:  peano4nninf  11365
  Copyright terms: Public domain W3C validator