P. 73 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7201-7300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	djune 7201	Left and right injection never produce equal values. (Contributed by Jim Kingdon, 2-Jul-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (inl‘𝐴) ≠ (inr‘𝐵))
Theorem	updjudhf 7202*	The mapping of an element of the disjoint union to the value of the corresponding function is a function. (Contributed by AV, 26-Jun-2022.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ (𝐴 ⊔ 𝐵) ↦ if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))))    ⇒   ⊢ (𝜑 → 𝐻:(𝐴 ⊔ 𝐵)⟶𝐶)
Theorem	updjudhcoinlf 7203*	The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the left injection equals the first function. (Contributed by AV, 27-Jun-2022.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ (𝐴 ⊔ 𝐵) ↦ if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))))    ⇒   ⊢ (𝜑 → (𝐻 ∘ (inl ↾ 𝐴)) = 𝐹)
Theorem	updjudhcoinrg 7204*	The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the right injection equals the second function. (Contributed by AV, 27-Jun-2022.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ (𝐴 ⊔ 𝐵) ↦ if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))))    ⇒   ⊢ (𝜑 → (𝐻 ∘ (inr ↾ 𝐵)) = 𝐺)
Theorem	updjud 7205*	Universal property of the disjoint union. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∃!ℎ(ℎ:(𝐴 ⊔ 𝐵)⟶𝐶 ∧ (ℎ ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (ℎ ∘ (inr ↾ 𝐵)) = 𝐺))
Syntax	cdjucase 7206	Syntax for the "case" construction.
class case(𝑅, 𝑆)
Definition	df-case 7207	The "case" construction: if 𝐹:𝐴⟶𝑋 and 𝐺:𝐵⟶𝑋 are functions, then case(𝐹, 𝐺):(𝐴 ⊔ 𝐵)⟶𝑋 is the natural function obtained by a definition by cases, hence the name. It is the unique function whose existence is asserted by the universal property of disjoint unions updjud 7205. The definition is adapted to make sense also for binary relations (where the universal property also holds). (Contributed by MC and BJ, 10-Jul-2022.)
⊢ case(𝑅, 𝑆) = ((𝑅 ∘ ◡inl) ∪ (𝑆 ∘ ◡inr))
Theorem	casefun 7208	The "case" construction of two functions is a function. (Contributed by BJ, 10-Jul-2022.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → Fun 𝐺)    ⇒   ⊢ (𝜑 → Fun case(𝐹, 𝐺))
Theorem	casedm 7209	The domain of the "case" construction is the disjoint union of the domains. TODO (although less important): ⊢ ran case(𝐹, 𝐺) = (ran 𝐹 ∪ ran 𝐺). (Contributed by BJ, 10-Jul-2022.)
⊢ dom case(𝐹, 𝐺) = (dom 𝐹 ⊔ dom 𝐺)
Theorem	caserel 7210	The "case" construction of two relations is a relation, with bounds on its domain and codomain. Typically, the "case" construction is used when both relations have a common codomain. (Contributed by BJ, 10-Jul-2022.)
⊢ case(𝑅, 𝑆) ⊆ ((dom 𝑅 ⊔ dom 𝑆) × (ran 𝑅 ∪ ran 𝑆))
Theorem	casef 7211	The "case" construction of two functions is a function on the disjoint union of their domains. (Contributed by BJ, 10-Jul-2022.)
⊢ (𝜑 → 𝐹:𝐴⟶𝑋)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝑋)    ⇒   ⊢ (𝜑 → case(𝐹, 𝐺):(𝐴 ⊔ 𝐵)⟶𝑋)
Theorem	caseinj 7212	The "case" construction of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.)
⊢ (𝜑 → Fun ◡𝑅)    &   ⊢ (𝜑 → Fun ◡𝑆)    &   ⊢ (𝜑 → (ran 𝑅 ∩ ran 𝑆) = ∅)    ⇒   ⊢ (𝜑 → Fun ◡case(𝑅, 𝑆))
Theorem	casef1 7213	The "case" construction of two injective functions with disjoint ranges is an injective function. (Contributed by BJ, 10-Jul-2022.)
⊢ (𝜑 → 𝐹:𝐴–1-1→𝑋)    &   ⊢ (𝜑 → 𝐺:𝐵–1-1→𝑋)    &   ⊢ (𝜑 → (ran 𝐹 ∩ ran 𝐺) = ∅)    ⇒   ⊢ (𝜑 → case(𝐹, 𝐺):(𝐴 ⊔ 𝐵)–1-1→𝑋)
Theorem	caseinl 7214	Applying the "case" construction to a left injection. (Contributed by Jim Kingdon, 15-Mar-2023.)
⊢ (𝜑 → 𝐹 Fn 𝐵)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (case(𝐹, 𝐺)‘(inl‘𝐴)) = (𝐹‘𝐴))
Theorem	caseinr 7215	Applying the "case" construction to a right injection. (Contributed by Jim Kingdon, 12-Jul-2023.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (case(𝐹, 𝐺)‘(inr‘𝐴)) = (𝐺‘𝐴))
2.6.36.4  Dominance and equinumerosity properties of disjoint union
Theorem	djudom 7216	Dominance law for disjoint union. (Contributed by Jim Kingdon, 25-Jul-2022.)
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) → (𝐴 ⊔ 𝐶) ≼ (𝐵 ⊔ 𝐷))
Theorem	omp1eomlem 7217*	Lemma for omp1eom 7218. (Contributed by Jim Kingdon, 11-Jul-2023.)
⊢ 𝐹 = (𝑥 ∈ ω ↦ if(𝑥 = ∅, (inr‘𝑥), (inl‘∪ 𝑥)))    &   ⊢ 𝑆 = (𝑥 ∈ ω ↦ suc 𝑥)    &   ⊢ 𝐺 = case(𝑆, ( I ↾ 1o))    ⇒   ⊢ 𝐹:ω–1-1-onto→(ω ⊔ 1o)
Theorem	omp1eom 7218	Adding one to ω. (Contributed by Jim Kingdon, 10-Jul-2023.)
⊢ (ω ⊔ 1o) ≈ ω
Theorem	endjusym 7219	Reversing right and left operands of a disjoint union produces an equinumerous result. (Contributed by Jim Kingdon, 10-Jul-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⊔ 𝐵) ≈ (𝐵 ⊔ 𝐴))
Theorem	eninl 7220	Equinumerosity of a set and its image under left injection. (Contributed by Jim Kingdon, 30-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (inl “ 𝐴) ≈ 𝐴)
Theorem	eninr 7221	Equinumerosity of a set and its image under right injection. (Contributed by Jim Kingdon, 30-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (inr “ 𝐴) ≈ 𝐴)
Theorem	difinfsnlem 7222*	Lemma for difinfsn 7223. The case where we need to swap 𝐵 and (inr‘∅) in building the mapping 𝐺. (Contributed by Jim Kingdon, 9-Aug-2023.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹:(ω ⊔ 1o)–1-1→𝐴)    &   ⊢ (𝜑 → (𝐹‘(inr‘∅)) ≠ 𝐵)    &   ⊢ 𝐺 = (𝑛 ∈ ω ↦ if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛))))    ⇒   ⊢ (𝜑 → 𝐺:ω–1-1→(𝐴 ∖ {𝐵}))
Theorem	difinfsn 7223*	An infinite set minus one element is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.)
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ω ≼ 𝐴 ∧ 𝐵 ∈ 𝐴) → ω ≼ (𝐴 ∖ {𝐵}))
Theorem	difinfinf 7224*	An infinite set minus a finite subset is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.)
⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ω ≼ 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ∈ Fin)) → ω ≼ (𝐴 ∖ 𝐵))
2.6.36.5  Older definition temporarily kept for comparison, to be deleted
Syntax	cdjud 7225	Syntax for the domain-disjoint-union of two relations.
class (𝑅 ⊔d 𝑆)
Definition	df-djud 7226	The "domain-disjoint-union" of two relations: if 𝑅 ⊆ (𝐴 × 𝑋) and 𝑆 ⊆ (𝐵 × 𝑋) are two binary relations, then (𝑅 ⊔d 𝑆) is the binary relation from (𝐴 ⊔ 𝐵) to 𝑋 having the universal property of disjoint unions (see updjud 7205 in the case of functions). Remark: the restrictions to dom 𝑅 (resp. dom 𝑆) are not necessary since extra stuff would be thrown away in the post-composition with 𝑅 (resp. 𝑆), as in df-case 7207, but they are explicitly written for clarity. (Contributed by MC and BJ, 10-Jul-2022.)
⊢ (𝑅 ⊔d 𝑆) = ((𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ (𝑆 ∘ ◡(inr ↾ dom 𝑆)))
Theorem	djufun 7227	The "domain-disjoint-union" of two functions is a function. (Contributed by BJ, 10-Jul-2022.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → Fun 𝐺)    ⇒   ⊢ (𝜑 → Fun (𝐹 ⊔d 𝐺))
Theorem	djudm 7228	The domain of the "domain-disjoint-union" is the disjoint union of the domains. Remark: its range is the (standard) union of the ranges. (Contributed by BJ, 10-Jul-2022.)
⊢ dom (𝐹 ⊔d 𝐺) = (dom 𝐹 ⊔ dom 𝐺)
Theorem	djuinj 7229	The "domain-disjoint-union" of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.)
⊢ (𝜑 → Fun ◡𝑅)    &   ⊢ (𝜑 → Fun ◡𝑆)    &   ⊢ (𝜑 → (ran 𝑅 ∩ ran 𝑆) = ∅)    ⇒   ⊢ (𝜑 → Fun ◡(𝑅 ⊔d 𝑆))
2.6.36.6  Countable sets
Theorem	0ct 7230	The empty set is countable. Remark of [BauerSwan], p. 14:3 which also has the definition of countable used here. (Contributed by Jim Kingdon, 13-Mar-2023.)
⊢ ∃𝑓 𝑓:ω–onto→(∅ ⊔ 1o)
Theorem	ctmlemr 7231*	Lemma for ctm 7232. One of the directions of the biconditional. (Contributed by Jim Kingdon, 16-Mar-2023.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∃𝑓 𝑓:ω–onto→𝐴 → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o)))
Theorem	ctm 7232*	Two equivalent definitions of countable for an inhabited set. Remark of [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑓 𝑓:ω–onto→𝐴))
Theorem	ctssdclemn0 7233*	Lemma for ctssdc 7236. The ¬ ∅ ∈ 𝑆 case. (Contributed by Jim Kingdon, 16-Aug-2023.)
⊢ (𝜑 → 𝑆 ⊆ ω)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)    &   ⊢ (𝜑 → ¬ ∅ ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
Theorem	ctssdccl 7234*	A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 7236 but expressed in terms of classes rather than ∃. (Contributed by Jim Kingdon, 30-Oct-2023.)
⊢ (𝜑 → 𝐹:ω–onto→(𝐴 ⊔ 1o))    &   ⊢ 𝑆 = {𝑥 ∈ ω ∣ (𝐹‘𝑥) ∈ (inl “ 𝐴)}    &   ⊢ 𝐺 = (◡inl ∘ 𝐹)    ⇒   ⊢ (𝜑 → (𝑆 ⊆ ω ∧ 𝐺:𝑆–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆))
Theorem	ctssdclemr 7235*	Lemma for ctssdc 7236. Showing that our usual definition of countable implies the alternate one. (Contributed by Jim Kingdon, 16-Aug-2023.)
⊢ (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑠))
Theorem	ctssdc 7236*	A set is countable iff there is a surjection from a decidable subset of the natural numbers onto it. The decidability condition is needed as shown at ctssexmid 7273. (Contributed by Jim Kingdon, 15-Aug-2023.)
⊢ (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑠) ↔ ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
Theorem	enumctlemm 7237*	Lemma for enumct 7238. The case where 𝑁 is greater than zero. (Contributed by Jim Kingdon, 13-Mar-2023.)
⊢ (𝜑 → 𝐹:𝑁–onto→𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → ∅ ∈ 𝑁)    &   ⊢ 𝐺 = (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑁, (𝐹‘𝑘), (𝐹‘∅)))    ⇒   ⊢ (𝜑 → 𝐺:ω–onto→𝐴)
Theorem	enumct 7238*	A finitely enumerable set is countable. Lemma 8.1.14 of [AczelRathjen], p. 73 (except that our definition of countable does not require the set to be inhabited). "Finitely enumerable" is defined as ∃𝑛 ∈ ω∃𝑓𝑓:𝑛–onto→𝐴 per Definition 8.1.4 of [AczelRathjen], p. 71 and "countable" is defined as ∃𝑔𝑔:ω–onto→(𝐴 ⊔ 1o) per [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.)
⊢ (∃𝑛 ∈ ω ∃𝑓 𝑓:𝑛–onto→𝐴 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
Theorem	finct 7239*	A finite set is countable. (Contributed by Jim Kingdon, 17-Mar-2023.)
⊢ (𝐴 ∈ Fin → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
Theorem	omct 7240	ω is countable. (Contributed by Jim Kingdon, 23-Dec-2023.)
⊢ ∃𝑓 𝑓:ω–onto→(ω ⊔ 1o)
Theorem	ctfoex 7241*	A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.)
⊢ (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → 𝐴 ∈ V)
2.6.37  The one-point compactification of the natural numbers This section introduces the one-point compactification of the set of natural numbers, introduced by Escardo as the set of nonincreasing sequences on ω with values in 2o. The topological results justifying its name will be proved later.
Syntax	xnninf 7242	Set of nonincreasing sequences in 2o ↑𝑚 ω.
class ℕ∞
Definition	df-nninf 7243*	Define the set of nonincreasing sequences in 2o ↑𝑚 ω. Definition in Section 3.1 of [Pierik], p. 15. If we assumed excluded middle, this would be essentially the same as ℕ0* as defined at df-xnn0 9389 but in its absence the relationship between the two is more complicated. This definition would function much the same whether we used ω or ℕ0, but the former allows us to take advantage of 2o = {∅, 1o} (df2o3 6534) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.)
⊢ ℕ∞ = {𝑓 ∈ (2o ↑𝑚 ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓‘𝑖)}
Theorem	nninfex 7244	ℕ∞ is a set. (Contributed by Jim Kingdon, 10-Aug-2022.)
⊢ ℕ∞ ∈ V
Theorem	nninff 7245	An element of ℕ∞ is a sequence of zeroes and ones. (Contributed by Jim Kingdon, 4-Aug-2022.)
⊢ (𝐴 ∈ ℕ∞ → 𝐴:ω⟶2o)
Theorem	nninfninc 7246	All values beyond a zero in an ℕ∞ sequence are zero. This is another way of stating that elements of ℕ∞ are nonincreasing. (Contributed by Jim Kingdon, 12-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕ∞)    &   ⊢ (𝜑 → 𝑋 ∈ ω)    &   ⊢ (𝜑 → 𝑌 ∈ ω)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑌)    &   ⊢ (𝜑 → (𝐴‘𝑋) = ∅)    ⇒   ⊢ (𝜑 → (𝐴‘𝑌) = ∅)
Theorem	infnninf 7247	The point at infinity in ℕ∞ is the constant sequence equal to 1o. Note that with our encoding of functions, that constant function can also be expressed as (ω × {1o}), as fconstmpt 4735 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.)
⊢ (𝑖 ∈ ω ↦ 1o) ∈ ℕ∞
Theorem	infnninfOLD 7248	Obsolete version of infnninf 7247 as of 10-Aug-2024. (Contributed by Jim Kingdon, 14-Jul-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (ω × {1o}) ∈ ℕ∞
Theorem	nnnninf 7249*	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 7250. (Contributed by Jim Kingdon, 14-Jul-2022.)
⊢ (𝑁 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈ ℕ∞)
Theorem	nnnninf2 7250*	Canonical embedding of suc ω into ℕ∞. (Contributed by BJ, 10-Aug-2024.)
⊢ (𝑁 ∈ suc ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈ ℕ∞)
Theorem	nnnninfeq 7251*	Mapping of a natural number to an element of ℕ∞. (Contributed by Jim Kingdon, 4-Aug-2022.)
⊢ (𝜑 → 𝑃 ∈ ℕ∞)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑁 (𝑃‘𝑥) = 1o)    &   ⊢ (𝜑 → (𝑃‘𝑁) = ∅)    ⇒   ⊢ (𝜑 → 𝑃 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)))
Theorem	nnnninfeq2 7252*	Mapping of a natural number to an element of ℕ∞. Similar to nnnninfeq 7251 but if we have information about a single 1o digit, that gives information about all previous digits. (Contributed by Jim Kingdon, 4-Aug-2022.)
⊢ (𝜑 → 𝑃 ∈ ℕ∞)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → (𝑃‘∪ 𝑁) = 1o)    &   ⊢ (𝜑 → (𝑃‘𝑁) = ∅)    ⇒   ⊢ (𝜑 → 𝑃 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)))
Theorem	nninfisollem0 7253*	Lemma for nninfisol 7256. The case where 𝑁 is zero. (Contributed by Jim Kingdon, 13-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ ℕ∞)    &   ⊢ (𝜑 → (𝑋‘𝑁) = ∅)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → 𝑁 = ∅)    ⇒   ⊢ (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
Theorem	nninfisollemne 7254*	Lemma for nninfisol 7256. A case where 𝑁 is a successor and 𝑁 and 𝑋 are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ ℕ∞)    &   ⊢ (𝜑 → (𝑋‘𝑁) = ∅)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ≠ ∅)    &   ⊢ (𝜑 → (𝑋‘∪ 𝑁) = ∅)    ⇒   ⊢ (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
Theorem	nninfisollemeq 7255*	Lemma for nninfisol 7256. The case where 𝑁 is a successor and 𝑁 and 𝑋 are equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ ℕ∞)    &   ⊢ (𝜑 → (𝑋‘𝑁) = ∅)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ≠ ∅)    &   ⊢ (𝜑 → (𝑋‘∪ 𝑁) = 1o)    ⇒   ⊢ (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
Theorem	nninfisol 7256*	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 7303). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.)
⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
2.6.38  Omniscient sets
Syntax	comni 7257	Extend class definition to include the class of omniscient sets.
class Omni
Definition	df-omni 7258*	An omniscient set is one where we can decide whether a predicate (here represented by a function 𝑓) holds (is equal to 1o) for all elements or fails to hold (is equal to ∅) for some element. Definition 3.1 of [Pierik], p. 14. In particular, ω ∈ Omni is known as the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 28-Jun-2022.)
⊢ Omni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o))}
Theorem	isomni 7259*	The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓(𝑓:𝐴⟶2o → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o))))
Theorem	isomnimap 7260*	The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)))
Theorem	enomnilem 7261	Lemma for enomni 7262. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Omni → 𝐵 ∈ Omni))
Theorem	enomni 7262	Omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Limited Principle of Omniscience as either ω ∈ Omni or ℕ0 ∈ Omni. The former is a better match to conventional notation in the sense that df2o3 6534 says that 2o = {∅, 1o} whereas the corresponding relationship does not exist between 2 and {0, 1}. (Contributed by Jim Kingdon, 13-Jul-2022.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Omni ↔ 𝐵 ∈ Omni))
Theorem	finomni 7263	A finite set is omniscient. Remark right after Definition 3.1 of [Pierik], p. 14. (Contributed by Jim Kingdon, 28-Jun-2022.)
⊢ (𝐴 ∈ Fin → 𝐴 ∈ Omni)
Theorem	exmidomniim 7264	Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 7265. (Contributed by Jim Kingdon, 29-Jun-2022.)
⊢ (EXMID → ∀𝑥 𝑥 ∈ Omni)
Theorem	exmidomni 7265	Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.)
⊢ (EXMID ↔ ∀𝑥 𝑥 ∈ Omni)
Theorem	exmidlpo 7266	Excluded middle implies the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 29-Mar-2023.)
⊢ (EXMID → ω ∈ Omni)
Theorem	fodjuomnilemdc 7267*	Lemma for fodjuomni 7272. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.)
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑂) → DECID ∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧))
Theorem	fodjuf 7268*	Lemma for fodjuomni 7272 and fodjumkv 7283. Domain and range of 𝑃. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.)
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵))    &   ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1o))    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑃 ∈ (2o ↑𝑚 𝑂))
Theorem	fodjum 7269*	Lemma for fodjuomni 7272 and fodjumkv 7283. A condition which shows that 𝐴 is inhabited. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.)
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵))    &   ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1o))    &   ⊢ (𝜑 → ∃𝑤 ∈ 𝑂 (𝑃‘𝑤) = ∅)    ⇒   ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)
Theorem	fodju0 7270*	Lemma for fodjuomni 7272 and fodjumkv 7283. A condition which shows that 𝐴 is empty. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.)
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵))    &   ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1o))    &   ⊢ (𝜑 → ∀𝑤 ∈ 𝑂 (𝑃‘𝑤) = 1o)    ⇒   ⊢ (𝜑 → 𝐴 = ∅)
Theorem	fodjuomnilemres 7271*	Lemma for fodjuomni 7272. The final result with 𝑃 expressed as a local definition. (Contributed by Jim Kingdon, 29-Jul-2022.)
⊢ (𝜑 → 𝑂 ∈ Omni)    &   ⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵))    &   ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1o))    ⇒   ⊢ (𝜑 → (∃𝑥 𝑥 ∈ 𝐴 ∨ 𝐴 = ∅))
Theorem	fodjuomni 7272*	A condition which ensures 𝐴 is either inhabited or empty. Lemma 3.2 of [PradicBrown2022], p. 4. (Contributed by Jim Kingdon, 27-Jul-2022.)
⊢ (𝜑 → 𝑂 ∈ Omni)    &   ⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵))    ⇒   ⊢ (𝜑 → (∃𝑥 𝑥 ∈ 𝐴 ∨ 𝐴 = ∅))
Theorem	ctssexmid 7273*	The decidability condition in ctssdc 7236 is needed. More specifically, ctssdc 7236 minus that condition, plus the Limited Principle of Omniscience (LPO), implies excluded middle. (Contributed by Jim Kingdon, 15-Aug-2023.)
⊢ ((𝑦 ⊆ ω ∧ ∃𝑓 𝑓:𝑦–onto→𝑥) → ∃𝑓 𝑓:ω–onto→(𝑥 ⊔ 1o))    &   ⊢ ω ∈ Omni    ⇒   ⊢ (𝜑 ∨ ¬ 𝜑)
2.6.39  Markov's principle
Syntax	cmarkov 7274	Extend class definition to include the class of Markov sets.
class Markov
Definition	df-markov 7275*	A Markov set is one where if a predicate (here represented by a function 𝑓) on that set does not hold (where hold means is equal to 1o) for all elements, then there exists an element where it fails (is equal to ∅). Generalization of definition 2.5 of [Pierik], p. 9. In particular, ω ∈ Markov is known as Markov's Principle (MP). (Contributed by Jim Kingdon, 18-Mar-2023.)
⊢ Markov = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (¬ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅))}
Theorem	ismkv 7276*	The predicate of being Markov. (Contributed by Jim Kingdon, 18-Mar-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))))
Theorem	ismkvmap 7277*	The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 18-Mar-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)))
Theorem	ismkvnex 7278*	The predicate of being Markov stated in terms of double negation and comparison with 1o. (Contributed by Jim Kingdon, 29-Nov-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ (2o ↑𝑚 𝐴)(¬ ¬ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)))
Theorem	omnimkv 7279	An omniscient set is Markov. In particular, the case where 𝐴 is ω means that the Limited Principle of Omniscience (LPO) implies Markov's Principle (MP). (Contributed by Jim Kingdon, 18-Mar-2023.)
⊢ (𝐴 ∈ Omni → 𝐴 ∈ Markov)
Theorem	exmidmp 7280	Excluded middle implies Markov's Principle (MP). (Contributed by Jim Kingdon, 4-Apr-2023.)
⊢ (EXMID → ω ∈ Markov)
Theorem	mkvprop 7281*	Markov's Principle expressed in terms of propositions (or more precisely, the 𝐴 = ω case is Markov's Principle). (Contributed by Jim Kingdon, 19-Mar-2023.)
⊢ ((𝐴 ∈ Markov ∧ ∀𝑛 ∈ 𝐴 DECID 𝜑 ∧ ¬ ∀𝑛 ∈ 𝐴 ¬ 𝜑) → ∃𝑛 ∈ 𝐴 𝜑)
Theorem	fodjumkvlemres 7282*	Lemma for fodjumkv 7283. The final result with 𝑃 expressed as a local definition. (Contributed by Jim Kingdon, 25-Mar-2023.)
⊢ (𝜑 → 𝑀 ∈ Markov)    &   ⊢ (𝜑 → 𝐹:𝑀–onto→(𝐴 ⊔ 𝐵))    &   ⊢ 𝑃 = (𝑦 ∈ 𝑀 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1o))    ⇒   ⊢ (𝜑 → (𝐴 ≠ ∅ → ∃𝑥 𝑥 ∈ 𝐴))
Theorem	fodjumkv 7283*	A condition which ensures that a nonempty set is inhabited. (Contributed by Jim Kingdon, 25-Mar-2023.)
⊢ (𝜑 → 𝑀 ∈ Markov)    &   ⊢ (𝜑 → 𝐹:𝑀–onto→(𝐴 ⊔ 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 ≠ ∅ → ∃𝑥 𝑥 ∈ 𝐴))
Theorem	enmkvlem 7284	Lemma for enmkv 7285. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Markov → 𝐵 ∈ Markov))
Theorem	enmkv 7285	Being Markov is invariant with respect to equinumerosity. For example, this means that we can express the Markov's Principle as either ω ∈ Markov or ℕ0 ∈ Markov. The former is a better match to conventional notation in the sense that df2o3 6534 says that 2o = {∅, 1o} whereas the corresponding relationship does not exist between 2 and {0, 1}. (Contributed by Jim Kingdon, 24-Jun-2024.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Markov ↔ 𝐵 ∈ Markov))
2.6.40  Weakly omniscient sets
Syntax	cwomni 7286	Extend class definition to include the class of weakly omniscient sets.
class WOmni
Definition	df-womni 7287*	A weakly omniscient set is one where we can decide whether a predicate (here represented by a function 𝑓) holds (is equal to 1o) for all elements or not. Generalization of definition 2.4 of [Pierik], p. 9. In particular, ω ∈ WOmni is known as the Weak Limited Principle of Omniscience (WLPO). The term WLPO is common in the literature; there appears to be no widespread term for what we are calling a weakly omniscient set. (Contributed by Jim Kingdon, 9-Jun-2024.)
⊢ WOmni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → DECID ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o)}
Theorem	iswomni 7288*	The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓(𝑓:𝐴⟶2o → DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)))
Theorem	iswomnimap 7289*	The predicate of being weakly omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 9-Jun-2024.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o))
Theorem	omniwomnimkv 7290	A set is omniscient if and only if it is weakly omniscient and Markov. The case 𝐴 = ω says that LPO ↔ WLPO ∧ MP which is a remark following Definition 2.5 of [Pierik], p. 9. (Contributed by Jim Kingdon, 9-Jun-2024.)
⊢ (𝐴 ∈ Omni ↔ (𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov))
Theorem	lpowlpo 7291	LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7290. There is an analogue in terms of analytic omniscience principles at tridceq 16167. (Contributed by Jim Kingdon, 24-Jul-2024.)
⊢ (ω ∈ Omni → ω ∈ WOmni)
Theorem	enwomnilem 7292	Lemma for enwomni 7293. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ WOmni → 𝐵 ∈ WOmni))
Theorem	enwomni 7293	Weak omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Weak Limited Principle of Omniscience as either ω ∈ WOmni or ℕ0 ∈ WOmni. The former is a better match to conventional notation in the sense that df2o3 6534 says that 2o = {∅, 1o} whereas the corresponding relationship does not exist between 2 and {0, 1}. (Contributed by Jim Kingdon, 20-Jun-2024.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ WOmni ↔ 𝐵 ∈ WOmni))
Theorem	nninfdcinf 7294*	The Weak Limited Principle of Omniscience (WLPO) implies that it is decidable whether an element of ℕ∞ equals the point at infinity. (Contributed by Jim Kingdon, 3-Dec-2024.)
⊢ (𝜑 → ω ∈ WOmni)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ∞)    ⇒   ⊢ (𝜑 → DECID 𝑁 = (𝑖 ∈ ω ↦ 1o))
Theorem	nninfwlporlemd 7295*	Given two countably infinite sequences of zeroes and ones, they are equal if and only if a sequence formed by pointwise comparing them is all ones. (Contributed by Jim Kingdon, 6-Dec-2024.)
⊢ (𝜑 → 𝑋:ω⟶2o)    &   ⊢ (𝜑 → 𝑌:ω⟶2o)    &   ⊢ 𝐷 = (𝑖 ∈ ω ↦ if((𝑋‘𝑖) = (𝑌‘𝑖), 1o, ∅))    ⇒   ⊢ (𝜑 → (𝑋 = 𝑌 ↔ 𝐷 = (𝑖 ∈ ω ↦ 1o)))
Theorem	nninfwlporlem 7296*	Lemma for nninfwlpor 7297. The result. (Contributed by Jim Kingdon, 7-Dec-2024.)
⊢ (𝜑 → 𝑋:ω⟶2o)    &   ⊢ (𝜑 → 𝑌:ω⟶2o)    &   ⊢ 𝐷 = (𝑖 ∈ ω ↦ if((𝑋‘𝑖) = (𝑌‘𝑖), 1o, ∅))    &   ⊢ (𝜑 → ω ∈ WOmni)    ⇒   ⊢ (𝜑 → DECID 𝑋 = 𝑌)
Theorem	nninfwlpor 7297*	The Weak Limited Principle of Omniscience (WLPO) implies that equality for ℕ∞ is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.)
⊢ (ω ∈ WOmni → ∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦)
Theorem	nninfwlpoimlemg 7298*	Lemma for nninfwlpoim 7302. (Contributed by Jim Kingdon, 8-Dec-2024.)
⊢ (𝜑 → 𝐹:ω⟶2o)    &   ⊢ 𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅, 1o))    ⇒   ⊢ (𝜑 → 𝐺 ∈ ℕ∞)
Theorem	nninfwlpoimlemginf 7299*	Lemma for nninfwlpoim 7302. (Contributed by Jim Kingdon, 8-Dec-2024.)
⊢ (𝜑 → 𝐹:ω⟶2o)    &   ⊢ 𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅, 1o))    ⇒   ⊢ (𝜑 → (𝐺 = (𝑖 ∈ ω ↦ 1o) ↔ ∀𝑛 ∈ ω (𝐹‘𝑛) = 1o))
Theorem	nninfwlpoimlemdc 7300*	Lemma for nninfwlpoim 7302. (Contributed by Jim Kingdon, 8-Dec-2024.)
⊢ (𝜑 → 𝐹:ω⟶2o)    &   ⊢ 𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅, 1o))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦)    ⇒   ⊢ (𝜑 → DECID ∀𝑛 ∈ ω (𝐹‘𝑛) = 1o)