Theorem nninfisol 7321

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).

By contrast, the point at infinity being isolated is equivalent to the Weak Limited Principle of Omniscience (WLPO) (nninfinfwlpo 7368). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.)

Assertion

Ref	Expression
nninfisol	⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)

Distinct variable groups:   𝑖,𝑁   𝑖,𝑋

Proof of Theorem nninfisol

Step	Hyp	Ref	Expression
1		simpllr 534	. . . 4 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ 𝑁 = ∅) → 𝑋 ∈ ℕ∞)
2		simplr 528	. . . 4 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ 𝑁 = ∅) → (𝑋‘𝑁) = ∅)
3		simplll 533	. . . 4 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ 𝑁 = ∅) → 𝑁 ∈ ω)
4		simpr 110	. . . 4 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ 𝑁 = ∅) → 𝑁 = ∅)
5	1, 2, 3, 4	nninfisollem0 7318	. . 3 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ 𝑁 = ∅) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
6		simp-4r 542	. . . . 5 ⊢ (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋‘∪ 𝑁) = ∅) → 𝑋 ∈ ℕ∞)
7		simpllr 534	. . . . 5 ⊢ (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋‘∪ 𝑁) = ∅) → (𝑋‘𝑁) = ∅)
8		simp-4l 541	. . . . 5 ⊢ (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋‘∪ 𝑁) = ∅) → 𝑁 ∈ ω)
9		simpr 110	. . . . . . 7 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) → ¬ 𝑁 = ∅)
10	9	neqned 2407	. . . . . 6 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) → 𝑁 ≠ ∅)
11	10	adantr 276	. . . . 5 ⊢ (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋‘∪ 𝑁) = ∅) → 𝑁 ≠ ∅)
12		simpr 110	. . . . 5 ⊢ (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋‘∪ 𝑁) = ∅) → (𝑋‘∪ 𝑁) = ∅)
13	6, 7, 8, 11, 12	nninfisollemne 7319	. . . 4 ⊢ (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋‘∪ 𝑁) = ∅) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
14		simp-4r 542	. . . . 5 ⊢ (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋‘∪ 𝑁) = 1o) → 𝑋 ∈ ℕ∞)
15		simpllr 534	. . . . 5 ⊢ (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋‘∪ 𝑁) = 1o) → (𝑋‘𝑁) = ∅)
16		simp-4l 541	. . . . 5 ⊢ (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋‘∪ 𝑁) = 1o) → 𝑁 ∈ ω)
17	10	adantr 276	. . . . 5 ⊢ (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋‘∪ 𝑁) = 1o) → 𝑁 ≠ ∅)
18		simpr 110	. . . . 5 ⊢ (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋‘∪ 𝑁) = 1o) → (𝑋‘∪ 𝑁) = 1o)
19	14, 15, 16, 17, 18	nninfisollemeq 7320	. . . 4 ⊢ (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋‘∪ 𝑁) = 1o) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
20		nninff 7310	. . . . . . . . 9 ⊢ (𝑋 ∈ ℕ∞ → 𝑋:ω⟶2o)
21	20	adantl 277	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → 𝑋:ω⟶2o)
22		nnpredcl 4717	. . . . . . . . 9 ⊢ (𝑁 ∈ ω → ∪ 𝑁 ∈ ω)
23	22	adantr 276	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → ∪ 𝑁 ∈ ω)
24	21, 23	ffvelcdmd 5777	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → (𝑋‘∪ 𝑁) ∈ 2o)
25		df2o3 6590	. . . . . . 7 ⊢ 2o = {∅, 1o}
26	24, 25	eleqtrdi 2322	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → (𝑋‘∪ 𝑁) ∈ {∅, 1o})
27		elpri 3690	. . . . . 6 ⊢ ((𝑋‘∪ 𝑁) ∈ {∅, 1o} → ((𝑋‘∪ 𝑁) = ∅ ∨ (𝑋‘∪ 𝑁) = 1o))
28	26, 27	syl 14	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → ((𝑋‘∪ 𝑁) = ∅ ∨ (𝑋‘∪ 𝑁) = 1o))
29	28	ad2antrr 488	. . . 4 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) → ((𝑋‘∪ 𝑁) = ∅ ∨ (𝑋‘∪ 𝑁) = 1o))
30	13, 19, 29	mpjaodan 803	. . 3 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
31		nndceq0 4712	. . . . 5 ⊢ (𝑁 ∈ ω → DECID 𝑁 = ∅)
32		exmiddc 841	. . . . 5 ⊢ (DECID 𝑁 = ∅ → (𝑁 = ∅ ∨ ¬ 𝑁 = ∅))
33	31, 32	syl 14	. . . 4 ⊢ (𝑁 ∈ ω → (𝑁 = ∅ ∨ ¬ 𝑁 = ∅))
34	33	ad2antrr 488	. . 3 ⊢ (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) → (𝑁 = ∅ ∨ ¬ 𝑁 = ∅))
35	5, 30, 34	mpjaodan 803	. 2 ⊢ (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
36		1n0 6593	. . . . . 6 ⊢ 1o ≠ ∅
37	36	neii 2402	. . . . 5 ⊢ ¬ 1o = ∅
38		simpr 110	. . . . . . . 8 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = 1o) ∧ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
39	38	fveq1d 5635	. . . . . . 7 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = 1o) ∧ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘𝑁) = (𝑋‘𝑁))
40		eqid 2229	. . . . . . . . . 10 ⊢ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))
41		eleq1 2292	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑁 → (𝑖 ∈ 𝑁 ↔ 𝑁 ∈ 𝑁))
42	41	ifbid 3625	. . . . . . . . . 10 ⊢ (𝑖 = 𝑁 → if(𝑖 ∈ 𝑁, 1o, ∅) = if(𝑁 ∈ 𝑁, 1o, ∅))
43		id 19	. . . . . . . . . 10 ⊢ (𝑁 ∈ ω → 𝑁 ∈ ω)
44		nnord 4706	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ω → Ord 𝑁)
45		ordirr 4636	. . . . . . . . . . . . 13 ⊢ (Ord 𝑁 → ¬ 𝑁 ∈ 𝑁)
46	44, 45	syl 14	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ω → ¬ 𝑁 ∈ 𝑁)
47	46	iffalsed 3613	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ω → if(𝑁 ∈ 𝑁, 1o, ∅) = ∅)
48		peano1 4688	. . . . . . . . . . 11 ⊢ ∅ ∈ ω
49	47, 48	eqeltrdi 2320	. . . . . . . . . 10 ⊢ (𝑁 ∈ ω → if(𝑁 ∈ 𝑁, 1o, ∅) ∈ ω)
50	40, 42, 43, 49	fvmptd3 5734	. . . . . . . . 9 ⊢ (𝑁 ∈ ω → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘𝑁) = if(𝑁 ∈ 𝑁, 1o, ∅))
51	50, 47	eqtrd 2262	. . . . . . . 8 ⊢ (𝑁 ∈ ω → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘𝑁) = ∅)
52	51	ad3antrrr 492	. . . . . . 7 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = 1o) ∧ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘𝑁) = ∅)
53		simplr 528	. . . . . . 7 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = 1o) ∧ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) → (𝑋‘𝑁) = 1o)
54	39, 52, 53	3eqtr3rd 2271	. . . . . 6 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = 1o) ∧ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) → 1o = ∅)
55	54	ex 115	. . . . 5 ⊢ (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = 1o) → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋 → 1o = ∅))
56	37, 55	mtoi 668	. . . 4 ⊢ (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = 1o) → ¬ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
57	56	olcd 739	. . 3 ⊢ (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = 1o) → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋 ∨ ¬ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋))
58		df-dc 840	. . 3 ⊢ (DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋 ↔ ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋 ∨ ¬ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋))
59	57, 58	sylibr 134	. 2 ⊢ (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = 1o) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
60		simpl 109	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → 𝑁 ∈ ω)
61	21, 60	ffvelcdmd 5777	. . . 4 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → (𝑋‘𝑁) ∈ 2o)
62	61, 25	eleqtrdi 2322	. . 3 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → (𝑋‘𝑁) ∈ {∅, 1o})
63		elpri 3690	. . 3 ⊢ ((𝑋‘𝑁) ∈ {∅, 1o} → ((𝑋‘𝑁) = ∅ ∨ (𝑋‘𝑁) = 1o))
64	62, 63	syl 14	. 2 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → ((𝑋‘𝑁) = ∅ ∨ (𝑋‘𝑁) = 1o))
65	35, 59, 64	mpjaodan 803	1 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 713  DECID wdc 839   = wceq 1395   ∈ wcel 2200   ≠ wne 2400  ∅c0 3492  ifcif 3603  {cpr 3668  ∪ cuni 3889   ↦ cmpt 4146  Ord word 4455  ωcom 4684  ⟶wf 5318  ‘cfv 5322  1_oc1o 6568  2_oc2o 6569  ℕ_∞xnninf 7307

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4203  ax-nul 4211  ax-pow 4260  ax-pr 4295  ax-un 4526  ax-setind 4631  ax-iinf 4682

This theorem depends on definitions:  df-bi 117  df-dc 840  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2802  df-sbc 3030  df-csb 3126  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-nul 3493  df-if 3604  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3890  df-int 3925  df-br 4085  df-opab 4147  df-mpt 4148  df-tr 4184  df-id 4386  df-iord 4459  df-on 4461  df-suc 4464  df-iom 4685  df-xp 4727  df-rel 4728  df-cnv 4729  df-co 4730  df-dm 4731  df-rn 4732  df-iota 5282  df-fun 5324  df-fn 5325  df-f 5326  df-fv 5330  df-ov 6014  df-oprab 6015  df-mpo 6016  df-1o 6575  df-2o 6576  df-map 6812  df-nninf 7308

This theorem is referenced by: (None)