Home | Intuitionistic Logic Explorer Theorem List (p. 71 of 135) | < 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 | djuinj 7001 | 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 7002 | 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→(∅ ⊔ 1_{o}) | ||
Theorem | ctmlemr 7003* | Lemma for ctm 7004. One of the directions of the biconditional. (Contributed by Jim Kingdon, 16-Mar-2023.) |
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∃𝑓 𝑓:ω–onto→𝐴 → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1_{o}))) | ||
Theorem | ctm 7004* | Two equivalent definitions of countable for an inhabited set. Remark of [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1_{o}) ↔ ∃𝑓 𝑓:ω–onto→𝐴)) | ||
Theorem | ctssdclemn0 7005* | Lemma for ctssdc 7008. The ¬ ∅ ∈ 𝑆 case. (Contributed by Jim Kingdon, 16-Aug-2023.) |
⊢ (𝜑 → 𝑆 ⊆ ω) & ⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆) & ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴) & ⊢ (𝜑 → ¬ ∅ ∈ 𝑆) ⇒ ⊢ (𝜑 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1_{o})) | ||
Theorem | ctssdccl 7006* | A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 7008 but expressed in terms of classes rather than ∃. (Contributed by Jim Kingdon, 30-Oct-2023.) |
⊢ (𝜑 → 𝐹:ω–onto→(𝐴 ⊔ 1_{o})) & ⊢ 𝑆 = {𝑥 ∈ ω ∣ (𝐹‘𝑥) ∈ (inl “ 𝐴)} & ⊢ 𝐺 = (^{◡}inl ∘ 𝐹) ⇒ ⊢ (𝜑 → (𝑆 ⊆ ω ∧ 𝐺:𝑆–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑆)) | ||
Theorem | ctssdclemr 7007* | Lemma for ctssdc 7008. Showing that our usual definition of countable implies the alternate one. (Contributed by Jim Kingdon, 16-Aug-2023.) |
⊢ (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1_{o}) → ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑠)) | ||
Theorem | ctssdc 7008* | 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 7034. (Contributed by Jim Kingdon, 15-Aug-2023.) |
⊢ (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑠) ↔ ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1_{o})) | ||
Theorem | enumctlemm 7009* | Lemma for enumct 7010. The case where 𝑁 is greater than zero. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊢ (𝜑 → 𝐹:𝑁–onto→𝐴) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → ∅ ∈ 𝑁) & ⊢ 𝐺 = (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑁, (𝐹‘𝑘), (𝐹‘∅))) ⇒ ⊢ (𝜑 → 𝐺:ω–onto→𝐴) | ||
Theorem | enumct 7010* | 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→(𝐴 ⊔ 1_{o}) per [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊢ (∃𝑛 ∈ ω ∃𝑓 𝑓:𝑛–onto→𝐴 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1_{o})) | ||
Theorem | finct 7011* | A finite set is countable. (Contributed by Jim Kingdon, 17-Mar-2023.) |
⊢ (𝐴 ∈ Fin → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1_{o})) | ||
Theorem | omct 7012 | ω is countable. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊢ ∃𝑓 𝑓:ω–onto→(ω ⊔ 1_{o}) | ||
Theorem | ctfoex 7013* | A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.) |
⊢ (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1_{o}) → 𝐴 ∈ V) | ||
Syntax | comni 7014 | Extend class definition to include the class of omniscient sets. |
class Omni | ||
Syntax | xnninf 7015 | Set of nonincreasing sequences in 2_{o} ↑_{𝑚} ω. |
class ℕ_{∞} | ||
Definition | df-omni 7016* |
An omniscient set is one where we can decide whether a predicate (here
represented by a function 𝑓) holds (is equal to 1_{o}) 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 = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2_{o} → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1_{o}))} | ||
Definition | df-nninf 7017* | Define the set of nonincreasing sequences in 2_{o} ↑_{𝑚} ω. 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 9085 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 2_{o} = {∅, 1_{o}} (df2o3 6336) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.) |
⊢ ℕ_{∞} = {𝑓 ∈ (2_{o} ↑_{𝑚} ω) ∣ ∀𝑖 ∈ ω (𝑓‘suc 𝑖) ⊆ (𝑓‘𝑖)} | ||
Theorem | isomni 7018* | The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓(𝑓:𝐴⟶2_{o} → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1_{o})))) | ||
Theorem | isomnimap 7019* | The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ (2_{o} ↑_{𝑚} 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1_{o}))) | ||
Theorem | enomnilem 7020 | Lemma for enomni 7021. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Omni → 𝐵 ∈ Omni)) | ||
Theorem | enomni 7021 | 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 6336 says that 2_{o} = {∅, 1_{o}} whereas the corresponding relationship does not exist between 2 and {0, 1}. (Contributed by Jim Kingdon, 13-Jul-2022.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Omni ↔ 𝐵 ∈ Omni)) | ||
Theorem | finomni 7022 | 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 7023 | Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 7024. (Contributed by Jim Kingdon, 29-Jun-2022.) |
⊢ (EXMID → ∀𝑥 𝑥 ∈ Omni) | ||
Theorem | exmidomni 7024 | Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.) |
⊢ (EXMID ↔ ∀𝑥 𝑥 ∈ Omni) | ||
Theorem | exmidlpo 7025 | Excluded middle implies the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 29-Mar-2023.) |
⊢ (EXMID → ω ∈ Omni) | ||
Theorem | fodjuomnilemdc 7026* | Lemma for fodjuomni 7031. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑂) → DECID ∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧)) | ||
Theorem | fodjuf 7027* | Lemma for fodjuomni 7031 and fodjumkv 7044. Domain and range of 𝑃. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1_{o})) & ⊢ (𝜑 → 𝑂 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑃 ∈ (2_{o} ↑_{𝑚} 𝑂)) | ||
Theorem | fodjum 7028* | Lemma for fodjuomni 7031 and fodjumkv 7044. A condition which shows that 𝐴 is inhabited. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1_{o})) & ⊢ (𝜑 → ∃𝑤 ∈ 𝑂 (𝑃‘𝑤) = ∅) ⇒ ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | fodju0 7029* | Lemma for fodjuomni 7031 and fodjumkv 7044. A condition which shows that 𝐴 is empty. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1_{o})) & ⊢ (𝜑 → ∀𝑤 ∈ 𝑂 (𝑃‘𝑤) = 1_{o}) ⇒ ⊢ (𝜑 → 𝐴 = ∅) | ||
Theorem | fodjuomnilemres 7030* | Lemma for fodjuomni 7031. The final result with 𝑃 expressed as a local definition. (Contributed by Jim Kingdon, 29-Jul-2022.) |
⊢ (𝜑 → 𝑂 ∈ Omni) & ⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1_{o})) ⇒ ⊢ (𝜑 → (∃𝑥 𝑥 ∈ 𝐴 ∨ 𝐴 = ∅)) | ||
Theorem | fodjuomni 7031* | 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 | infnninf 7032 | The point at infinity in ℕ_{∞} (the constant sequence equal to 1_{o}). (Contributed by Jim Kingdon, 14-Jul-2022.) |
⊢ (ω × {1_{o}}) ∈ ℕ_{∞} | ||
Theorem | nnnninf 7033* | Elements of ℕ_{∞} corresponding to natural numbers. The natural number 𝑁 corresponds to a sequence of 𝑁 ones followed by zeroes. Contrast to a sequence which is all ones as seen at infnninf 7032. Remark/TODO: the theorem still holds if 𝑁 = ω, that is, the antecedent could be weakened to 𝑁 ∈ suc ω. (Contributed by Jim Kingdon, 14-Jul-2022.) |
⊢ (𝑁 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1_{o}, ∅)) ∈ ℕ_{∞}) | ||
Theorem | ctssexmid 7034* | The decidability condition in ctssdc 7008 is needed. More specifically, ctssdc 7008 minus that condition, plus the Limited Principle of Omniscience (LPO), implies excluded middle. (Contributed by Jim Kingdon, 15-Aug-2023.) |
⊢ ((𝑦 ⊆ ω ∧ ∃𝑓 𝑓:𝑦–onto→𝑥) → ∃𝑓 𝑓:ω–onto→(𝑥 ⊔ 1_{o})) & ⊢ ω ∈ Omni ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
Syntax | cmarkov 7035 | Extend class definition to include the class of Markov sets. |
class Markov | ||
Definition | df-markov 7036* |
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 1_{o})
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 = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2_{o} → (¬ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1_{o} → ∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅))} | ||
Theorem | ismkv 7037* | The predicate of being Markov. (Contributed by Jim Kingdon, 18-Mar-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓(𝑓:𝐴⟶2_{o} → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1_{o} → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)))) | ||
Theorem | ismkvmap 7038* | The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 18-Mar-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ (2_{o} ↑_{𝑚} 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1_{o} → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))) | ||
Theorem | ismkvnex 7039* | The predicate of being Markov stated in terms of double negation and comparison with 1_{o}. (Contributed by Jim Kingdon, 29-Nov-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ (2_{o} ↑_{𝑚} 𝐴)(¬ ¬ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1_{o} → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1_{o}))) | ||
Theorem | omnimkv 7040 | 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 7041 | Excluded middle implies Markov's Principle (MP). (Contributed by Jim Kingdon, 4-Apr-2023.) |
⊢ (EXMID → ω ∈ Markov) | ||
Theorem | mkvprop 7042* | 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 7043* | Lemma for fodjumkv 7044. The final result with 𝑃 expressed as a local definition. (Contributed by Jim Kingdon, 25-Mar-2023.) |
⊢ (𝜑 → 𝑀 ∈ Markov) & ⊢ (𝜑 → 𝐹:𝑀–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑀 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1_{o})) ⇒ ⊢ (𝜑 → (𝐴 ≠ ∅ → ∃𝑥 𝑥 ∈ 𝐴)) | ||
Theorem | fodjumkv 7044* | A condition which ensures that a nonempty set is inhabited. (Contributed by Jim Kingdon, 25-Mar-2023.) |
⊢ (𝜑 → 𝑀 ∈ Markov) & ⊢ (𝜑 → 𝐹:𝑀–onto→(𝐴 ⊔ 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 ≠ ∅ → ∃𝑥 𝑥 ∈ 𝐴)) | ||
Theorem | enmkvlem 7045 | Lemma for enmkv 7046. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Markov → 𝐵 ∈ Markov)) | ||
Theorem | enmkv 7046 | 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 6336 says that 2_{o} = {∅, 1_{o}} whereas the corresponding relationship does not exist between 2 and {0, 1}. (Contributed by Jim Kingdon, 24-Jun-2024.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Markov ↔ 𝐵 ∈ Markov)) | ||
Syntax | cwomni 7047 | Extend class definition to include the class of weakly omniscient sets. |
class WOmni | ||
Definition | df-womni 7048* |
A weakly omniscient set is one where we can decide whether a predicate
(here represented by a function 𝑓) holds (is equal to 1_{o}) 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 = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2_{o} → DECID ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1_{o})} | ||
Theorem | iswomni 7049* | The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓(𝑓:𝐴⟶2_{o} → DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1_{o}))) | ||
Theorem | iswomnimap 7050* | The predicate of being weakly omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 9-Jun-2024.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ (2_{o} ↑_{𝑚} 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1_{o})) | ||
Theorem | omniwomnimkv 7051 | 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 7052 | LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7051. There is an analogue in terms of analytic omniscience principles at tridceq 13445. (Contributed by Jim Kingdon, 24-Jul-2024.) |
⊢ (ω ∈ Omni → ω ∈ WOmni) | ||
Theorem | enwomnilem 7053 | Lemma for enwomni 7054. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ WOmni → 𝐵 ∈ WOmni)) | ||
Theorem | enwomni 7054 | 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 6336 says that 2_{o} = {∅, 1_{o}} whereas the corresponding relationship does not exist between 2 and {0, 1}. (Contributed by Jim Kingdon, 20-Jun-2024.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ WOmni ↔ 𝐵 ∈ WOmni)) | ||
Syntax | ccrd 7055 | Extend class definition to include the cardinal size function. |
class card | ||
Definition | df-card 7056* | 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 7057* | The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.) |
⊢ (∃𝑦 ∈ On 𝑦 ≈ 𝐴 → (card‘𝐴) ∈ On) | ||
Theorem | isnumi 7058 | A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ On ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ dom card) | ||
Theorem | finnum 7059 | Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card) | ||
Theorem | onenon 7060 | Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ On → 𝐴 ∈ dom card) | ||
Theorem | cardval3ex 7061* | The value of (card‘𝐴). (Contributed by Jim Kingdon, 30-Aug-2021.) |
⊢ (∃𝑥 ∈ On 𝑥 ≈ 𝐴 → (card‘𝐴) = ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴}) | ||
Theorem | oncardval 7062* | 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 7063 | 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 7064 | The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.) |
⊢ (card‘∅) = ∅ | ||
Theorem | carden2bex 7065* | If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.) |
⊢ ((𝐴 ≈ 𝐵 ∧ ∃𝑥 ∈ On 𝑥 ≈ 𝐴) → (card‘𝐴) = (card‘𝐵)) | ||
Theorem | pm54.43 7066 | Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.) |
⊢ ((𝐴 ≈ 1_{o} ∧ 𝐵 ≈ 1_{o}) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2_{o})) | ||
Theorem | pr2nelem 7067 | Lemma for pr2ne 7068. (Contributed by FL, 17-Aug-2008.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2_{o}) | ||
Theorem | pr2ne 7068 | If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2_{o} ↔ 𝐴 ≠ 𝐵)) | ||
Theorem | exmidonfinlem 7069* | Lemma for exmidonfin 7070. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
⊢ 𝐴 = {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ⇒ ⊢ (ω = (On ∩ Fin) → DECID 𝜑) | ||
Theorem | exmidonfin 7070 | 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 6775 and nnon 4532. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
⊢ (ω = (On ∩ Fin) → EXMID) | ||
Theorem | en2eleq 7071 | 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.) |
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2_{o}) → 𝑃 = {𝑋, ∪ (𝑃 ∖ {𝑋})}) | ||
Theorem | en2other2 7072 | Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2_{o}) → ∪ (𝑃 ∖ {∪ (𝑃 ∖ {𝑋})}) = 𝑋) | ||
Theorem | dju1p1e2 7073 | Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊢ (1_{o} ⊔ 1_{o}) ≈ 2_{o} | ||
Theorem | infpwfidom 7074 | 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 7075 | Lemma for exmidfodomr 7080. A variant of djur 6964. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 1_{o}) & ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1_{o})) ⇒ ⊢ (𝜑 → (𝐵 = (inl‘∅) ∨ 𝐵 = (inr‘∅))) | ||
Theorem | exmidfodomrlemreseldju 7076 | Lemma for exmidfodomrlemrALT 7079. A variant of eldju 6963. (Contributed by Jim Kingdon, 9-Jul-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 1_{o}) & ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1_{o})) ⇒ ⊢ (𝜑 → ((∅ ∈ 𝐴 ∧ 𝐵 = ((inl ↾ 𝐴)‘∅)) ∨ 𝐵 = ((inr ↾ 1_{o})‘∅))) | ||
Theorem | exmidfodomrlemim 7077* | 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 7078* | 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 7079* | 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 7078. In particular, this proof uses eldju 6963 instead of djur 6964 and avoids djulclb 6950. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.) |
⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID) | ||
Theorem | exmidfodomr 7080* | 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→𝑦)) | ||
Syntax | wac 7081 | Formula for an abbreviation of the axiom of choice. |
wff CHOICE | ||
Definition | df-ac 7082* |
The expression CHOICE will be used as a
readable shorthand for any
form of the axiom of choice; all concrete forms are long, cryptic, have
dummy variables, or all three, making it useful to have a short name.
Similar to the Axiom of Choice (first form) of [Enderton] p. 49.
There are some decisions about how to write this definition especially around whether ax-setind 4461 is needed to show equivalence to other ways of stating choice, and about whether choice functions are available for nonempty sets or inhabited sets. (Contributed by Mario Carneiro, 22-Feb-2015.) |
⊢ (CHOICE ↔ ∀𝑥∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥)) | ||
Theorem | acfun 7083* | A convenient form of choice. The goal here is to state choice as the existence of a choice function on a set of inhabited sets, while making full use of our notation around functions and function values. (Contributed by Jim Kingdon, 20-Nov-2023.) |
⊢ (𝜑 → CHOICE) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑤 𝑤 ∈ 𝑥) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥)) | ||
Theorem | exmidaclem 7084* | Lemma for exmidac 7085. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.) |
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})} & ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})} & ⊢ 𝐶 = {𝐴, 𝐵} ⇒ ⊢ (CHOICE → EXMID) | ||
Theorem | exmidac 7085 | The axiom of choice implies excluded middle. See acexmid 5782 for more discussion of this theorem and a way of stating it without using CHOICE or EXMID. (Contributed by Jim Kingdon, 21-Nov-2023.) |
⊢ (CHOICE → EXMID) | ||
Theorem | endjudisj 7086 | Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ⊔ 𝐵) ≈ (𝐴 ∪ 𝐵)) | ||
Theorem | djuen 7087 | Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 ⊔ 𝐶) ≈ (𝐵 ⊔ 𝐷)) | ||
Theorem | djuenun 7088 | Disjoint union is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015.) (Revised by Jim Kingdon, 19-Aug-2023.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ⊔ 𝐶) ≈ (𝐵 ∪ 𝐷)) | ||
Theorem | dju1en 7089 | Cardinal addition with cardinal one (which is the same as ordinal one). Used in proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ 𝐴) → (𝐴 ⊔ 1_{o}) ≈ suc 𝐴) | ||
Theorem | dju0en 7090 | Cardinal addition with cardinal zero (the empty set). Part (a1) of proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ⊔ ∅) ≈ 𝐴) | ||
Theorem | xp2dju 7091 | Two times a cardinal number. Exercise 4.56(g) of [Mendelson] p. 258. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (2_{o} × 𝐴) = (𝐴 ⊔ 𝐴) | ||
Theorem | djucomen 7092 | Commutative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 24-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⊔ 𝐵) ≈ (𝐵 ⊔ 𝐴)) | ||
Theorem | djuassen 7093 | Associative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ⊔ 𝐵) ⊔ 𝐶) ≈ (𝐴 ⊔ (𝐵 ⊔ 𝐶))) | ||
Theorem | xpdjuen 7094 | Cardinal multiplication distributes over cardinal addition. Theorem 6I(3) of [Enderton] p. 142. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × (𝐵 ⊔ 𝐶)) ≈ ((𝐴 × 𝐵) ⊔ (𝐴 × 𝐶))) | ||
Theorem | djudoml 7095 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ≼ (𝐴 ⊔ 𝐵)) | ||
Theorem | djudomr 7096 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐵 ≼ (𝐴 ⊔ 𝐵)) | ||
Theorem | pw1on 7097 | The power set of 1_{o} is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.) |
⊢ 𝒫 1_{o} ∈ On | ||
Theorem | pw1dom2 7098 | The power set of 1_{o} dominates 2_{o}. Also see pwpw0ss 3740 which is similar. (Contributed by Jim Kingdon, 21-Sep-2022.) |
⊢ 2_{o} ≼ 𝒫 1_{o} | ||
Theorem | pw1ne0 7099 | The power set of 1_{o} is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.) |
⊢ 𝒫 1_{o} ≠ ∅ | ||
Theorem | pw1ne1 7100 | The power set of 1_{o} is not one. (Contributed by Jim Kingdon, 30-Jul-2024.) |
⊢ 𝒫 1_{o} ≠ 1_{o} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |