Home | Intuitionistic Logic Explorer Theorem List (p. 71 of 133) | < 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 | isomni 7001* | The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓(𝑓:𝐴⟶2o → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)))) | ||
Theorem | isomnimap 7002* | The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ (2o ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o))) | ||
Theorem | enomnilem 7003 | Lemma for enomni 7004. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Omni → 𝐵 ∈ Omni)) | ||
Theorem | enomni 7004 | 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 6320 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 7005 | 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 7006 | Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 7007. (Contributed by Jim Kingdon, 29-Jun-2022.) |
⊢ (EXMID → ∀𝑥 𝑥 ∈ Omni) | ||
Theorem | exmidomni 7007 | Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.) |
⊢ (EXMID ↔ ∀𝑥 𝑥 ∈ Omni) | ||
Theorem | exmidlpo 7008 | Excluded middle implies the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 29-Mar-2023.) |
⊢ (EXMID → ω ∈ Omni) | ||
Theorem | fodjuomnilemdc 7009* | Lemma for fodjuomni 7014. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑂) → DECID ∃𝑧 ∈ 𝐴 (𝐹‘𝑋) = (inl‘𝑧)) | ||
Theorem | fodjuf 7010* | Lemma for fodjuomni 7014 and fodjumkv 7027. 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 7011* | Lemma for fodjuomni 7014 and fodjumkv 7027. 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 7012* | Lemma for fodjuomni 7014 and fodjumkv 7027. 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 7013* | Lemma for fodjuomni 7014. The final result with 𝑃 expressed as a local definition. (Contributed by Jim Kingdon, 29-Jul-2022.) |
⊢ (𝜑 → 𝑂 ∈ Omni) & ⊢ (𝜑 → 𝐹:𝑂–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑂 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1o)) ⇒ ⊢ (𝜑 → (∃𝑥 𝑥 ∈ 𝐴 ∨ 𝐴 = ∅)) | ||
Theorem | fodjuomni 7014* | 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 7015 | The point at infinity in ℕ∞ (the constant sequence equal to 1o). (Contributed by Jim Kingdon, 14-Jul-2022.) |
⊢ (ω × {1o}) ∈ ℕ∞ | ||
Theorem | nnnninf 7016* | 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 7015. Remark/TODO: the theorem still holds if 𝑁 = ω, that is, the antecedent could be weakened to 𝑁 ∈ suc ω. (Contributed by Jim Kingdon, 14-Jul-2022.) |
⊢ (𝑁 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈ ℕ∞) | ||
Theorem | ctssexmid 7017* | The decidability condition in ctssdc 6991 is needed. More specifically, ctssdc 6991 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 7018 | Extend class definition to include the class of Markov sets. |
class Markov | ||
Definition | df-markov 7019* |
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 7020* | The predicate of being Markov. (Contributed by Jim Kingdon, 18-Mar-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓(𝑓:𝐴⟶2o → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)))) | ||
Theorem | ismkvmap 7021* | The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 18-Mar-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ (2o ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))) | ||
Theorem | ismkvnex 7022* | 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 7023 | 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 7024 | Excluded middle implies Markov's Principle (MP). (Contributed by Jim Kingdon, 4-Apr-2023.) |
⊢ (EXMID → ω ∈ Markov) | ||
Theorem | mkvprop 7025* | 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 7026* | Lemma for fodjumkv 7027. The final result with 𝑃 expressed as a local definition. (Contributed by Jim Kingdon, 25-Mar-2023.) |
⊢ (𝜑 → 𝑀 ∈ Markov) & ⊢ (𝜑 → 𝐹:𝑀–onto→(𝐴 ⊔ 𝐵)) & ⊢ 𝑃 = (𝑦 ∈ 𝑀 ↦ if(∃𝑧 ∈ 𝐴 (𝐹‘𝑦) = (inl‘𝑧), ∅, 1o)) ⇒ ⊢ (𝜑 → (𝐴 ≠ ∅ → ∃𝑥 𝑥 ∈ 𝐴)) | ||
Theorem | fodjumkv 7027* | A condition which ensures that a nonempty set is inhabited. (Contributed by Jim Kingdon, 25-Mar-2023.) |
⊢ (𝜑 → 𝑀 ∈ Markov) & ⊢ (𝜑 → 𝐹:𝑀–onto→(𝐴 ⊔ 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 ≠ ∅ → ∃𝑥 𝑥 ∈ 𝐴)) | ||
Syntax | ccrd 7028 | Extend class definition to include the cardinal size function. |
class card | ||
Definition | df-card 7029* | 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 7030* | The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.) |
⊢ (∃𝑦 ∈ On 𝑦 ≈ 𝐴 → (card‘𝐴) ∈ On) | ||
Theorem | isnumi 7031 | A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ On ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ dom card) | ||
Theorem | finnum 7032 | Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card) | ||
Theorem | onenon 7033 | Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ On → 𝐴 ∈ dom card) | ||
Theorem | cardval3ex 7034* | The value of (card‘𝐴). (Contributed by Jim Kingdon, 30-Aug-2021.) |
⊢ (∃𝑥 ∈ On 𝑥 ≈ 𝐴 → (card‘𝐴) = ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴}) | ||
Theorem | oncardval 7035* | 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 7036 | 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 7037 | The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.) |
⊢ (card‘∅) = ∅ | ||
Theorem | carden2bex 7038* | If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.) |
⊢ ((𝐴 ≈ 𝐵 ∧ ∃𝑥 ∈ On 𝑥 ≈ 𝐴) → (card‘𝐴) = (card‘𝐵)) | ||
Theorem | pm54.43 7039 | Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.) |
⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2o)) | ||
Theorem | pr2nelem 7040 | Lemma for pr2ne 7041. (Contributed by FL, 17-Aug-2008.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o) | ||
Theorem | pr2ne 7041 | If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2o ↔ 𝐴 ≠ 𝐵)) | ||
Theorem | exmidonfinlem 7042* | Lemma for exmidonfin 7043. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
⊢ 𝐴 = {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}} ⇒ ⊢ (ω = (On ∩ Fin) → DECID 𝜑) | ||
Theorem | exmidonfin 7043 | 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 6759 and nnon 4518. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
⊢ (ω = (On ∩ Fin) → EXMID) | ||
Theorem | en2eleq 7044 | 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 7045 | 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 7046 | Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊢ (1o ⊔ 1o) ≈ 2o | ||
Theorem | infpwfidom 7047 | 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 7048 | Lemma for exmidfodomr 7053. A variant of djur 6947. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 1o) & ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1o)) ⇒ ⊢ (𝜑 → (𝐵 = (inl‘∅) ∨ 𝐵 = (inr‘∅))) | ||
Theorem | exmidfodomrlemreseldju 7049 | Lemma for exmidfodomrlemrALT 7052. A variant of eldju 6946. (Contributed by Jim Kingdon, 9-Jul-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 1o) & ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1o)) ⇒ ⊢ (𝜑 → ((∅ ∈ 𝐴 ∧ 𝐵 = ((inl ↾ 𝐴)‘∅)) ∨ 𝐵 = ((inr ↾ 1o)‘∅))) | ||
Theorem | exmidfodomrlemim 7050* | 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 7051* | 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 7052* | 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 7051. In particular, this proof uses eldju 6946 instead of djur 6947 and avoids djulclb 6933. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.) |
⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID) | ||
Theorem | exmidfodomr 7053* | 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 7054 | Formula for an abbreviation of the axiom of choice. |
wff CHOICE | ||
Definition | df-ac 7055* |
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 4447 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 7056* | 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 7057* | Lemma for exmidac 7058. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.) |
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})} & ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})} & ⊢ 𝐶 = {𝐴, 𝐵} ⇒ ⊢ (CHOICE → EXMID) | ||
Theorem | exmidac 7058 | The axiom of choice implies excluded middle. See acexmid 5766 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 7059 | Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ⊔ 𝐵) ≈ (𝐴 ∪ 𝐵)) | ||
Theorem | djuen 7060 | Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 ⊔ 𝐶) ≈ (𝐵 ⊔ 𝐷)) | ||
Theorem | djuenun 7061 | 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 7062 | 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.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ 𝐴) → (𝐴 ⊔ 1o) ≈ suc 𝐴) | ||
Theorem | dju0en 7063 | 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 7064 | 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.) |
⊢ (2o × 𝐴) = (𝐴 ⊔ 𝐴) | ||
Theorem | djucomen 7065 | 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 7066 | 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 7067 | 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 7068 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ≼ (𝐴 ⊔ 𝐵)) | ||
Theorem | djudomr 7069 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐵 ≼ (𝐴 ⊔ 𝐵)) | ||
We have already introduced the full Axiom of Choice df-ac 7055 but since it implies excluded middle as shown at exmidac 7058, it is not especially relevant to us. In this section we define countable choice and dependent choice, which are not as strong as thus often considered in mathematics which seeks to avoid full excluded middle. | ||
Syntax | wacc 7070 | Formula for an abbreviation of countable choice. |
wff CCHOICE | ||
Definition | df-cc 7071* | The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7055 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.) |
⊢ (CCHOICE ↔ ∀𝑥(dom 𝑥 ≈ ω → ∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥))) | ||
Theorem | ccfunen 7072* | Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.) |
⊢ (𝜑 → CCHOICE) & ⊢ (𝜑 → 𝐴 ≈ ω) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑤 𝑤 ∈ 𝑥) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥)) | ||
This section derives the basics of real and complex numbers. To construct the real numbers constructively, we follow two main sources. The first is Metamath Proof Explorer, which has the advantage of being already formalized in metamath. Its disadvantage, for our purposes, is that it assumes the law of the excluded middle throughout. Since we have already developed natural numbers ( for example, nna0 6363 and similar theorems ), going from there to positive integers (df-ni 7105) and then positive rational numbers (df-nqqs 7149) does not involve a major change in approach compared with the Metamath Proof Explorer. It is when we proceed to Dedekind cuts that we bring in more material from Section 11.2 of [HoTT], which focuses on the aspects of Dedekind cuts which are different without excluded middle. With excluded middle, it is natural to define the cut as the lower set only (as Metamath Proof Explorer does), but we define the cut as a pair of both the lower and upper sets, as [HoTT] does. There are also differences in how we handle order and replacing "not equal to zero" with "apart from zero". | ||
Syntax | cnpi 7073 |
The set of positive integers, which is the set of natural numbers ω
with 0 removed.
Note: This is the start of the Dedekind-cut construction of real and complex numbers. |
class N | ||
Syntax | cpli 7074 | Positive integer addition. |
class +N | ||
Syntax | cmi 7075 | Positive integer multiplication. |
class ·N | ||
Syntax | clti 7076 | Positive integer ordering relation. |
class <N | ||
Syntax | cplpq 7077 | Positive pre-fraction addition. |
class +pQ | ||
Syntax | cmpq 7078 | Positive pre-fraction multiplication. |
class ·pQ | ||
Syntax | cltpq 7079 | Positive pre-fraction ordering relation. |
class <pQ | ||
Syntax | ceq 7080 | Equivalence class used to construct positive fractions. |
class ~Q | ||
Syntax | cnq 7081 | Set of positive fractions. |
class Q | ||
Syntax | c1q 7082 | The positive fraction constant 1. |
class 1Q | ||
Syntax | cplq 7083 | Positive fraction addition. |
class +Q | ||
Syntax | cmq 7084 | Positive fraction multiplication. |
class ·Q | ||
Syntax | crq 7085 | Positive fraction reciprocal operation. |
class *Q | ||
Syntax | cltq 7086 | Positive fraction ordering relation. |
class <Q | ||
Syntax | ceq0 7087 | Equivalence class used to construct nonnegative fractions. |
class ~Q0 | ||
Syntax | cnq0 7088 | Set of nonnegative fractions. |
class Q0 | ||
Syntax | c0q0 7089 | The nonnegative fraction constant 0. |
class 0Q0 | ||
Syntax | cplq0 7090 | Nonnegative fraction addition. |
class +Q0 | ||
Syntax | cmq0 7091 | Nonnegative fraction multiplication. |
class ·Q0 | ||
Syntax | cnp 7092 | Set of positive reals. |
class P | ||
Syntax | c1p 7093 | Positive real constant 1. |
class 1P | ||
Syntax | cpp 7094 | Positive real addition. |
class +P | ||
Syntax | cmp 7095 | Positive real multiplication. |
class ·P | ||
Syntax | cltp 7096 | Positive real ordering relation. |
class <P | ||
Syntax | cer 7097 | Equivalence class used to construct signed reals. |
class ~R | ||
Syntax | cnr 7098 | Set of signed reals. |
class R | ||
Syntax | c0r 7099 | The signed real constant 0. |
class 0R | ||
Syntax | c1r 7100 | The signed real constant 1. |
class 1R |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |