Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  nnnninf GIF version

Theorem nnnninf 7058
 Description: Elements of ℕ∞ corresponding to natural numbers. The natural number 𝑁 corresponds to a sequence of 𝑁 ones followed by zeroes. This can be strengthened to include infinity, see nnnninf2 7059. (Contributed by Jim Kingdon, 14-Jul-2022.)
Assertion
Ref Expression
nnnninf (𝑁 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) ∈ ℕ)
Distinct variable group:   𝑖,𝑁

Proof of Theorem nnnninf
Dummy variables 𝑓 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1lt2o 6383 . . . . . 6 1o ∈ 2o
21a1i 9 . . . . 5 ((𝑁 ∈ ω ∧ 𝑖 ∈ ω) → 1o ∈ 2o)
3 0lt2o 6382 . . . . . 6 ∅ ∈ 2o
43a1i 9 . . . . 5 ((𝑁 ∈ ω ∧ 𝑖 ∈ ω) → ∅ ∈ 2o)
5 nndcel 6440 . . . . . 6 ((𝑖 ∈ ω ∧ 𝑁 ∈ ω) → DECID 𝑖𝑁)
65ancoms 266 . . . . 5 ((𝑁 ∈ ω ∧ 𝑖 ∈ ω) → DECID 𝑖𝑁)
72, 4, 6ifcldcd 3540 . . . 4 ((𝑁 ∈ ω ∧ 𝑖 ∈ ω) → if(𝑖𝑁, 1o, ∅) ∈ 2o)
87fmpttd 5619 . . 3 (𝑁 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)):ω⟶2o)
9 2onn 6461 . . . . 5 2o ∈ ω
109elexi 2724 . . . 4 2o ∈ V
11 omex 4550 . . . 4 ω ∈ V
1210, 11elmap 6615 . . 3 ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) ∈ (2o𝑚 ω) ↔ (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)):ω⟶2o)
138, 12sylibr 133 . 2 (𝑁 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) ∈ (2o𝑚 ω))
14 ssid 3148 . . . . . . . . 9 1o ⊆ 1o
15 iftrue 3510 . . . . . . . . . . 11 (suc 𝑗𝑁 → if(suc 𝑗𝑁, 1o, ∅) = 1o)
1615sseq1d 3157 . . . . . . . . . 10 (suc 𝑗𝑁 → (if(suc 𝑗𝑁, 1o, ∅) ⊆ 1o ↔ 1o ⊆ 1o))
1716adantl 275 . . . . . . . . 9 (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ suc 𝑗𝑁) → (if(suc 𝑗𝑁, 1o, ∅) ⊆ 1o ↔ 1o ⊆ 1o))
1814, 17mpbiri 167 . . . . . . . 8 (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ suc 𝑗𝑁) → if(suc 𝑗𝑁, 1o, ∅) ⊆ 1o)
19 0ss 3432 . . . . . . . . 9 ∅ ⊆ 1o
20 iffalse 3513 . . . . . . . . . . 11 (¬ suc 𝑗𝑁 → if(suc 𝑗𝑁, 1o, ∅) = ∅)
2120sseq1d 3157 . . . . . . . . . 10 (¬ suc 𝑗𝑁 → (if(suc 𝑗𝑁, 1o, ∅) ⊆ 1o ↔ ∅ ⊆ 1o))
2221adantl 275 . . . . . . . . 9 (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ ¬ suc 𝑗𝑁) → (if(suc 𝑗𝑁, 1o, ∅) ⊆ 1o ↔ ∅ ⊆ 1o))
2319, 22mpbiri 167 . . . . . . . 8 (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ ¬ suc 𝑗𝑁) → if(suc 𝑗𝑁, 1o, ∅) ⊆ 1o)
24 peano2 4552 . . . . . . . . . . 11 (𝑗 ∈ ω → suc 𝑗 ∈ ω)
2524adantl 275 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → suc 𝑗 ∈ ω)
26 simpl 108 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → 𝑁 ∈ ω)
27 nndcel 6440 . . . . . . . . . 10 ((suc 𝑗 ∈ ω ∧ 𝑁 ∈ ω) → DECID suc 𝑗𝑁)
2825, 26, 27syl2anc 409 . . . . . . . . 9 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → DECID suc 𝑗𝑁)
29 exmiddc 822 . . . . . . . . 9 (DECID suc 𝑗𝑁 → (suc 𝑗𝑁 ∨ ¬ suc 𝑗𝑁))
3028, 29syl 14 . . . . . . . 8 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → (suc 𝑗𝑁 ∨ ¬ suc 𝑗𝑁))
3118, 23, 30mpjaodan 788 . . . . . . 7 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → if(suc 𝑗𝑁, 1o, ∅) ⊆ 1o)
3231adantr 274 . . . . . 6 (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑗𝑁) → if(suc 𝑗𝑁, 1o, ∅) ⊆ 1o)
33 iftrue 3510 . . . . . . 7 (𝑗𝑁 → if(𝑗𝑁, 1o, ∅) = 1o)
3433adantl 275 . . . . . 6 (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑗𝑁) → if(𝑗𝑁, 1o, ∅) = 1o)
3532, 34sseqtrrd 3167 . . . . 5 (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑗𝑁) → if(suc 𝑗𝑁, 1o, ∅) ⊆ if(𝑗𝑁, 1o, ∅))
36 ssid 3148 . . . . . . 7 ∅ ⊆ ∅
3736a1i 9 . . . . . 6 (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗𝑁) → ∅ ⊆ ∅)
38 nnord 4569 . . . . . . . . . . . 12 (𝑁 ∈ ω → Ord 𝑁)
39 ordtr 4337 . . . . . . . . . . . 12 (Ord 𝑁 → Tr 𝑁)
4038, 39syl 14 . . . . . . . . . . 11 (𝑁 ∈ ω → Tr 𝑁)
41 trsuc 4381 . . . . . . . . . . 11 ((Tr 𝑁 ∧ suc 𝑗𝑁) → 𝑗𝑁)
4240, 41sylan 281 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ suc 𝑗𝑁) → 𝑗𝑁)
4342ex 114 . . . . . . . . 9 (𝑁 ∈ ω → (suc 𝑗𝑁𝑗𝑁))
4443adantr 274 . . . . . . . 8 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → (suc 𝑗𝑁𝑗𝑁))
4544con3dimp 625 . . . . . . 7 (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗𝑁) → ¬ suc 𝑗𝑁)
4645, 20syl 14 . . . . . 6 (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗𝑁) → if(suc 𝑗𝑁, 1o, ∅) = ∅)
47 iffalse 3513 . . . . . . 7 𝑗𝑁 → if(𝑗𝑁, 1o, ∅) = ∅)
4847adantl 275 . . . . . 6 (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗𝑁) → if(𝑗𝑁, 1o, ∅) = ∅)
4937, 46, 483sstr4d 3173 . . . . 5 (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗𝑁) → if(suc 𝑗𝑁, 1o, ∅) ⊆ if(𝑗𝑁, 1o, ∅))
50 nndcel 6440 . . . . . . 7 ((𝑗 ∈ ω ∧ 𝑁 ∈ ω) → DECID 𝑗𝑁)
5150ancoms 266 . . . . . 6 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → DECID 𝑗𝑁)
52 exmiddc 822 . . . . . 6 (DECID 𝑗𝑁 → (𝑗𝑁 ∨ ¬ 𝑗𝑁))
5351, 52syl 14 . . . . 5 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → (𝑗𝑁 ∨ ¬ 𝑗𝑁))
5435, 49, 53mpjaodan 788 . . . 4 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → if(suc 𝑗𝑁, 1o, ∅) ⊆ if(𝑗𝑁, 1o, ∅))
551a1i 9 . . . . . 6 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → 1o ∈ 2o)
563a1i 9 . . . . . 6 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → ∅ ∈ 2o)
5755, 56, 28ifcldcd 3540 . . . . 5 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → if(suc 𝑗𝑁, 1o, ∅) ∈ 2o)
58 eleq1 2220 . . . . . . 7 (𝑖 = suc 𝑗 → (𝑖𝑁 ↔ suc 𝑗𝑁))
5958ifbid 3526 . . . . . 6 (𝑖 = suc 𝑗 → if(𝑖𝑁, 1o, ∅) = if(suc 𝑗𝑁, 1o, ∅))
60 eqid 2157 . . . . . 6 (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))
6159, 60fvmptg 5541 . . . . 5 ((suc 𝑗 ∈ ω ∧ if(suc 𝑗𝑁, 1o, ∅) ∈ 2o) → ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘suc 𝑗) = if(suc 𝑗𝑁, 1o, ∅))
6225, 57, 61syl2anc 409 . . . 4 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘suc 𝑗) = if(suc 𝑗𝑁, 1o, ∅))
63 simpr 109 . . . . 5 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → 𝑗 ∈ ω)
6455, 56, 51ifcldcd 3540 . . . . 5 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → if(𝑗𝑁, 1o, ∅) ∈ 2o)
65 eleq1 2220 . . . . . . 7 (𝑖 = 𝑗 → (𝑖𝑁𝑗𝑁))
6665ifbid 3526 . . . . . 6 (𝑖 = 𝑗 → if(𝑖𝑁, 1o, ∅) = if(𝑗𝑁, 1o, ∅))
6766, 60fvmptg 5541 . . . . 5 ((𝑗 ∈ ω ∧ if(𝑗𝑁, 1o, ∅) ∈ 2o) → ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑗) = if(𝑗𝑁, 1o, ∅))
6863, 64, 67syl2anc 409 . . . 4 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑗) = if(𝑗𝑁, 1o, ∅))
6954, 62, 683sstr4d 3173 . . 3 ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑗))
7069ralrimiva 2530 . 2 (𝑁 ∈ ω → ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑗))
71 fveq1 5464 . . . . 5 (𝑓 = (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) → (𝑓‘suc 𝑗) = ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘suc 𝑗))
72 fveq1 5464 . . . . 5 (𝑓 = (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) → (𝑓𝑗) = ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑗))
7371, 72sseq12d 3159 . . . 4 (𝑓 = (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) → ((𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑗)))
7473ralbidv 2457 . . 3 (𝑓 = (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑗)))
75 df-nninf 7054 . . 3 = {𝑓 ∈ (2o𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗)}
7674, 75elrab2 2871 . 2 ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) ∈ ℕ ↔ ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) ∈ (2o𝑚 ω) ∧ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑗)))
7713, 70, 76sylanbrc 414 1 (𝑁 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) ∈ ℕ)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 820   = wceq 1335   ∈ wcel 2128  ∀wral 2435   ⊆ wss 3102  ∅c0 3394  ifcif 3505   ↦ cmpt 4025  Tr wtr 4062  Ord word 4321  suc csuc 4324  ωcom 4547  ⟶wf 5163  ‘cfv 5167  (class class class)co 5818  1oc1o 6350  2oc2o 6351   ↑𝑚 cmap 6586  ℕ∞xnninf 7053 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-nul 4090  ax-pow 4134  ax-pr 4168  ax-un 4392  ax-setind 4494  ax-iinf 4545 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-sbc 2938  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-if 3506  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-id 4252  df-iord 4325  df-on 4327  df-suc 4330  df-iom 4548  df-xp 4589  df-rel 4590  df-cnv 4591  df-co 4592  df-dm 4593  df-rn 4594  df-res 4595  df-ima 4596  df-iota 5132  df-fun 5169  df-fn 5170  df-f 5171  df-fv 5175  df-ov 5821  df-oprab 5822  df-mpo 5823  df-1o 6357  df-2o 6358  df-map 6588  df-nninf 7054 This theorem is referenced by:  nnnninf2  7059  fnn0nninf  10318  nninfsellemdc  13544  nninfsellemqall  13549  nninffeq  13554
 Copyright terms: Public domain W3C validator