Theorem nninfisol 7217

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 7264). (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 7214	. . 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 2382	. . . . . 6 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) → 𝑁 ≠ ∅)
11	10	adantr 276	. . . . 5 ⊢ (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋‘∪ 𝑁) = ∅) → 𝑁 ≠ ∅)
12		simpr 110	. . . . 5 ⊢ (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋‘∪ 𝑁) = ∅) → (𝑋‘∪ 𝑁) = ∅)
13	6, 7, 8, 11, 12	nninfisollemne 7215	. . . 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 7216	. . . 4 ⊢ (((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) ∧ (𝑋‘∪ 𝑁) = 1o) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
20		nninff 7206	. . . . . . . . 9 ⊢ (𝑋 ∈ ℕ∞ → 𝑋:ω⟶2o)
21	20	adantl 277	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → 𝑋:ω⟶2o)
22		nnpredcl 4669	. . . . . . . . 9 ⊢ (𝑁 ∈ ω → ∪ 𝑁 ∈ ω)
23	22	adantr 276	. . . . . . . 8 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → ∪ 𝑁 ∈ ω)
24	21, 23	ffvelcdmd 5710	. . . . . . 7 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → (𝑋‘∪ 𝑁) ∈ 2o)
25		df2o3 6506	. . . . . . 7 ⊢ 2o = {∅, 1o}
26	24, 25	eleqtrdi 2297	. . . . . 6 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → (𝑋‘∪ 𝑁) ∈ {∅, 1o})
27		elpri 3655	. . . . . 6 ⊢ ((𝑋‘∪ 𝑁) ∈ {∅, 1o} → ((𝑋‘∪ 𝑁) = ∅ ∨ (𝑋‘∪ 𝑁) = 1o))
28	26, 27	syl 14	. . . . 5 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → ((𝑋‘∪ 𝑁) = ∅ ∨ (𝑋‘∪ 𝑁) = 1o))
29	28	ad2antrr 488	. . . 4 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) → ((𝑋‘∪ 𝑁) = ∅ ∨ (𝑋‘∪ 𝑁) = 1o))
30	13, 19, 29	mpjaodan 799	. . 3 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) ∧ ¬ 𝑁 = ∅) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
31		nndceq0 4664	. . . . 5 ⊢ (𝑁 ∈ ω → DECID 𝑁 = ∅)
32		exmiddc 837	. . . . 5 ⊢ (DECID 𝑁 = ∅ → (𝑁 = ∅ ∨ ¬ 𝑁 = ∅))
33	31, 32	syl 14	. . . 4 ⊢ (𝑁 ∈ ω → (𝑁 = ∅ ∨ ¬ 𝑁 = ∅))
34	33	ad2antrr 488	. . 3 ⊢ (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) → (𝑁 = ∅ ∨ ¬ 𝑁 = ∅))
35	5, 30, 34	mpjaodan 799	. 2 ⊢ (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = ∅) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
36		1n0 6508	. . . . . 6 ⊢ 1o ≠ ∅
37	36	neii 2377	. . . . 5 ⊢ ¬ 1o = ∅
38		simpr 110	. . . . . . . 8 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = 1o) ∧ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
39	38	fveq1d 5572	. . . . . . 7 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = 1o) ∧ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘𝑁) = (𝑋‘𝑁))
40		eqid 2204	. . . . . . . . . 10 ⊢ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))
41		eleq1 2267	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑁 → (𝑖 ∈ 𝑁 ↔ 𝑁 ∈ 𝑁))
42	41	ifbid 3591	. . . . . . . . . 10 ⊢ (𝑖 = 𝑁 → if(𝑖 ∈ 𝑁, 1o, ∅) = if(𝑁 ∈ 𝑁, 1o, ∅))
43		id 19	. . . . . . . . . 10 ⊢ (𝑁 ∈ ω → 𝑁 ∈ ω)
44		nnord 4658	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ω → Ord 𝑁)
45		ordirr 4588	. . . . . . . . . . . . 13 ⊢ (Ord 𝑁 → ¬ 𝑁 ∈ 𝑁)
46	44, 45	syl 14	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ω → ¬ 𝑁 ∈ 𝑁)
47	46	iffalsed 3580	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ω → if(𝑁 ∈ 𝑁, 1o, ∅) = ∅)
48		peano1 4640	. . . . . . . . . . 11 ⊢ ∅ ∈ ω
49	47, 48	eqeltrdi 2295	. . . . . . . . . 10 ⊢ (𝑁 ∈ ω → if(𝑁 ∈ 𝑁, 1o, ∅) ∈ ω)
50	40, 42, 43, 49	fvmptd3 5667	. . . . . . . . 9 ⊢ (𝑁 ∈ ω → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘𝑁) = if(𝑁 ∈ 𝑁, 1o, ∅))
51	50, 47	eqtrd 2237	. . . . . . . 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 2246	. . . . . 6 ⊢ ((((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = 1o) ∧ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) → 1o = ∅)
55	54	ex 115	. . . . 5 ⊢ (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = 1o) → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋 → 1o = ∅))
56	37, 55	mtoi 665	. . . 4 ⊢ (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = 1o) → ¬ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
57	56	olcd 735	. . 3 ⊢ (((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) ∧ (𝑋‘𝑁) = 1o) → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋 ∨ ¬ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋))
58		df-dc 836	. . 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 5710	. . . 4 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → (𝑋‘𝑁) ∈ 2o)
62	61, 25	eleqtrdi 2297	. . 3 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → (𝑋‘𝑁) ∈ {∅, 1o})
63		elpri 3655	. . 3 ⊢ ((𝑋‘𝑁) ∈ {∅, 1o} → ((𝑋‘𝑁) = ∅ ∨ (𝑋‘𝑁) = 1o))
64	62, 63	syl 14	. 2 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → ((𝑋‘𝑁) = ∅ ∨ (𝑋‘𝑁) = 1o))
65	35, 59, 64	mpjaodan 799	1 ⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 709  DECID wdc 835   = wceq 1372   ∈ wcel 2175   ≠ wne 2375  ∅c0 3459  ifcif 3570  {cpr 3633  ∪ cuni 3849   ↦ cmpt 4104  Ord word 4407  ωcom 4636  ⟶wf 5264  ‘cfv 5268  1_oc1o 6485  2_oc2o 6486  ℕ_∞xnninf 7203

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 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-nul 4169  ax-pow 4217  ax-pr 4252  ax-un 4478  ax-setind 4583  ax-iinf 4634

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-ral 2488  df-rex 2489  df-rab 2492  df-v 2773  df-sbc 2998  df-csb 3093  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-nul 3460  df-if 3571  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-br 4044  df-opab 4105  df-mpt 4106  df-tr 4142  df-id 4338  df-iord 4411  df-on 4413  df-suc 4416  df-iom 4637  df-xp 4679  df-rel 4680  df-cnv 4681  df-co 4682  df-dm 4683  df-rn 4684  df-iota 5229  df-fun 5270  df-fn 5271  df-f 5272  df-fv 5276  df-ov 5937  df-oprab 5938  df-mpo 5939  df-1o 6492  df-2o 6493  df-map 6727  df-nninf 7204

This theorem is referenced by: (None)