Home | Intuitionistic Logic Explorer Theorem List (p. 72 of 137) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mkvprop 7101* | 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 7102* | Lemma for fodjumkv 7103. The final result with expressed as a local definition. (Contributed by Jim Kingdon, 25-Mar-2023.) |
Markov ⊔ inl | ||
Theorem | fodjumkv 7103* | A condition which ensures that a nonempty set is inhabited. (Contributed by Jim Kingdon, 25-Mar-2023.) |
Markov ⊔ | ||
Theorem | enmkvlem 7104 | Lemma for enmkv 7105. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.) |
Markov Markov | ||
Theorem | enmkv 7105 | Being Markov is invariant with respect to equinumerosity. For example, this means that we can express the Markov's Principle as either Markov or Markov. The former is a better match to conventional notation in the sense that df2o3 6377 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 24-Jun-2024.) |
Markov Markov | ||
Syntax | cwomni 7106 | Extend class definition to include the class of weakly omniscient sets. |
WOmni | ||
Definition | df-womni 7107* |
A weakly omniscient set is one where we can decide whether a predicate
(here represented by a function ) holds (is equal to ) 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 DECID | ||
Theorem | iswomni 7108* | The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.) |
WOmni DECID | ||
Theorem | iswomnimap 7109* | The predicate of being weakly omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 9-Jun-2024.) |
WOmni DECID | ||
Theorem | omniwomnimkv 7110 | 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 7111 | LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7110. There is an analogue in terms of analytic omniscience principles at tridceq 13638. (Contributed by Jim Kingdon, 24-Jul-2024.) |
Omni WOmni | ||
Theorem | enwomnilem 7112 | Lemma for enwomni 7113. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.) |
WOmni WOmni | ||
Theorem | enwomni 7113 | 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 WOmni. The former is a better match to conventional notation in the sense that df2o3 6377 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 20-Jun-2024.) |
WOmni WOmni | ||
Syntax | ccrd 7114 | Extend class definition to include the cardinal size function. |
Definition | df-card 7115* | 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.) |
Theorem | cardcl 7116* | The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | isnumi 7117 | A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | finnum 7118 | Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
Theorem | onenon 7119 | Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | cardval3ex 7120* | The value of . (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | oncardval 7121* | 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.) |
Theorem | cardonle 7122 | 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.) |
Theorem | card0 7123 | The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.) |
Theorem | carden2bex 7124* | If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | pm54.43 7125 | Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.) |
Theorem | pr2nelem 7126 | Lemma for pr2ne 7127. (Contributed by FL, 17-Aug-2008.) |
Theorem | pr2ne 7127 | If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.) |
Theorem | exmidonfinlem 7128* | Lemma for exmidonfin 7129. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
DECID | ||
Theorem | exmidonfin 7129 | 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 6817 and nnon 4569. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
EXMID | ||
Theorem | en2eleq 7130 | 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.) |
Theorem | en2other2 7131 | Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
Theorem | dju1p1e2 7132 | Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊔ | ||
Theorem | infpwfidom 7133 | The collection of finite subsets of a set dominates the set. (We use the weaker sethood assumption because this theorem also implies that is a set if is.) (Contributed by Mario Carneiro, 17-May-2015.) |
Theorem | exmidfodomrlemeldju 7134 | Lemma for exmidfodomr 7139. A variant of djur 7013. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊔ inl inr | ||
Theorem | exmidfodomrlemreseldju 7135 | Lemma for exmidfodomrlemrALT 7138. A variant of eldju 7012. (Contributed by Jim Kingdon, 9-Jul-2022.) |
⊔ inl inr | ||
Theorem | exmidfodomrlemim 7136* | 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 | ||
Theorem | exmidfodomrlemr 7137* | 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.) |
EXMID | ||
Theorem | exmidfodomrlemrALT 7138* | 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 7137. In particular, this proof uses eldju 7012 instead of djur 7013 and avoids djulclb 6999. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.) |
EXMID | ||
Theorem | exmidfodomr 7139* | 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 | ||
Syntax | wac 7140 | Formula for an abbreviation of the axiom of choice. |
CHOICE | ||
Definition | df-ac 7141* |
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 4496 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 | ||
Theorem | acfun 7142* | 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 | ||
Theorem | exmidaclem 7143* | Lemma for exmidac 7144. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.) |
CHOICE EXMID | ||
Theorem | exmidac 7144 | The axiom of choice implies excluded middle. See acexmid 5823 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 7145 | Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊔ | ||
Theorem | djuen 7146 | Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊔ ⊔ | ||
Theorem | djuenun 7147 | 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 7148 | 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.) |
⊔ | ||
Theorem | dju0en 7149 | 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 7150 | 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.) |
⊔ | ||
Theorem | djucomen 7151 | 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 7152 | 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 7153 | 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 7154 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊔ | ||
Theorem | djudomr 7155 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊔ | ||
Theorem | exmidontriimlem1 7156 | Lemma for exmidontriim 7160. A variation of r19.30dc 2604. (Contributed by Jim Kingdon, 12-Aug-2024.) |
EXMID | ||
Theorem | exmidontriimlem2 7157* | Lemma for exmidontriim 7160. (Contributed by Jim Kingdon, 12-Aug-2024.) |
EXMID | ||
Theorem | exmidontriimlem3 7158* | Lemma for exmidontriim 7160. What we get to do based on induction on both and . (Contributed by Jim Kingdon, 10-Aug-2024.) |
EXMID | ||
Theorem | exmidontriimlem4 7159* | Lemma for exmidontriim 7160. The induction step for the induction on . (Contributed by Jim Kingdon, 10-Aug-2024.) |
EXMID | ||
Theorem | exmidontriim 7160* | Excluded middle implies ordinal trichotomy. Lemma 10.4.1 of [HoTT], p. (varies). The proof follows the proof from the HoTT book fairly closely. (Contributed by Jim Kingdon, 10-Aug-2024.) |
EXMID | ||
Theorem | pw1on 7161 | The power set of is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.) |
Theorem | pw1dom2 7162 | The power set of dominates . Also see pwpw0ss 3767 which is similar. (Contributed by Jim Kingdon, 21-Sep-2022.) |
Theorem | pw1ne0 7163 | The power set of is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.) |
Theorem | pw1ne1 7164 | The power set of is not one. (Contributed by Jim Kingdon, 30-Jul-2024.) |
Theorem | pw1ne3 7165 | The power set of is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
Theorem | pw1nel3 7166 | Negated excluded middle implies that the power set of is not an element of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
EXMID | ||
Theorem | sucpw1ne3 7167 | Negated excluded middle implies that the successor of the power set of is not three . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
EXMID | ||
Theorem | sucpw1nel3 7168 | The successor of the power set of is not an element of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
Theorem | 3nelsucpw1 7169 | Three is not an element of the successor of the power set of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
Theorem | sucpw1nss3 7170 | Negated excluded middle implies that the successor of the power set of is not a subset of . (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.) |
EXMID | ||
Theorem | 3nsssucpw1 7171 | Negated excluded middle implies that is not a subset of the successor of the power set of . (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.) |
EXMID | ||
Theorem | onntri35 7172* |
Double negated ordinal trichotomy.
There are five equivalent statements: (1) , (2) , (3) , (4) , and (5) EXMID. That these are all equivalent is expressed by (1) implies (3) (onntri13 7173), (3) implies (5) (onntri35 7172), (5) implies (1) (onntri51 7175), (2) implies (4) (onntri24 7177), (4) implies (5) (onntri45 7176), and (5) implies (2) (onntri52 7179). Another way of stating this is that EXMID is equivalent to trichotomy, either the or the form, as shown in exmidontri 7174 and exmidontri2or 7178, respectively. Thus EXMID is equivalent to (1) or (2). In addition, EXMID is equivalent to (3) by onntri3or 7180 and (4) by onntri2or 7181. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
Theorem | onntri13 7173 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
Theorem | exmidontri 7174* | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) |
EXMID | ||
Theorem | onntri51 7175* | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
Theorem | onntri45 7176* | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
Theorem | onntri24 7177 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
Theorem | exmidontri2or 7178* | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) |
EXMID | ||
Theorem | onntri52 7179* | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
Theorem | onntri3or 7180* | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) |
EXMID | ||
Theorem | onntri2or 7181* | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) |
EXMID | ||
We have already introduced the full Axiom of Choice df-ac 7141 but since it implies excluded middle as shown at exmidac 7144, 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 7182 | Formula for an abbreviation of countable choice. |
CCHOICE | ||
Definition | df-cc 7183* | The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7141 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.) |
CCHOICE | ||
Theorem | ccfunen 7184* | Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.) |
CCHOICE | ||
Theorem | cc1 7185* | Countable choice in terms of a choice function on a countably infinite set of inhabited sets. (Contributed by Jim Kingdon, 27-Apr-2024.) |
CCHOICE | ||
Theorem | cc2lem 7186* | Lemma for cc2 7187. (Contributed by Jim Kingdon, 27-Apr-2024.) |
CCHOICE | ||
Theorem | cc2 7187* | Countable choice using sequences instead of countable sets. (Contributed by Jim Kingdon, 27-Apr-2024.) |
CCHOICE | ||
Theorem | cc3 7188* | Countable choice using a sequence F(n) . (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Jim Kingdon, 29-Apr-2024.) |
CCHOICE | ||
Theorem | cc4f 7189* | Countable choice by showing the existence of a function which can choose a value at each index such that holds. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.) |
CCHOICE | ||
Theorem | cc4 7190* | Countable choice by showing the existence of a function which can choose a value at each index such that holds. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 1-May-2024.) |
CCHOICE | ||
Theorem | cc4n 7191* | Countable choice with a simpler restriction on how every set in the countable collection needs to be inhabited. That is, compared with cc4 7190, the hypotheses only require an A(n) for each value of , not a single set which suffices for every . (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.) |
CCHOICE | ||
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 6421 and similar theorems ), going from there to positive integers (df-ni 7224) and then positive rational numbers (df-nqqs 7268) 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 or choice principles. With excluded middle, it is natural to define a cut as the lower set only (as Metamath Proof Explorer does), but here 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". When working constructively, there are several possible definitions of real numbers. Here we adopt the most common definition, as two-sided Dedekind cuts with the properties described at df-inp 7386. The Cauchy reals (without countable choice) fail to satisfy ax-caucvg 7852 and the MacNeille reals fail to satisfy axltwlin 7945, and we do not develop them here. For more on differing definitions of the reals, see the introduction to Chapter 11 in [HoTT] or Section 1.2 of [BauerHanson]. | ||
Syntax | cnpi 7192 |
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. |
Syntax | cpli 7193 | Positive integer addition. |
Syntax | cmi 7194 | Positive integer multiplication. |
Syntax | clti 7195 | Positive integer ordering relation. |
Syntax | cplpq 7196 | Positive pre-fraction addition. |
Syntax | cmpq 7197 | Positive pre-fraction multiplication. |
Syntax | cltpq 7198 | Positive pre-fraction ordering relation. |
Syntax | ceq 7199 | Equivalence class used to construct positive fractions. |
Syntax | cnq 7200 | Set of positive fractions. |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |