Home | Intuitionistic Logic Explorer Theorem List (p. 71 of 133) | < 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 | finct 7001* | A finite set is countable. (Contributed by Jim Kingdon, 17-Mar-2023.) |
⊔ | ||
Theorem | omct 7002 | is countable. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ | ||
Theorem | ctfoex 7003* | A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.) |
⊔ | ||
Syntax | comni 7004 | Extend class definition to include the class of omniscient sets. |
Omni | ||
Syntax | xnninf 7005 | Set of nonincreasing sequences in . |
ℕ_{∞} | ||
Definition | df-omni 7006* |
An omniscient set is one where we can decide whether a predicate (here
represented by a function ) holds (is equal to ) 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 | ||
Definition | df-nninf 7007* | Define the set of nonincreasing sequences in . Definition in Section 3.1 of [Pierik], p. 15. If we assumed excluded middle, this would be essentially the same as NN0* as defined at df-xnn0 9041 but in its absence the relationship between the two is more complicated. This definition would function much the same whether we used or , but the former allows us to take advantage of (df2o3 6327) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ_{∞} | ||
Theorem | isomni 7008* | The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.) |
Omni | ||
Theorem | isomnimap 7009* | The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni | ||
Theorem | enomnilem 7010 | Lemma for enomni 7011. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni Omni | ||
Theorem | enomni 7011 | Omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Limited Principle of Omniscience as either Omni or Omni. The former is a better match to conventional notation in the sense that df2o3 6327 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni Omni | ||
Theorem | finomni 7012 | A finite set is omniscient. Remark right after Definition 3.1 of [Pierik], p. 14. (Contributed by Jim Kingdon, 28-Jun-2022.) |
Omni | ||
Theorem | exmidomniim 7013 | Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 7014. (Contributed by Jim Kingdon, 29-Jun-2022.) |
EXMID Omni | ||
Theorem | exmidomni 7014 | Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.) |
EXMID Omni | ||
Theorem | exmidlpo 7015 | Excluded middle implies the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 29-Mar-2023.) |
EXMID Omni | ||
Theorem | fodjuomnilemdc 7016* | Lemma for fodjuomni 7021. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊔ DECID inl | ||
Theorem | fodjuf 7017* | Lemma for fodjuomni 7021 and fodjumkv 7034. Domain and range of . (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊔ inl | ||
Theorem | fodjum 7018* | Lemma for fodjuomni 7021 and fodjumkv 7034. A condition which shows that is inhabited. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊔ inl | ||
Theorem | fodju0 7019* | Lemma for fodjuomni 7021 and fodjumkv 7034. A condition which shows that is empty. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊔ inl | ||
Theorem | fodjuomnilemres 7020* | Lemma for fodjuomni 7021. The final result with expressed as a local definition. (Contributed by Jim Kingdon, 29-Jul-2022.) |
Omni ⊔ inl | ||
Theorem | fodjuomni 7021* | A condition which ensures is either inhabited or empty. Lemma 3.2 of [PradicBrown2022], p. 4. (Contributed by Jim Kingdon, 27-Jul-2022.) |
Omni ⊔ | ||
Theorem | infnninf 7022 | The point at infinity in ℕ_{∞} (the constant sequence equal to ). (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ_{∞} | ||
Theorem | nnnninf 7023* | 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 7022. Remark/TODO: the theorem still holds if , that is, the antecedent could be weakened to . (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ_{∞} | ||
Theorem | ctssexmid 7024* | The decidability condition in ctssdc 6998 is needed. More specifically, ctssdc 6998 minus that condition, plus the Limited Principle of Omniscience (LPO), implies excluded middle. (Contributed by Jim Kingdon, 15-Aug-2023.) |
⊔ Omni | ||
Syntax | cmarkov 7025 | Extend class definition to include the class of Markov sets. |
Markov | ||
Definition | df-markov 7026* |
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 )
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 | ||
Theorem | ismkv 7027* | The predicate of being Markov. (Contributed by Jim Kingdon, 18-Mar-2023.) |
Markov | ||
Theorem | ismkvmap 7028* | The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 18-Mar-2023.) |
Markov | ||
Theorem | ismkvnex 7029* | The predicate of being Markov stated in terms of double negation and comparison with . (Contributed by Jim Kingdon, 29-Nov-2023.) |
Markov | ||
Theorem | omnimkv 7030 | 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 7031 | Excluded middle implies Markov's Principle (MP). (Contributed by Jim Kingdon, 4-Apr-2023.) |
EXMID Markov | ||
Theorem | mkvprop 7032* | 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 7033* | Lemma for fodjumkv 7034. The final result with expressed as a local definition. (Contributed by Jim Kingdon, 25-Mar-2023.) |
Markov ⊔ inl | ||
Theorem | fodjumkv 7034* | A condition which ensures that a nonempty set is inhabited. (Contributed by Jim Kingdon, 25-Mar-2023.) |
Markov ⊔ | ||
Syntax | ccrd 7035 | Extend class definition to include the cardinal size function. |
Definition | df-card 7036* | 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 7037* | The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | isnumi 7038 | A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | finnum 7039 | Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
Theorem | onenon 7040 | Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | cardval3ex 7041* | The value of . (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | oncardval 7042* | 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 7043 | 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 7044 | The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.) |
Theorem | carden2bex 7045* | If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | pm54.43 7046 | Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.) |
Theorem | pr2nelem 7047 | Lemma for pr2ne 7048. (Contributed by FL, 17-Aug-2008.) |
Theorem | pr2ne 7048 | If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.) |
Theorem | exmidonfinlem 7049* | Lemma for exmidonfin 7050. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
DECID | ||
Theorem | exmidonfin 7050 | 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 6766 and nnon 4523. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
EXMID | ||
Theorem | en2eleq 7051 | 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 7052 | Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
Theorem | dju1p1e2 7053 | Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊔ | ||
Theorem | infpwfidom 7054 | 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 7055 | Lemma for exmidfodomr 7060. A variant of djur 6954. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊔ inl inr | ||
Theorem | exmidfodomrlemreseldju 7056 | Lemma for exmidfodomrlemrALT 7059. A variant of eldju 6953. (Contributed by Jim Kingdon, 9-Jul-2022.) |
⊔ inl inr | ||
Theorem | exmidfodomrlemim 7057* | 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 7058* | 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 7059* | 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 7058. In particular, this proof uses eldju 6953 instead of djur 6954 and avoids djulclb 6940. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.) |
EXMID | ||
Theorem | exmidfodomr 7060* | 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 7061 | Formula for an abbreviation of the axiom of choice. |
CHOICE | ||
Definition | df-ac 7062* |
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 4452 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 7063* | 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 7064* | Lemma for exmidac 7065. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.) |
CHOICE EXMID | ||
Theorem | exmidac 7065 | The axiom of choice implies excluded middle. See acexmid 5773 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 7066 | Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊔ | ||
Theorem | djuen 7067 | Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊔ ⊔ | ||
Theorem | djuenun 7068 | 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 7069 | 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 7070 | 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 7071 | 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 7072 | 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 7073 | 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 7074 | 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 7075 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊔ | ||
Theorem | djudomr 7076 | 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 7062 but since it implies excluded middle as shown at exmidac 7065, 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 7077 | Formula for an abbreviation of countable choice. |
CCHOICE | ||
Definition | df-cc 7078* | The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7062 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.) |
CCHOICE | ||
Theorem | ccfunen 7079* | Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.) |
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 6370 and similar theorems ), going from there to positive integers (df-ni 7112) and then positive rational numbers (df-nqqs 7156) 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 7080 |
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 7081 | Positive integer addition. |
Syntax | cmi 7082 | Positive integer multiplication. |
Syntax | clti 7083 | Positive integer ordering relation. |
Syntax | cplpq 7084 | Positive pre-fraction addition. |
Syntax | cmpq 7085 | Positive pre-fraction multiplication. |
Syntax | cltpq 7086 | Positive pre-fraction ordering relation. |
Syntax | ceq 7087 | Equivalence class used to construct positive fractions. |
Syntax | cnq 7088 | Set of positive fractions. |
Syntax | c1q 7089 | The positive fraction constant 1. |
Syntax | cplq 7090 | Positive fraction addition. |
Syntax | cmq 7091 | Positive fraction multiplication. |
Syntax | crq 7092 | Positive fraction reciprocal operation. |
Syntax | cltq 7093 | Positive fraction ordering relation. |
Syntax | ceq0 7094 | Equivalence class used to construct nonnegative fractions. |
~_{Q0} | ||
Syntax | cnq0 7095 | Set of nonnegative fractions. |
Q_{0} | ||
Syntax | c0q0 7096 | The nonnegative fraction constant 0. |
0_{Q0} | ||
Syntax | cplq0 7097 | Nonnegative fraction addition. |
+_{Q0} | ||
Syntax | cmq0 7098 | Nonnegative fraction multiplication. |
·_{Q0} | ||
Syntax | cnp 7099 | Set of positive reals. |
Syntax | c1p 7100 | Positive real constant 1. |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |