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

Theorem nninfisol 7125
Description: Finite elements of are isolated. That is, given a natural number and any element of , it is decidable whether the natural number (when converted to an element of ) is equal to the given element of . Stated in an online post by Martin Escardo. One way to understand this theorem is that you do not need to look at an unbounded number of elements of the sequence 𝑋 to decide whether it is equal to 𝑁 (in fact, you only need to look at two elements and 𝑁 tells you where to look). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.)
Assertion
Ref Expression
nninfisol ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) → DECID (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋)
Distinct variable groups:   𝑖,𝑁   𝑖,𝑋

Proof of Theorem nninfisol
StepHypRef Expression
1 simpllr 534 . . . 4 ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ 𝑁 = ∅) → 𝑋 ∈ ℕ)
2 simplr 528 . . . 4 ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ 𝑁 = ∅) → (𝑋𝑁) = ∅)
3 simplll 533 . . . 4 ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ 𝑁 = ∅) → 𝑁 ∈ ω)
4 simpr 110 . . . 4 ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ 𝑁 = ∅) → 𝑁 = ∅)
51, 2, 3, 4nninfisollem0 7122 . . 3 ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ 𝑁 = ∅) → DECID (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋)
6 simp-4r 542 . . . . 5 (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋 𝑁) = ∅) → 𝑋 ∈ ℕ)
7 simpllr 534 . . . . 5 (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋 𝑁) = ∅) → (𝑋𝑁) = ∅)
8 simp-4l 541 . . . . 5 (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋 𝑁) = ∅) → 𝑁 ∈ ω)
9 simpr 110 . . . . . . 7 ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ ¬ 𝑁 = ∅) → ¬ 𝑁 = ∅)
109neqned 2354 . . . . . 6 ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ ¬ 𝑁 = ∅) → 𝑁 ≠ ∅)
1110adantr 276 . . . . 5 (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋 𝑁) = ∅) → 𝑁 ≠ ∅)
12 simpr 110 . . . . 5 (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋 𝑁) = ∅) → (𝑋 𝑁) = ∅)
136, 7, 8, 11, 12nninfisollemne 7123 . . . 4 (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋 𝑁) = ∅) → DECID (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋)
14 simp-4r 542 . . . . 5 (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋 𝑁) = 1o) → 𝑋 ∈ ℕ)
15 simpllr 534 . . . . 5 (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋 𝑁) = 1o) → (𝑋𝑁) = ∅)
16 simp-4l 541 . . . . 5 (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋 𝑁) = 1o) → 𝑁 ∈ ω)
1710adantr 276 . . . . 5 (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋 𝑁) = 1o) → 𝑁 ≠ ∅)
18 simpr 110 . . . . 5 (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋 𝑁) = 1o) → (𝑋 𝑁) = 1o)
1914, 15, 16, 17, 18nninfisollemeq 7124 . . . 4 (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋 𝑁) = 1o) → DECID (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋)
20 nninff 7115 . . . . . . . . 9 (𝑋 ∈ ℕ𝑋:ω⟶2o)
2120adantl 277 . . . . . . . 8 ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) → 𝑋:ω⟶2o)
22 nnpredcl 4619 . . . . . . . . 9 (𝑁 ∈ ω → 𝑁 ∈ ω)
2322adantr 276 . . . . . . . 8 ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) → 𝑁 ∈ ω)
2421, 23ffvelcdmd 5648 . . . . . . 7 ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) → (𝑋 𝑁) ∈ 2o)
25 df2o3 6425 . . . . . . 7 2o = {∅, 1o}
2624, 25eleqtrdi 2270 . . . . . 6 ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) → (𝑋 𝑁) ∈ {∅, 1o})
27 elpri 3614 . . . . . 6 ((𝑋 𝑁) ∈ {∅, 1o} → ((𝑋 𝑁) = ∅ ∨ (𝑋 𝑁) = 1o))
2826, 27syl 14 . . . . 5 ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) → ((𝑋 𝑁) = ∅ ∨ (𝑋 𝑁) = 1o))
2928ad2antrr 488 . . . 4 ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ ¬ 𝑁 = ∅) → ((𝑋 𝑁) = ∅ ∨ (𝑋 𝑁) = 1o))
3013, 19, 29mpjaodan 798 . . 3 ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) ∧ ¬ 𝑁 = ∅) → DECID (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋)
31 nndceq0 4614 . . . . 5 (𝑁 ∈ ω → DECID 𝑁 = ∅)
32 exmiddc 836 . . . . 5 (DECID 𝑁 = ∅ → (𝑁 = ∅ ∨ ¬ 𝑁 = ∅))
3331, 32syl 14 . . . 4 (𝑁 ∈ ω → (𝑁 = ∅ ∨ ¬ 𝑁 = ∅))
3433ad2antrr 488 . . 3 (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) → (𝑁 = ∅ ∨ ¬ 𝑁 = ∅))
355, 30, 34mpjaodan 798 . 2 (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = ∅) → DECID (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋)
36 1n0 6427 . . . . . 6 1o ≠ ∅
3736neii 2349 . . . . 5 ¬ 1o = ∅
38 simpr 110 . . . . . . . 8 ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = 1o) ∧ (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋) → (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋)
3938fveq1d 5513 . . . . . . 7 ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = 1o) ∧ (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋) → ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑁) = (𝑋𝑁))
40 eqid 2177 . . . . . . . . . 10 (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))
41 eleq1 2240 . . . . . . . . . . 11 (𝑖 = 𝑁 → (𝑖𝑁𝑁𝑁))
4241ifbid 3555 . . . . . . . . . 10 (𝑖 = 𝑁 → if(𝑖𝑁, 1o, ∅) = if(𝑁𝑁, 1o, ∅))
43 id 19 . . . . . . . . . 10 (𝑁 ∈ ω → 𝑁 ∈ ω)
44 nnord 4608 . . . . . . . . . . . . 13 (𝑁 ∈ ω → Ord 𝑁)
45 ordirr 4538 . . . . . . . . . . . . 13 (Ord 𝑁 → ¬ 𝑁𝑁)
4644, 45syl 14 . . . . . . . . . . . 12 (𝑁 ∈ ω → ¬ 𝑁𝑁)
4746iffalsed 3544 . . . . . . . . . . 11 (𝑁 ∈ ω → if(𝑁𝑁, 1o, ∅) = ∅)
48 peano1 4590 . . . . . . . . . . 11 ∅ ∈ ω
4947, 48eqeltrdi 2268 . . . . . . . . . 10 (𝑁 ∈ ω → if(𝑁𝑁, 1o, ∅) ∈ ω)
5040, 42, 43, 49fvmptd3 5605 . . . . . . . . 9 (𝑁 ∈ ω → ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑁) = if(𝑁𝑁, 1o, ∅))
5150, 47eqtrd 2210 . . . . . . . 8 (𝑁 ∈ ω → ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑁) = ∅)
5251ad3antrrr 492 . . . . . . 7 ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = 1o) ∧ (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋) → ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑁) = ∅)
53 simplr 528 . . . . . . 7 ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = 1o) ∧ (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋) → (𝑋𝑁) = 1o)
5439, 52, 533eqtr3rd 2219 . . . . . 6 ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = 1o) ∧ (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋) → 1o = ∅)
5554ex 115 . . . . 5 (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = 1o) → ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋 → 1o = ∅))
5637, 55mtoi 664 . . . 4 (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = 1o) → ¬ (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋)
5756olcd 734 . . 3 (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = 1o) → ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋 ∨ ¬ (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋))
58 df-dc 835 . . 3 (DECID (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋 ↔ ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋 ∨ ¬ (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋))
5957, 58sylibr 134 . 2 (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) ∧ (𝑋𝑁) = 1o) → DECID (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋)
60 simpl 109 . . . . 5 ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) → 𝑁 ∈ ω)
6121, 60ffvelcdmd 5648 . . . 4 ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) → (𝑋𝑁) ∈ 2o)
6261, 25eleqtrdi 2270 . . 3 ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) → (𝑋𝑁) ∈ {∅, 1o})
63 elpri 3614 . . 3 ((𝑋𝑁) ∈ {∅, 1o} → ((𝑋𝑁) = ∅ ∨ (𝑋𝑁) = 1o))
6462, 63syl 14 . 2 ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) → ((𝑋𝑁) = ∅ ∨ (𝑋𝑁) = 1o))
6535, 59, 64mpjaodan 798 1 ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ) → DECID (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = 𝑋)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wo 708  DECID wdc 834   = wceq 1353  wcel 2148  wne 2347  c0 3422  ifcif 3534  {cpr 3592   cuni 3807  cmpt 4061  Ord word 4359  ωcom 4586  wf 5208  cfv 5212  1oc1o 6404  2oc2o 6405  xnninf 7112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-iord 4363  df-on 4365  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-fv 5220  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1o 6411  df-2o 6412  df-map 6644  df-nninf 7113
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator