![]() |
Intuitionistic Logic Explorer Theorem List (p. 72 of 147) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | djudm 7101 | 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 7102 | 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 𝑆)) | ||
Theorem | 0ct 7103 | 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 7104* | Lemma for ctm 7105. One of the directions of the biconditional. (Contributed by Jim Kingdon, 16-Mar-2023.) |
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∃𝑓 𝑓:ω–onto→𝐴 → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))) | ||
Theorem | ctm 7105* | 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 7106* | Lemma for ctssdc 7109. The ¬ ∅ ∈ 𝑆 case. (Contributed by Jim Kingdon, 16-Aug-2023.) |
⊢ (𝜑 → 𝑆 ⊆ ω) & ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆) & ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴) & ⊢ (𝜑 → ¬ ∅ ∈ 𝑆) ⇒ ⊢ (𝜑 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)) | ||
Theorem | ctssdccl 7107* | A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 7109 but expressed in terms of classes rather than ∃. (Contributed by Jim Kingdon, 30-Oct-2023.) |
⊢ (𝜑 → 𝐹:ω–onto→(𝐴 ⊔ 1o)) & ⊢ 𝑆 = {𝑥 ∈ ω ∣ (𝐹‘𝑥) ∈ (inl “ 𝐴)} & ⊢ 𝐺 = (◡inl ∘ 𝐹) ⇒ ⊢ (𝜑 → (𝑆 ⊆ ω ∧ 𝐺:𝑆–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)) | ||
Theorem | ctssdclemr 7108* | Lemma for ctssdc 7109. Showing that our usual definition of countable implies the alternate one. (Contributed by Jim Kingdon, 16-Aug-2023.) |
⊢ (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑠)) | ||
Theorem | ctssdc 7109* | 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 7145. (Contributed by Jim Kingdon, 15-Aug-2023.) |
⊢ (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑠) ↔ ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o)) | ||
Theorem | enumctlemm 7110* | Lemma for enumct 7111. The case where 𝑁 is greater than zero. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊢ (𝜑 → 𝐹:𝑁–onto→𝐴) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → ∅ ∈ 𝑁) & ⊢ 𝐺 = (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑁, (𝐹‘𝑘), (𝐹‘∅))) ⇒ ⊢ (𝜑 → 𝐺:ω–onto→𝐴) | ||
Theorem | enumct 7111* | 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 7112* | A finite set is countable. (Contributed by Jim Kingdon, 17-Mar-2023.) |
⊢ (𝐴 ∈ Fin → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)) | ||
Theorem | omct 7113 | ω is countable. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊢ ∃𝑓 𝑓:ω–onto→(ω ⊔ 1o) | ||
Theorem | ctfoex 7114* | A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.) |
⊢ (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → 𝐴 ∈ V) | ||
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 7115 | Set of nonincreasing sequences in 2o ↑𝑚 ω. |
class ℕ∞ | ||
Definition | df-nninf 7116* | 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 9236 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 6428) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.) |
⊢ ℕ∞ = {𝑓 ∈ (2o ↑𝑚 ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓‘𝑖)} | ||
Theorem | nninfex 7117 | ℕ∞ is a set. (Contributed by Jim Kingdon, 10-Aug-2022.) |
⊢ ℕ∞ ∈ V | ||
Theorem | nninff 7118 | An element of ℕ∞ is a sequence of zeroes and ones. (Contributed by Jim Kingdon, 4-Aug-2022.) |
⊢ (𝐴 ∈ ℕ∞ → 𝐴:ω⟶2o) | ||
Theorem | infnninf 7119 | 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 4672 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.) |
⊢ (𝑖 ∈ ω ↦ 1o) ∈ ℕ∞ | ||
Theorem | infnninfOLD 7120 | Obsolete version of infnninf 7119 as of 10-Aug-2024. (Contributed by Jim Kingdon, 14-Jul-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (ω × {1o}) ∈ ℕ∞ | ||
Theorem | nnnninf 7121* | 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 7122. (Contributed by Jim Kingdon, 14-Jul-2022.) |
⊢ (𝑁 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈ ℕ∞) | ||
Theorem | nnnninf2 7122* | Canonical embedding of suc ω into ℕ∞. (Contributed by BJ, 10-Aug-2024.) |
⊢ (𝑁 ∈ suc ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈ ℕ∞) | ||
Theorem | nnnninfeq 7123* | Mapping of a natural number to an element of ℕ∞. (Contributed by Jim Kingdon, 4-Aug-2022.) |
⊢ (𝜑 → 𝑃 ∈ ℕ∞) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑁 (𝑃‘𝑥) = 1o) & ⊢ (𝜑 → (𝑃‘𝑁) = ∅) ⇒ ⊢ (𝜑 → 𝑃 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))) | ||
Theorem | nnnninfeq2 7124* | Mapping of a natural number to an element of ℕ∞. Similar to nnnninfeq 7123 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 7125* | Lemma for nninfisol 7128. The case where 𝑁 is zero. (Contributed by Jim Kingdon, 13-Sep-2024.) |
⊢ (𝜑 → 𝑋 ∈ ℕ∞) & ⊢ (𝜑 → (𝑋‘𝑁) = ∅) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → 𝑁 = ∅) ⇒ ⊢ (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) | ||
Theorem | nninfisollemne 7126* | Lemma for nninfisol 7128. A case where 𝑁 is a successor and 𝑁 and 𝑋 are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.) |
⊢ (𝜑 → 𝑋 ∈ ℕ∞) & ⊢ (𝜑 → (𝑋‘𝑁) = ∅) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → 𝑁 ≠ ∅) & ⊢ (𝜑 → (𝑋‘∪ 𝑁) = ∅) ⇒ ⊢ (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) | ||
Theorem | nninfisollemeq 7127* | Lemma for nninfisol 7128. The case where 𝑁 is a successor and 𝑁 and 𝑋 are equal. (Contributed by Jim Kingdon, 13-Sep-2024.) |
⊢ (𝜑 → 𝑋 ∈ ℕ∞) & ⊢ (𝜑 → (𝑋‘𝑁) = ∅) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → 𝑁 ≠ ∅) & ⊢ (𝜑 → (𝑋‘∪ 𝑁) = 1o) ⇒ ⊢ (𝜑 → DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) | ||
Theorem | nninfisol 7128* | 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, ∅)) = 𝑋) | ||
Syntax | comni 7129 | Extend class definition to include the class of omniscient sets. |
class Omni | ||
Definition | df-omni 7130* |
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 7131* | The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓(𝑓:𝐴⟶2o → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)))) | ||
Theorem | isomnimap 7132* | The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o))) | ||
Theorem | enomnilem 7133 | Lemma for enomni 7134. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Omni → 𝐵 ∈ Omni)) | ||
Theorem | enomni 7134 | 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 6428 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 7135 | 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 7136 | Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 7137. (Contributed by Jim Kingdon, 29-Jun-2022.) |
⊢ (EXMID → ∀𝑥 𝑥 ∈ Omni) | ||
Theorem | exmidomni 7137 | Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.) |
⊢ (EXMID ↔ ∀𝑥 𝑥 ∈ Omni) | ||
Theorem | exmidlpo 7138 | Excluded middle implies the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 29-Mar-2023.) |
⊢ (EXMID → ω ∈ Omni) | ||
Theorem | fodjuomnilemdc 7139* | Lemma for fodjuomni 7144. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑂) → DECID ∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧)) | ||
Theorem | fodjuf 7140* | Lemma for fodjuomni 7144 and fodjumkv 7155. 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 7141* | Lemma for fodjuomni 7144 and fodjumkv 7155. 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 7142* | Lemma for fodjuomni 7144 and fodjumkv 7155. 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 7143* | Lemma for fodjuomni 7144. The final result with 𝑃 expressed as a local definition. (Contributed by Jim Kingdon, 29-Jul-2022.) |
⊢ (𝜑 → 𝑂 ∈ Omni) & ⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1o)) ⇒ ⊢ (𝜑 → (∃𝑥 𝑥 ∈ 𝐴 ∨ 𝐴 = ∅)) | ||
Theorem | fodjuomni 7144* | 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 7145* | The decidability condition in ctssdc 7109 is needed. More specifically, ctssdc 7109 minus that condition, plus the Limited Principle of Omniscience (LPO), implies excluded middle. (Contributed by Jim Kingdon, 15-Aug-2023.) |
⊢ ((𝑦 ⊆ ω ∧ ∃𝑓 𝑓:𝑦–onto→𝑥) → ∃𝑓 𝑓:ω–onto→(𝑥 ⊔ 1o)) & ⊢ ω ∈ Omni ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
Syntax | cmarkov 7146 | Extend class definition to include the class of Markov sets. |
class Markov | ||
Definition | df-markov 7147* |
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 7148* | The predicate of being Markov. (Contributed by Jim Kingdon, 18-Mar-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)))) | ||
Theorem | ismkvmap 7149* | The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 18-Mar-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))) | ||
Theorem | ismkvnex 7150* | 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 7151 | 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 7152 | Excluded middle implies Markov's Principle (MP). (Contributed by Jim Kingdon, 4-Apr-2023.) |
⊢ (EXMID → ω ∈ Markov) | ||
Theorem | mkvprop 7153* | 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 7154* | Lemma for fodjumkv 7155. The final result with 𝑃 expressed as a local definition. (Contributed by Jim Kingdon, 25-Mar-2023.) |
⊢ (𝜑 → 𝑀 ∈ Markov) & ⊢ (𝜑 → 𝐹:𝑀–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑀 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1o)) ⇒ ⊢ (𝜑 → (𝐴 ≠ ∅ → ∃𝑥 𝑥 ∈ 𝐴)) | ||
Theorem | fodjumkv 7155* | A condition which ensures that a nonempty set is inhabited. (Contributed by Jim Kingdon, 25-Mar-2023.) |
⊢ (𝜑 → 𝑀 ∈ Markov) & ⊢ (𝜑 → 𝐹:𝑀–onto→(𝐴 ⊔ 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 ≠ ∅ → ∃𝑥 𝑥 ∈ 𝐴)) | ||
Theorem | enmkvlem 7156 | Lemma for enmkv 7157. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Markov → 𝐵 ∈ Markov)) | ||
Theorem | enmkv 7157 | 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 6428 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)) | ||
Syntax | cwomni 7158 | Extend class definition to include the class of weakly omniscient sets. |
class WOmni | ||
Definition | df-womni 7159* |
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 7160* | The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓(𝑓:𝐴⟶2o → DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o))) | ||
Theorem | iswomnimap 7161* | 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 7162 | 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 7163 | LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7162. There is an analogue in terms of analytic omniscience principles at tridceq 14664. (Contributed by Jim Kingdon, 24-Jul-2024.) |
⊢ (ω ∈ Omni → ω ∈ WOmni) | ||
Theorem | enwomnilem 7164 | Lemma for enwomni 7165. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ WOmni → 𝐵 ∈ WOmni)) | ||
Theorem | enwomni 7165 | 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 6428 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 7166* | 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 7167* | 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 7168* | Lemma for nninfwlpor 7169. The result. (Contributed by Jim Kingdon, 7-Dec-2024.) |
⊢ (𝜑 → 𝑋:ω⟶2o) & ⊢ (𝜑 → 𝑌:ω⟶2o) & ⊢ 𝐷 = (𝑖 ∈ ω ↦ if((𝑋‘𝑖) = (𝑌‘𝑖), 1o, ∅)) & ⊢ (𝜑 → ω ∈ WOmni) ⇒ ⊢ (𝜑 → DECID 𝑋 = 𝑌) | ||
Theorem | nninfwlpor 7169* | The Weak Limited Principle of Omniscience (WLPO) implies that equality for ℕ∞ is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.) |
⊢ (ω ∈ WOmni → ∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦) | ||
Theorem | nninfwlpoimlemg 7170* | Lemma for nninfwlpoim 7173. (Contributed by Jim Kingdon, 8-Dec-2024.) |
⊢ (𝜑 → 𝐹:ω⟶2o) & ⊢ 𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅, 1o)) ⇒ ⊢ (𝜑 → 𝐺 ∈ ℕ∞) | ||
Theorem | nninfwlpoimlemginf 7171* | Lemma for nninfwlpoim 7173. (Contributed by Jim Kingdon, 8-Dec-2024.) |
⊢ (𝜑 → 𝐹:ω⟶2o) & ⊢ 𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅, 1o)) ⇒ ⊢ (𝜑 → (𝐺 = (𝑖 ∈ ω ↦ 1o) ↔ ∀𝑛 ∈ ω (𝐹‘𝑛) = 1o)) | ||
Theorem | nninfwlpoimlemdc 7172* | Lemma for nninfwlpoim 7173. (Contributed by Jim Kingdon, 8-Dec-2024.) |
⊢ (𝜑 → 𝐹:ω⟶2o) & ⊢ 𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅, 1o)) & ⊢ (𝜑 → ∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦) ⇒ ⊢ (𝜑 → DECID ∀𝑛 ∈ ω (𝐹‘𝑛) = 1o) | ||
Theorem | nninfwlpoim 7173* | Decidable equality for ℕ∞ implies the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.) |
⊢ (∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦 → ω ∈ WOmni) | ||
Theorem | nninfwlpo 7174* | Decidability of equality for ℕ∞ is equivalent to the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 3-Dec-2024.) |
⊢ (∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦 ↔ ω ∈ WOmni) | ||
Syntax | ccrd 7175 | Extend class definition to include the cardinal size function. |
class card | ||
Definition | df-card 7176* | 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 7177* | The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.) |
⊢ (∃𝑦 ∈ On 𝑦 ≈ 𝐴 → (card‘𝐴) ∈ On) | ||
Theorem | isnumi 7178 | A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ On ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ dom card) | ||
Theorem | finnum 7179 | Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card) | ||
Theorem | onenon 7180 | Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ On → 𝐴 ∈ dom card) | ||
Theorem | cardval3ex 7181* | The value of (card‘𝐴). (Contributed by Jim Kingdon, 30-Aug-2021.) |
⊢ (∃𝑥 ∈ On 𝑥 ≈ 𝐴 → (card‘𝐴) = ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴}) | ||
Theorem | oncardval 7182* | 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 7183 | 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 7184 | The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.) |
⊢ (card‘∅) = ∅ | ||
Theorem | carden2bex 7185* | If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.) |
⊢ ((𝐴 ≈ 𝐵 ∧ ∃𝑥 ∈ On 𝑥 ≈ 𝐴) → (card‘𝐴) = (card‘𝐵)) | ||
Theorem | pm54.43 7186 | Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.) |
⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2o)) | ||
Theorem | pr2nelem 7187 | Lemma for pr2ne 7188. (Contributed by FL, 17-Aug-2008.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o) | ||
Theorem | pr2ne 7188 | If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2o ↔ 𝐴 ≠ 𝐵)) | ||
Theorem | exmidonfinlem 7189* | Lemma for exmidonfin 7190. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
⊢ 𝐴 = {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ⇒ ⊢ (ω = (On ∩ Fin) → DECID 𝜑) | ||
Theorem | exmidonfin 7190 | 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 6869 and nnon 4608. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
⊢ (ω = (On ∩ Fin) → EXMID) | ||
Theorem | en2eleq 7191 | 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 7192 | 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 7193 | Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊢ (1o ⊔ 1o) ≈ 2o | ||
Theorem | infpwfidom 7194 | 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 7195 | Lemma for exmidfodomr 7200. A variant of djur 7065. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 1o) & ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1o)) ⇒ ⊢ (𝜑 → (𝐵 = (inl‘∅) ∨ 𝐵 = (inr‘∅))) | ||
Theorem | exmidfodomrlemreseldju 7196 | Lemma for exmidfodomrlemrALT 7199. A variant of eldju 7064. (Contributed by Jim Kingdon, 9-Jul-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 1o) & ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1o)) ⇒ ⊢ (𝜑 → ((∅ ∈ 𝐴 ∧ 𝐵 = ((inl ↾ 𝐴)‘∅)) ∨ 𝐵 = ((inr ↾ 1o)‘∅))) | ||
Theorem | exmidfodomrlemim 7197* | 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→𝑦)) | ||
Theorem | exmidfodomrlemr 7198* | The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID) | ||
Theorem | exmidfodomrlemrALT 7199* | The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. An alternative proof of exmidfodomrlemr 7198. In particular, this proof uses eldju 7064 instead of djur 7065 and avoids djulclb 7051. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.) |
⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID) | ||
Theorem | exmidfodomr 7200* | Excluded middle is equivalent to the existence of a mapping from any set onto any inhabited set that it dominates. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊢ (EXMID ↔ ∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |