Home | Intuitionistic Logic Explorer Theorem List (p. 72 of 142) | < 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 | infnninfOLD 7101 | Obsolete version of infnninf 7100 as of 10-Aug-2024. (Contributed by Jim Kingdon, 14-Jul-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
ℕ∞ | ||
Theorem | nnnninf 7102* | Elements of ℕ∞ corresponding to natural numbers. The natural number corresponds to a sequence of ones followed by zeroes. This can be strengthened to include infinity, see nnnninf2 7103. (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ∞ | ||
Theorem | nnnninf2 7103* | Canonical embedding of into ℕ∞. (Contributed by BJ, 10-Aug-2024.) |
ℕ∞ | ||
Theorem | nnnninfeq 7104* | Mapping of a natural number to an element of ℕ∞. (Contributed by Jim Kingdon, 4-Aug-2022.) |
ℕ∞ | ||
Theorem | nnnninfeq2 7105* | Mapping of a natural number to an element of ℕ∞. Similar to nnnninfeq 7104 but if we have information about a single digit, that gives information about all previous digits. (Contributed by Jim Kingdon, 4-Aug-2022.) |
ℕ∞ | ||
Theorem | nninfisollem0 7106* | Lemma for nninfisol 7109. The case where is zero. (Contributed by Jim Kingdon, 13-Sep-2024.) |
ℕ∞ DECID | ||
Theorem | nninfisollemne 7107* | Lemma for nninfisol 7109. A case where is a successor and and are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.) |
ℕ∞ DECID | ||
Theorem | nninfisollemeq 7108* | Lemma for nninfisol 7109. The case where is a successor and and are equal. (Contributed by Jim Kingdon, 13-Sep-2024.) |
ℕ∞ DECID | ||
Theorem | nninfisol 7109* | Finite elements of ℕ∞ are isolated. That is, given a natural number and any element of ℕ∞, it is decidable whether the natural number (when converted to an element of ℕ∞) is equal to the given element of ℕ∞. Stated in an online post by Martin Escardo. One way to understand this theorem is that you do not need to look at an unbounded number of elements of the sequence to decide whether it is equal to (in fact, you only need to look at two elements and tells you where to look). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.) |
ℕ∞ DECID | ||
Syntax | comni 7110 | Extend class definition to include the class of omniscient sets. |
Omni | ||
Definition | df-omni 7111* |
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 | ||
Theorem | isomni 7112* | The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.) |
Omni | ||
Theorem | isomnimap 7113* | The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni | ||
Theorem | enomnilem 7114 | Lemma for enomni 7115. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni Omni | ||
Theorem | enomni 7115 | 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 6409 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni Omni | ||
Theorem | finomni 7116 | 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 7117 | Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 7118. (Contributed by Jim Kingdon, 29-Jun-2022.) |
EXMID Omni | ||
Theorem | exmidomni 7118 | Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.) |
EXMID Omni | ||
Theorem | exmidlpo 7119 | Excluded middle implies the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 29-Mar-2023.) |
EXMID Omni | ||
Theorem | fodjuomnilemdc 7120* | Lemma for fodjuomni 7125. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊔ DECID inl | ||
Theorem | fodjuf 7121* | Lemma for fodjuomni 7125 and fodjumkv 7136. Domain and range of . (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊔ inl | ||
Theorem | fodjum 7122* | Lemma for fodjuomni 7125 and fodjumkv 7136. A condition which shows that is inhabited. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊔ inl | ||
Theorem | fodju0 7123* | Lemma for fodjuomni 7125 and fodjumkv 7136. A condition which shows that is empty. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊔ inl | ||
Theorem | fodjuomnilemres 7124* | Lemma for fodjuomni 7125. The final result with expressed as a local definition. (Contributed by Jim Kingdon, 29-Jul-2022.) |
Omni ⊔ inl | ||
Theorem | fodjuomni 7125* | 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 | ctssexmid 7126* | The decidability condition in ctssdc 7090 is needed. More specifically, ctssdc 7090 minus that condition, plus the Limited Principle of Omniscience (LPO), implies excluded middle. (Contributed by Jim Kingdon, 15-Aug-2023.) |
⊔ Omni | ||
Syntax | cmarkov 7127 | Extend class definition to include the class of Markov sets. |
Markov | ||
Definition | df-markov 7128* |
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 7129* | The predicate of being Markov. (Contributed by Jim Kingdon, 18-Mar-2023.) |
Markov | ||
Theorem | ismkvmap 7130* | The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 18-Mar-2023.) |
Markov | ||
Theorem | ismkvnex 7131* | The predicate of being Markov stated in terms of double negation and comparison with . (Contributed by Jim Kingdon, 29-Nov-2023.) |
Markov | ||
Theorem | omnimkv 7132 | 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 7133 | Excluded middle implies Markov's Principle (MP). (Contributed by Jim Kingdon, 4-Apr-2023.) |
EXMID Markov | ||
Theorem | mkvprop 7134* | 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 7135* | Lemma for fodjumkv 7136. The final result with expressed as a local definition. (Contributed by Jim Kingdon, 25-Mar-2023.) |
Markov ⊔ inl | ||
Theorem | fodjumkv 7136* | A condition which ensures that a nonempty set is inhabited. (Contributed by Jim Kingdon, 25-Mar-2023.) |
Markov ⊔ | ||
Theorem | enmkvlem 7137 | Lemma for enmkv 7138. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.) |
Markov Markov | ||
Theorem | enmkv 7138 | 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 6409 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 24-Jun-2024.) |
Markov Markov | ||
Syntax | cwomni 7139 | Extend class definition to include the class of weakly omniscient sets. |
WOmni | ||
Definition | df-womni 7140* |
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 7141* | The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.) |
WOmni DECID | ||
Theorem | iswomnimap 7142* | The predicate of being weakly omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 9-Jun-2024.) |
WOmni DECID | ||
Theorem | omniwomnimkv 7143 | 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 7144 | LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7143. There is an analogue in terms of analytic omniscience principles at tridceq 14088. (Contributed by Jim Kingdon, 24-Jul-2024.) |
Omni WOmni | ||
Theorem | enwomnilem 7145 | Lemma for enwomni 7146. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.) |
WOmni WOmni | ||
Theorem | enwomni 7146 | 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 6409 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 20-Jun-2024.) |
WOmni WOmni | ||
Theorem | nninfdcinf 7147* | The Weak Limited Principle of Omniscience (WLPO) implies that it is decidable whether an element of ℕ∞ equals the point at infinity. (Contributed by Jim Kingdon, 3-Dec-2024.) |
WOmni ℕ∞ DECID | ||
Theorem | nninfwlporlemd 7148* | Given two countably infinite sequences of zeroes and ones, they are equal if and only if a sequence formed by pointwise comparing them is all ones. (Contributed by Jim Kingdon, 6-Dec-2024.) |
Theorem | nninfwlporlem 7149* | Lemma for nninfwlpor 7150. The result. (Contributed by Jim Kingdon, 7-Dec-2024.) |
WOmni DECID | ||
Theorem | nninfwlpor 7150* | The Weak Limited Principle of Omniscience (WLPO) implies that equality for ℕ∞ is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.) |
WOmni ℕ∞ ℕ∞ DECID | ||
Theorem | nninfwlpoimlemg 7151* | Lemma for nninfwlpoim 7154. (Contributed by Jim Kingdon, 8-Dec-2024.) |
ℕ∞ | ||
Theorem | nninfwlpoimlemginf 7152* | Lemma for nninfwlpoim 7154. (Contributed by Jim Kingdon, 8-Dec-2024.) |
Theorem | nninfwlpoimlemdc 7153* | Lemma for nninfwlpoim 7154. (Contributed by Jim Kingdon, 8-Dec-2024.) |
ℕ∞ ℕ∞ DECID DECID | ||
Theorem | nninfwlpoim 7154* | Decidable equality for ℕ∞ implies the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.) |
ℕ∞ ℕ∞ DECID WOmni | ||
Theorem | nninfwlpo 7155* | Decidability of equality for ℕ∞ is equivalent to the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 3-Dec-2024.) |
ℕ∞ ℕ∞ DECID WOmni | ||
Syntax | ccrd 7156 | Extend class definition to include the cardinal size function. |
Definition | df-card 7157* | 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 7158* | The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | isnumi 7159 | A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | finnum 7160 | Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
Theorem | onenon 7161 | Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | cardval3ex 7162* | The value of . (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | oncardval 7163* | 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 7164 | 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 7165 | The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.) |
Theorem | carden2bex 7166* | If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | pm54.43 7167 | Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.) |
Theorem | pr2nelem 7168 | Lemma for pr2ne 7169. (Contributed by FL, 17-Aug-2008.) |
Theorem | pr2ne 7169 | If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.) |
Theorem | exmidonfinlem 7170* | Lemma for exmidonfin 7171. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
DECID | ||
Theorem | exmidonfin 7171 | 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 6850 and nnon 4594. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
EXMID | ||
Theorem | en2eleq 7172 | 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 7173 | Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
Theorem | dju1p1e2 7174 | Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊔ | ||
Theorem | infpwfidom 7175 | 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 7176 | Lemma for exmidfodomr 7181. A variant of djur 7046. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊔ inl inr | ||
Theorem | exmidfodomrlemreseldju 7177 | Lemma for exmidfodomrlemrALT 7180. A variant of eldju 7045. (Contributed by Jim Kingdon, 9-Jul-2022.) |
⊔ inl inr | ||
Theorem | exmidfodomrlemim 7178* | 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 7179* | 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 7180* | 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 7179. In particular, this proof uses eldju 7045 instead of djur 7046 and avoids djulclb 7032. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.) |
EXMID | ||
Theorem | exmidfodomr 7181* | 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 7182 | Formula for an abbreviation of the axiom of choice. |
CHOICE | ||
Definition | df-ac 7183* |
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 4521 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 7184* | 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 7185* | Lemma for exmidac 7186. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.) |
CHOICE EXMID | ||
Theorem | exmidac 7186 | The axiom of choice implies excluded middle. See acexmid 5852 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 7187 | Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊔ | ||
Theorem | djuen 7188 | Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊔ ⊔ | ||
Theorem | djuenun 7189 | 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 7190 | 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 7191 | 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 7192 | 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 7193 | 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 7194 | 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 7195 | 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 7196 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊔ | ||
Theorem | djudomr 7197 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊔ | ||
Theorem | exmidontriimlem1 7198 | Lemma for exmidontriim 7202. A variation of r19.30dc 2617. (Contributed by Jim Kingdon, 12-Aug-2024.) |
EXMID | ||
Theorem | exmidontriimlem2 7199* | Lemma for exmidontriim 7202. (Contributed by Jim Kingdon, 12-Aug-2024.) |
EXMID | ||
Theorem | exmidontriimlem3 7200* | Lemma for exmidontriim 7202. What we get to do based on induction on both and . (Contributed by Jim Kingdon, 10-Aug-2024.) |
EXMID |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |