Home | Intuitionistic Logic Explorer Theorem List (p. 71 of 132) | < 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 | fodjumkvlemres 7001* | Lemma for fodjumkv 7002. The final result with expressed as a local definition. (Contributed by Jim Kingdon, 25-Mar-2023.) |
Markov ⊔ inl | ||
Theorem | fodjumkv 7002* | A condition which ensures that a nonempty set is inhabited. (Contributed by Jim Kingdon, 25-Mar-2023.) |
Markov ⊔ | ||
Syntax | ccrd 7003 | Extend class definition to include the cardinal size function. |
Definition | df-card 7004* | 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 7005* | The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | isnumi 7006 | A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | finnum 7007 | Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
Theorem | onenon 7008 | Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | cardval3ex 7009* | The value of . (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | oncardval 7010* | 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 7011 | 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 7012 | The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.) |
Theorem | carden2bex 7013* | If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | pm54.43 7014 | Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.) |
Theorem | pr2nelem 7015 | Lemma for pr2ne 7016. (Contributed by FL, 17-Aug-2008.) |
Theorem | pr2ne 7016 | If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.) |
Theorem | exmidonfinlem 7017* | Lemma for exmidonfin 7018. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
DECID | ||
Theorem | exmidonfin 7018 | 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 6734 and nnon 4493. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
EXMID | ||
Theorem | en2eleq 7019 | 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 7020 | Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
Theorem | dju1p1e2 7021 | Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊔ | ||
Theorem | infpwfidom 7022 | 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 7023 | Lemma for exmidfodomr 7028. A variant of djur 6922. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊔ inl inr | ||
Theorem | exmidfodomrlemreseldju 7024 | Lemma for exmidfodomrlemrALT 7027. A variant of eldju 6921. (Contributed by Jim Kingdon, 9-Jul-2022.) |
⊔ inl inr | ||
Theorem | exmidfodomrlemim 7025* | 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 7026* | 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 7027* | 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 7026. In particular, this proof uses eldju 6921 instead of djur 6922 and avoids djulclb 6908. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.) |
EXMID | ||
Theorem | exmidfodomr 7028* | 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 7029 | Formula for an abbreviation of the axiom of choice. |
CHOICE | ||
Definition | df-ac 7030* |
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 4422 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 7031* | 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 7032* | Lemma for exmidac 7033. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.) |
CHOICE EXMID | ||
Theorem | exmidac 7033 | The axiom of choice implies excluded middle. See acexmid 5741 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 7034 | Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊔ | ||
Theorem | djuen 7035 | Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊔ ⊔ | ||
Theorem | djuenun 7036 | 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 7037 | 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 7038 | 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 7039 | 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 7040 | 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 7041 | 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 7042 | 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 7043 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊔ | ||
Theorem | djudomr 7044 | 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 7030 but since it implies excluded middle as shown at exmidac 7033, 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 7045 | Formula for an abbreviation of countable choice. |
CCHOICE | ||
Definition | df-cc 7046* | The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7030 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.) |
CCHOICE | ||
Theorem | ccfunen 7047* | 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 6338 and similar theorems ), going from there to positive integers (df-ni 7080) and then positive rational numbers (df-nqqs 7124) 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 7048 |
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 7049 | Positive integer addition. |
Syntax | cmi 7050 | Positive integer multiplication. |
Syntax | clti 7051 | Positive integer ordering relation. |
Syntax | cplpq 7052 | Positive pre-fraction addition. |
Syntax | cmpq 7053 | Positive pre-fraction multiplication. |
Syntax | cltpq 7054 | Positive pre-fraction ordering relation. |
Syntax | ceq 7055 | Equivalence class used to construct positive fractions. |
Syntax | cnq 7056 | Set of positive fractions. |
Syntax | c1q 7057 | The positive fraction constant 1. |
Syntax | cplq 7058 | Positive fraction addition. |
Syntax | cmq 7059 | Positive fraction multiplication. |
Syntax | crq 7060 | Positive fraction reciprocal operation. |
Syntax | cltq 7061 | Positive fraction ordering relation. |
Syntax | ceq0 7062 | Equivalence class used to construct nonnegative fractions. |
~Q0 | ||
Syntax | cnq0 7063 | Set of nonnegative fractions. |
Q0 | ||
Syntax | c0q0 7064 | The nonnegative fraction constant 0. |
0Q0 | ||
Syntax | cplq0 7065 | Nonnegative fraction addition. |
+Q0 | ||
Syntax | cmq0 7066 | Nonnegative fraction multiplication. |
·Q0 | ||
Syntax | cnp 7067 | Set of positive reals. |
Syntax | c1p 7068 | Positive real constant 1. |
Syntax | cpp 7069 | Positive real addition. |
Syntax | cmp 7070 | Positive real multiplication. |
Syntax | cltp 7071 | Positive real ordering relation. |
Syntax | cer 7072 | Equivalence class used to construct signed reals. |
Syntax | cnr 7073 | Set of signed reals. |
Syntax | c0r 7074 | The signed real constant 0. |
Syntax | c1r 7075 | The signed real constant 1. |
Syntax | cm1r 7076 | The signed real constant -1. |
Syntax | cplr 7077 | Signed real addition. |
Syntax | cmr 7078 | Signed real multiplication. |
Syntax | cltr 7079 | Signed real ordering relation. |
Definition | df-ni 7080 | Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.) |
Definition | df-pli 7081 | Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) |
Definition | df-mi 7082 | Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) |
Definition | df-lti 7083 | Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 6-Feb-1996.) |
Theorem | elni 7084 | Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.) |
Theorem | pinn 7085 | A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) |
Theorem | pion 7086 | A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.) |
Theorem | piord 7087 | A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.) |
Theorem | niex 7088 | The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.) |
Theorem | 0npi 7089 | The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.) |
Theorem | elni2 7090 | Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.) |
Theorem | 1pi 7091 | Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.) |
Theorem | addpiord 7092 | Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.) |
Theorem | mulpiord 7093 | Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.) |
Theorem | mulidpi 7094 | 1 is an identity element for multiplication on positive integers. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | ltpiord 7095 | Positive integer 'less than' in terms of ordinal membership. (Contributed by NM, 6-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | ltsopi 7096 | Positive integer 'less than' is a strict ordering. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Mario Carneiro, 10-Jul-2014.) |
Theorem | pitric 7097 | Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.) |
Theorem | pitri3or 7098 | Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.) |
Theorem | ltdcpi 7099 | Less-than for positive integers is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.) |
DECID | ||
Theorem | ltrelpi 7100 | Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |