P. 72 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7101-7200   *Has distinct variable group(s)

Type	Label	Description
Statement
2.6.36.5  Older definition temporarily kept for comparison, to be deleted
Syntax	cdjud 7101	Syntax for the domain-disjoint-union of two relations.
class (𝑅 ⊔d 𝑆)
Definition	df-djud 7102	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 7081 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 7083, but they are explicitly written for clarity. (Contributed by MC and BJ, 10-Jul-2022.)
⊢ (𝑅 ⊔d 𝑆) = ((𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ (𝑆 ∘ ◡(inr ↾ dom 𝑆)))
Theorem	djufun 7103	The "domain-disjoint-union" of two functions is a function. (Contributed by BJ, 10-Jul-2022.)
⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → Fun 𝐺)    ⇒   ⊢ (𝜑 → Fun (𝐹 ⊔d 𝐺))
Theorem	djudm 7104	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 7105	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 7106	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 7107*	Lemma for ctm 7108. One of the directions of the biconditional. (Contributed by Jim Kingdon, 16-Mar-2023.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∃𝑓 𝑓:ω–onto→𝐴 → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o)))
Theorem	ctm 7108*	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 7109*	Lemma for ctssdc 7112. The ¬ ∅ ∈ 𝑆 case. (Contributed by Jim Kingdon, 16-Aug-2023.)
⊢ (𝜑 → 𝑆 ⊆ ω)    &   ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)    &   ⊢ (𝜑 → ¬ ∅ ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
Theorem	ctssdccl 7110*	A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 7112 but expressed in terms of classes rather than ∃. (Contributed by Jim Kingdon, 30-Oct-2023.)
⊢ (𝜑 → 𝐹:ω–onto→(𝐴 ⊔ 1o))    &   ⊢ 𝑆 = {𝑥 ∈ ω ∣ (𝐹‘𝑥) ∈ (inl “ 𝐴)}    &   ⊢ 𝐺 = (◡inl ∘ 𝐹)    ⇒   ⊢ (𝜑 → (𝑆 ⊆ ω ∧ 𝐺:𝑆–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆))
Theorem	ctssdclemr 7111*	Lemma for ctssdc 7112. Showing that our usual definition of countable implies the alternate one. (Contributed by Jim Kingdon, 16-Aug-2023.)
⊢ (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑠))
Theorem	ctssdc 7112*	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 7148. (Contributed by Jim Kingdon, 15-Aug-2023.)
⊢ (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑠) ↔ ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
Theorem	enumctlemm 7113*	Lemma for enumct 7114. The case where 𝑁 is greater than zero. (Contributed by Jim Kingdon, 13-Mar-2023.)
⊢ (𝜑 → 𝐹:𝑁–onto→𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → ∅ ∈ 𝑁)    &   ⊢ 𝐺 = (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑁, (𝐹‘𝑘), (𝐹‘∅)))    ⇒   ⊢ (𝜑 → 𝐺:ω–onto→𝐴)
Theorem	enumct 7114*	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 7115*	A finite set is countable. (Contributed by Jim Kingdon, 17-Mar-2023.)
⊢ (𝐴 ∈ Fin → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
Theorem	omct 7116	ω is countable. (Contributed by Jim Kingdon, 23-Dec-2023.)
⊢ ∃𝑓 𝑓:ω–onto→(ω ⊔ 1o)
Theorem	ctfoex 7117*	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 7118	Set of nonincreasing sequences in 2o ↑𝑚 ω.
class ℕ∞
Definition	df-nninf 7119*	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 9240 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 6431) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.)
⊢ ℕ∞ = {𝑓 ∈ (2o ↑𝑚 ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓‘𝑖)}
Theorem	nninfex 7120	ℕ∞ is a set. (Contributed by Jim Kingdon, 10-Aug-2022.)
⊢ ℕ∞ ∈ V
Theorem	nninff 7121	An element of ℕ∞ is a sequence of zeroes and ones. (Contributed by Jim Kingdon, 4-Aug-2022.)
⊢ (𝐴 ∈ ℕ∞ → 𝐴:ω⟶2o)
Theorem	infnninf 7122	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 4674 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.)
⊢ (𝑖 ∈ ω ↦ 1o) ∈ ℕ∞
Theorem	infnninfOLD 7123	Obsolete version of infnninf 7122 as of 10-Aug-2024. (Contributed by Jim Kingdon, 14-Jul-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (ω × {1o}) ∈ ℕ∞
Theorem	nnnninf 7124*	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 7125. (Contributed by Jim Kingdon, 14-Jul-2022.)
⊢ (𝑁 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈ ℕ∞)
Theorem	nnnninf2 7125*	Canonical embedding of suc ω into ℕ∞. (Contributed by BJ, 10-Aug-2024.)
⊢ (𝑁 ∈ suc ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈ ℕ∞)
Theorem	nnnninfeq 7126*	Mapping of a natural number to an element of ℕ∞. (Contributed by Jim Kingdon, 4-Aug-2022.)
⊢ (𝜑 → 𝑃 ∈ ℕ∞)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑁 (𝑃‘𝑥) = 1o)    &   ⊢ (𝜑 → (𝑃‘𝑁) = ∅)    ⇒   ⊢ (𝜑 → 𝑃 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)))
Theorem	nnnninfeq2 7127*	Mapping of a natural number to an element of ℕ∞. Similar to nnnninfeq 7126 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 7128*	Lemma for nninfisol 7131. The case where 𝑁 is zero. (Contributed by Jim Kingdon, 13-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ ℕ∞)    &   ⊢ (𝜑 → (𝑋‘𝑁) = ∅)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → 𝑁 = ∅)    ⇒   ⊢ (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
Theorem	nninfisollemne 7129*	Lemma for nninfisol 7131. A case where 𝑁 is a successor and 𝑁 and 𝑋 are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ ℕ∞)    &   ⊢ (𝜑 → (𝑋‘𝑁) = ∅)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ≠ ∅)    &   ⊢ (𝜑 → (𝑋‘∪ 𝑁) = ∅)    ⇒   ⊢ (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
Theorem	nninfisollemeq 7130*	Lemma for nninfisol 7131. The case where 𝑁 is a successor and 𝑁 and 𝑋 are equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
⊢ (𝜑 → 𝑋 ∈ ℕ∞)    &   ⊢ (𝜑 → (𝑋‘𝑁) = ∅)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ≠ ∅)    &   ⊢ (𝜑 → (𝑋‘∪ 𝑁) = 1o)    ⇒   ⊢ (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
Theorem	nninfisol 7131*	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.)
⊢ ((𝑁 ∈ ω ∧ 𝑋 ∈ ℕ∞) → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)
2.6.38  Omniscient sets
Syntax	comni 7132	Extend class definition to include the class of omniscient sets.
class Omni
Definition	df-omni 7133*	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 7134*	The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓(𝑓:𝐴⟶2o → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o))))
Theorem	isomnimap 7135*	The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)))
Theorem	enomnilem 7136	Lemma for enomni 7137. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Omni → 𝐵 ∈ Omni))
Theorem	enomni 7137	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 6431 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 7138	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 7139	Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 7140. (Contributed by Jim Kingdon, 29-Jun-2022.)
⊢ (EXMID → ∀𝑥 𝑥 ∈ Omni)
Theorem	exmidomni 7140	Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.)
⊢ (EXMID ↔ ∀𝑥 𝑥 ∈ Omni)
Theorem	exmidlpo 7141	Excluded middle implies the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 29-Mar-2023.)
⊢ (EXMID → ω ∈ Omni)
Theorem	fodjuomnilemdc 7142*	Lemma for fodjuomni 7147. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.)
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑂) → DECID ∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧))
Theorem	fodjuf 7143*	Lemma for fodjuomni 7147 and fodjumkv 7158. 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 7144*	Lemma for fodjuomni 7147 and fodjumkv 7158. 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 7145*	Lemma for fodjuomni 7147 and fodjumkv 7158. 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 7146*	Lemma for fodjuomni 7147. The final result with 𝑃 expressed as a local definition. (Contributed by Jim Kingdon, 29-Jul-2022.)
⊢ (𝜑 → 𝑂 ∈ Omni)    &   ⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵))    &   ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1o))    ⇒   ⊢ (𝜑 → (∃𝑥 𝑥 ∈ 𝐴 ∨ 𝐴 = ∅))
Theorem	fodjuomni 7147*	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 7148*	The decidability condition in ctssdc 7112 is needed. More specifically, ctssdc 7112 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 7149	Extend class definition to include the class of Markov sets.
class Markov
Definition	df-markov 7150*	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 7151*	The predicate of being Markov. (Contributed by Jim Kingdon, 18-Mar-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))))
Theorem	ismkvmap 7152*	The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 18-Mar-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)))
Theorem	ismkvnex 7153*	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 7154	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 7155	Excluded middle implies Markov's Principle (MP). (Contributed by Jim Kingdon, 4-Apr-2023.)
⊢ (EXMID → ω ∈ Markov)
Theorem	mkvprop 7156*	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 7157*	Lemma for fodjumkv 7158. The final result with 𝑃 expressed as a local definition. (Contributed by Jim Kingdon, 25-Mar-2023.)
⊢ (𝜑 → 𝑀 ∈ Markov)    &   ⊢ (𝜑 → 𝐹:𝑀–onto→(𝐴 ⊔ 𝐵))    &   ⊢ 𝑃 = (𝑦 ∈ 𝑀 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1o))    ⇒   ⊢ (𝜑 → (𝐴 ≠ ∅ → ∃𝑥 𝑥 ∈ 𝐴))
Theorem	fodjumkv 7158*	A condition which ensures that a nonempty set is inhabited. (Contributed by Jim Kingdon, 25-Mar-2023.)
⊢ (𝜑 → 𝑀 ∈ Markov)    &   ⊢ (𝜑 → 𝐹:𝑀–onto→(𝐴 ⊔ 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 ≠ ∅ → ∃𝑥 𝑥 ∈ 𝐴))
Theorem	enmkvlem 7159	Lemma for enmkv 7160. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Markov → 𝐵 ∈ Markov))
Theorem	enmkv 7160	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 6431 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 7161	Extend class definition to include the class of weakly omniscient sets.
class WOmni
Definition	df-womni 7162*	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 7163*	The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓(𝑓:𝐴⟶2o → DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)))
Theorem	iswomnimap 7164*	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 7165	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 7166	LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7165. There is an analogue in terms of analytic omniscience principles at tridceq 14807. (Contributed by Jim Kingdon, 24-Jul-2024.)
⊢ (ω ∈ Omni → ω ∈ WOmni)
Theorem	enwomnilem 7167	Lemma for enwomni 7168. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ WOmni → 𝐵 ∈ WOmni))
Theorem	enwomni 7168	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 6431 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 7169*	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 7170*	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 7171*	Lemma for nninfwlpor 7172. The result. (Contributed by Jim Kingdon, 7-Dec-2024.)
⊢ (𝜑 → 𝑋:ω⟶2o)    &   ⊢ (𝜑 → 𝑌:ω⟶2o)    &   ⊢ 𝐷 = (𝑖 ∈ ω ↦ if((𝑋‘𝑖) = (𝑌‘𝑖), 1o, ∅))    &   ⊢ (𝜑 → ω ∈ WOmni)    ⇒   ⊢ (𝜑 → DECID 𝑋 = 𝑌)
Theorem	nninfwlpor 7172*	The Weak Limited Principle of Omniscience (WLPO) implies that equality for ℕ∞ is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.)
⊢ (ω ∈ WOmni → ∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦)
Theorem	nninfwlpoimlemg 7173*	Lemma for nninfwlpoim 7176. (Contributed by Jim Kingdon, 8-Dec-2024.)
⊢ (𝜑 → 𝐹:ω⟶2o)    &   ⊢ 𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅, 1o))    ⇒   ⊢ (𝜑 → 𝐺 ∈ ℕ∞)
Theorem	nninfwlpoimlemginf 7174*	Lemma for nninfwlpoim 7176. (Contributed by Jim Kingdon, 8-Dec-2024.)
⊢ (𝜑 → 𝐹:ω⟶2o)    &   ⊢ 𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅, 1o))    ⇒   ⊢ (𝜑 → (𝐺 = (𝑖 ∈ ω ↦ 1o) ↔ ∀𝑛 ∈ ω (𝐹‘𝑛) = 1o))
Theorem	nninfwlpoimlemdc 7175*	Lemma for nninfwlpoim 7176. (Contributed by Jim Kingdon, 8-Dec-2024.)
⊢ (𝜑 → 𝐹:ω⟶2o)    &   ⊢ 𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅, 1o))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦)    ⇒   ⊢ (𝜑 → DECID ∀𝑛 ∈ ω (𝐹‘𝑛) = 1o)
Theorem	nninfwlpoim 7176*	Decidable equality for ℕ∞ implies the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.)
⊢ (∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦 → ω ∈ WOmni)
Theorem	nninfwlpo 7177*	Decidability of equality for ℕ∞ is equivalent to the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 3-Dec-2024.)
⊢ (∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦 ↔ ω ∈ WOmni)
2.6.41  Cardinal numbers
Syntax	ccrd 7178	Extend class definition to include the cardinal size function.
class card
Definition	df-card 7179*	Define the cardinal number function. The cardinal number of a set is the least ordinal number equinumerous to it. In other words, it is the "size" of the set. Definition of [Enderton] p. 197. Our notation is from Enderton. Other textbooks often use a double bar over the set to express this function. (Contributed by NM, 21-Oct-2003.)
⊢ card = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝑥})
Theorem	cardcl 7180*	The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.)
⊢ (∃𝑦 ∈ On 𝑦 ≈ 𝐴 → (card‘𝐴) ∈ On)
Theorem	isnumi 7181	A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ On ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ dom card)
Theorem	finnum 7182	Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card)
Theorem	onenon 7183	Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ On → 𝐴 ∈ dom card)
Theorem	cardval3ex 7184*	The value of (card‘𝐴). (Contributed by Jim Kingdon, 30-Aug-2021.)
⊢ (∃𝑥 ∈ On 𝑥 ≈ 𝐴 → (card‘𝐴) = ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴})
Theorem	oncardval 7185*	The value of the cardinal number function with an ordinal number as its argument. (Contributed by NM, 24-Nov-2003.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ (𝐴 ∈ On → (card‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝑥 ≈ 𝐴})
Theorem	cardonle 7186	The cardinal of an ordinal number is less than or equal to the ordinal number. Proposition 10.6(3) of [TakeutiZaring] p. 85. (Contributed by NM, 22-Oct-2003.)
⊢ (𝐴 ∈ On → (card‘𝐴) ⊆ 𝐴)
Theorem	card0 7187	The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.)
⊢ (card‘∅) = ∅
Theorem	carden2bex 7188*	If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.)
⊢ ((𝐴 ≈ 𝐵 ∧ ∃𝑥 ∈ On 𝑥 ≈ 𝐴) → (card‘𝐴) = (card‘𝐵))
Theorem	pm54.43 7189	Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.)
⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2o))
Theorem	pr2nelem 7190	Lemma for pr2ne 7191. (Contributed by FL, 17-Aug-2008.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o)
Theorem	pr2ne 7191	If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2o ↔ 𝐴 ≠ 𝐵))
Theorem	exmidonfinlem 7192*	Lemma for exmidonfin 7193. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
⊢ 𝐴 = {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}}    ⇒   ⊢ (ω = (On ∩ Fin) → DECID 𝜑)
Theorem	exmidonfin 7193	If a finite ordinal is a natural number, excluded middle follows. That excluded middle implies that a finite ordinal is a natural number is proved in the Metamath Proof Explorer. That a natural number is a finite ordinal is shown at nnfi 6872 and nnon 4610. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
⊢ (ω = (On ∩ Fin) → EXMID)
Theorem	en2eleq 7194	Express a set of pair cardinality as the unordered pair of a given element and the other element. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → 𝑃 = {𝑋, ∪ (𝑃 ∖ {𝑋})})
Theorem	en2other2 7195	Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → ∪ (𝑃 ∖ {∪ (𝑃 ∖ {𝑋})}) = 𝑋)
Theorem	dju1p1e2 7196	Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.)
⊢ (1o ⊔ 1o) ≈ 2o
Theorem	infpwfidom 7197	The collection of finite subsets of a set dominates the set. (We use the weaker sethood assumption (𝒫 𝐴 ∩ Fin) ∈ V because this theorem also implies that 𝐴 is a set if 𝒫 𝐴 ∩ Fin is.) (Contributed by Mario Carneiro, 17-May-2015.)
⊢ ((𝒫 𝐴 ∩ Fin) ∈ V → 𝐴 ≼ (𝒫 𝐴 ∩ Fin))
Theorem	exmidfodomrlemeldju 7198	Lemma for exmidfodomr 7203. A variant of djur 7068. (Contributed by Jim Kingdon, 2-Jul-2022.)
⊢ (𝜑 → 𝐴 ⊆ 1o)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1o))    ⇒   ⊢ (𝜑 → (𝐵 = (inl‘∅) ∨ 𝐵 = (inr‘∅)))
Theorem	exmidfodomrlemreseldju 7199	Lemma for exmidfodomrlemrALT 7202. A variant of eldju 7067. (Contributed by Jim Kingdon, 9-Jul-2022.)
⊢ (𝜑 → 𝐴 ⊆ 1o)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1o))    ⇒   ⊢ (𝜑 → ((∅ ∈ 𝐴 ∧ 𝐵 = ((inl ↾ 𝐴)‘∅)) ∨ 𝐵 = ((inr ↾ 1o)‘∅)))
Theorem	exmidfodomrlemim 7200*	Excluded middle implies the existence of a mapping from any set onto any inhabited set that it dominates. Proposition 1.1 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.)
⊢ (EXMID → ∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦))