Home | Intuitionistic Logic Explorer Theorem List (p. 70 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 | ||
Definition | df-inr 6901 | Right injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
inr | ||
Theorem | djulclr 6902 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
inl ⊔ | ||
Theorem | djurclr 6903 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
inr ⊔ | ||
Theorem | djulcl 6904 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
inl ⊔ | ||
Theorem | djurcl 6905 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
inr ⊔ | ||
Theorem | djuf1olem 6906* | Lemma for djulf1o 6911 and djurf1o 6912. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
Theorem | djuf1olemr 6907* | Lemma for djulf1or 6909 and djurf1or 6910. For a version of this lemma with defined on and no restriction in the conclusion, see djuf1olem 6906. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
Theorem | djulclb 6908 | Left biconditional closure of disjoint union. (Contributed by Jim Kingdon, 2-Jul-2022.) |
inl ⊔ | ||
Theorem | djulf1or 6909 | The left injection function on all sets is one to one and onto. (Contributed by BJ and Jim Kingdon, 22-Jun-2022.) |
inl | ||
Theorem | djurf1or 6910 | The right injection function on all sets is one to one and onto. (Contributed by BJ and Jim Kingdon, 22-Jun-2022.) |
inr | ||
Theorem | djulf1o 6911 | The left injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.) |
inl | ||
Theorem | djurf1o 6912 | The right injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.) |
inr | ||
Theorem | inresflem 6913* | Lemma for inlresf1 6914 and inrresf1 6915. (Contributed by BJ, 4-Jul-2022.) |
Theorem | inlresf1 6914 | The left injection restricted to the left class of a disjoint union is an injective function from the left class into the disjoint union. (Contributed by AV, 28-Jun-2022.) |
inl ⊔ | ||
Theorem | inrresf1 6915 | The right injection restricted to the right class of a disjoint union is an injective function from the right class into the disjoint union. (Contributed by AV, 28-Jun-2022.) |
inr ⊔ | ||
Theorem | djuinr 6916 | The ranges of any left and right injections are disjoint. Remark: the extra generality offered by the two restrictions makes the theorem more readily usable (e.g., by djudom 6946 and djufun 6957) while the simpler statement inl inr is easily recovered from it by substituting for both and as done in casefun 6938). (Contributed by BJ and Jim Kingdon, 21-Jun-2022.) |
inl inr | ||
Theorem | djuin 6917 | The images of any classes under right and left injection produce disjoint sets. (Contributed by Jim Kingdon, 21-Jun-2022.) (Proof shortened by BJ, 9-Jul-2023.) |
inl inr | ||
Theorem | inl11 6918 | Left injection is one-to-one. (Contributed by Jim Kingdon, 12-Jul-2023.) |
inl inl | ||
Theorem | djuunr 6919 | The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 6-Jul-2022.) |
inl inr ⊔ | ||
Theorem | djuun 6920 | The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 9-Jul-2023.) |
inl inr ⊔ | ||
Theorem | eldju 6921* | Element of a disjoint union. (Contributed by BJ and Jim Kingdon, 23-Jun-2022.) |
⊔ inl inr | ||
Theorem | djur 6922* | A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022.) Upgrade implication to biconditional and shorten proof. (Revised by BJ, 14-Jul-2023.) |
⊔ inl inr | ||
Theorem | djuss 6923 | A disjoint union is a subset of a Cartesian product. (Contributed by AV, 25-Jun-2022.) |
⊔ | ||
Theorem | eldju1st 6924 | The first component of an element of a disjoint union is either or . (Contributed by AV, 26-Jun-2022.) |
⊔ | ||
Theorem | eldju2ndl 6925 | The second component of an element of a disjoint union is an element of the left class of the disjoint union if its first component is the empty set. (Contributed by AV, 26-Jun-2022.) |
⊔ | ||
Theorem | eldju2ndr 6926 | The second component of an element of a disjoint union is an element of the right class of the disjoint union if its first component is not the empty set. (Contributed by AV, 26-Jun-2022.) |
⊔ | ||
Theorem | 1stinl 6927 | The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.) |
inl | ||
Theorem | 2ndinl 6928 | The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.) |
inl | ||
Theorem | 1stinr 6929 | The first component of the value of a right injection is . (Contributed by AV, 27-Jun-2022.) |
inr | ||
Theorem | 2ndinr 6930 | The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.) |
inr | ||
Theorem | djune 6931 | Left and right injection never produce equal values. (Contributed by Jim Kingdon, 2-Jul-2022.) |
inl inr | ||
Theorem | updjudhf 6932* | The mapping of an element of the disjoint union to the value of the corresponding function is a function. (Contributed by AV, 26-Jun-2022.) |
⊔ ⊔ | ||
Theorem | updjudhcoinlf 6933* | The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the left injection equals the first function. (Contributed by AV, 27-Jun-2022.) |
⊔ inl | ||
Theorem | updjudhcoinrg 6934* | The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the right injection equals the second function. (Contributed by AV, 27-Jun-2022.) |
⊔ inr | ||
Theorem | updjud 6935* | Universal property of the disjoint union. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.) |
⊔ inl inr | ||
Syntax | cdjucase 6936 | Syntax for the "case" construction. |
case | ||
Definition | df-case 6937 | The "case" construction: if and are functions, then case ⊔ is the natural function obtained by a definition by cases, hence the name. It is the unique function whose existence is asserted by the universal property of disjoint unions updjud 6935. The definition is adapted to make sense also for binary relations (where the universal property also holds). (Contributed by MC and BJ, 10-Jul-2022.) |
case inl inr | ||
Theorem | casefun 6938 | The "case" construction of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
case | ||
Theorem | casedm 6939 | The domain of the "case" construction is the disjoint union of the domains. TODO (although less important): case . (Contributed by BJ, 10-Jul-2022.) |
case ⊔ | ||
Theorem | caserel 6940 | The "case" construction of two relations is a relation, with bounds on its domain and codomain. Typically, the "case" construction is used when both relations have a common codomain. (Contributed by BJ, 10-Jul-2022.) |
case ⊔ | ||
Theorem | casef 6941 | The "case" construction of two functions is a function on the disjoint union of their domains. (Contributed by BJ, 10-Jul-2022.) |
case ⊔ | ||
Theorem | caseinj 6942 | The "case" construction of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.) |
case | ||
Theorem | casef1 6943 | The "case" construction of two injective functions with disjoint ranges is an injective function. (Contributed by BJ, 10-Jul-2022.) |
case ⊔ | ||
Theorem | caseinl 6944 | Applying the "case" construction to a left injection. (Contributed by Jim Kingdon, 15-Mar-2023.) |
case inl | ||
Theorem | caseinr 6945 | Applying the "case" construction to a right injection. (Contributed by Jim Kingdon, 12-Jul-2023.) |
case inr | ||
Theorem | djudom 6946 | Dominance law for disjoint union. (Contributed by Jim Kingdon, 25-Jul-2022.) |
⊔ ⊔ | ||
Theorem | omp1eomlem 6947* | Lemma for omp1eom 6948. (Contributed by Jim Kingdon, 11-Jul-2023.) |
inr inl case ⊔ | ||
Theorem | omp1eom 6948 | Adding one to . (Contributed by Jim Kingdon, 10-Jul-2023.) |
⊔ | ||
Theorem | endjusym 6949 | Reversing right and left operands of a disjoint union produces an equinumerous result. (Contributed by Jim Kingdon, 10-Jul-2023.) |
⊔ ⊔ | ||
Theorem | eninl 6950 | Equinumerosity of a set and its image under left injection. (Contributed by Jim Kingdon, 30-Jul-2023.) |
inl | ||
Theorem | eninr 6951 | Equinumerosity of a set and its image under right injection. (Contributed by Jim Kingdon, 30-Jul-2023.) |
inr | ||
Theorem | difinfsnlem 6952* | Lemma for difinfsn 6953. The case where we need to swap and inr in building the mapping . (Contributed by Jim Kingdon, 9-Aug-2023.) |
DECID ⊔ inr inl inr inl | ||
Theorem | difinfsn 6953* | An infinite set minus one element is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.) |
DECID | ||
Theorem | difinfinf 6954* | An infinite set minus a finite subset is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.) |
DECID | ||
Syntax | cdjud 6955 | Syntax for the domain-disjoint-union of two relations. |
⊔d | ||
Definition | df-djud 6956 |
The "domain-disjoint-union" of two relations: if and
are two binary relations,
then ⊔d is the
binary relation from ⊔
to having the universal
property of disjoint unions (see updjud 6935 in the case of functions).
Remark: the restrictions to (resp. ) are not necessary since extra stuff would be thrown away in the post-composition with (resp. ), as in df-case 6937, but they are explicitly written for clarity. (Contributed by MC and BJ, 10-Jul-2022.) |
⊔d inl inr | ||
Theorem | djufun 6957 | The "domain-disjoint-union" of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
⊔d | ||
Theorem | djudm 6958 | The domain of the "domain-disjoint-union" is the disjoint union of the domains. Remark: its range is the (standard) union of the ranges. (Contributed by BJ, 10-Jul-2022.) |
⊔d ⊔ | ||
Theorem | djuinj 6959 | The "domain-disjoint-union" of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.) |
⊔d | ||
Theorem | 0ct 6960 | The empty set is countable. Remark of [BauerSwan], p. 14:3 which also has the definition of countable used here. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊔ | ||
Theorem | ctmlemr 6961* | Lemma for ctm 6962. One of the directions of the biconditional. (Contributed by Jim Kingdon, 16-Mar-2023.) |
⊔ | ||
Theorem | ctm 6962* | Two equivalent definitions of countable for an inhabited set. Remark of [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊔ | ||
Theorem | ctssdclemn0 6963* | Lemma for ctssdc 6966. The case. (Contributed by Jim Kingdon, 16-Aug-2023.) |
DECID ⊔ | ||
Theorem | ctssdccl 6964* | A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 6966 but expressed in terms of classes rather than . (Contributed by Jim Kingdon, 30-Oct-2023.) |
⊔ inl inl DECID | ||
Theorem | ctssdclemr 6965* | Lemma for ctssdc 6966. Showing that our usual definition of countable implies the alternate one. (Contributed by Jim Kingdon, 16-Aug-2023.) |
⊔ DECID | ||
Theorem | ctssdc 6966* | A set is countable iff there is a surjection from a decidable subset of the natural numbers onto it. The decidability condition is needed as shown at ctssexmid 6992. (Contributed by Jim Kingdon, 15-Aug-2023.) |
DECID ⊔ | ||
Theorem | enumctlemm 6967* | Lemma for enumct 6968. The case where is greater than zero. (Contributed by Jim Kingdon, 13-Mar-2023.) |
Theorem | enumct 6968* | A finitely enumerable set is countable. Lemma 8.1.14 of [AczelRathjen], p. 73 (except that our definition of countable does not require the set to be inhabited). "Finitely enumerable" is defined as per Definition 8.1.4 of [AczelRathjen], p. 71 and "countable" is defined as ⊔ per [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊔ | ||
Theorem | finct 6969* | A finite set is countable. (Contributed by Jim Kingdon, 17-Mar-2023.) |
⊔ | ||
Theorem | omct 6970 | is countable. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ | ||
Theorem | ctfoex 6971* | A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.) |
⊔ | ||
Syntax | comni 6972 | Extend class definition to include the class of omniscient sets. |
Omni | ||
Syntax | xnninf 6973 | Set of nonincreasing sequences in . |
ℕ∞ | ||
Definition | df-omni 6974* |
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 6975* | 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 9009 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 6295) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ∞ | ||
Theorem | isomni 6976* | The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.) |
Omni | ||
Theorem | isomnimap 6977* | The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni | ||
Theorem | enomnilem 6978 | Lemma for enomni 6979. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni Omni | ||
Theorem | enomni 6979 | 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 6295 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni Omni | ||
Theorem | finomni 6980 | 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 6981 | Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 6982. (Contributed by Jim Kingdon, 29-Jun-2022.) |
EXMID Omni | ||
Theorem | exmidomni 6982 | Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.) |
EXMID Omni | ||
Theorem | exmidlpo 6983 | Excluded middle implies the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 29-Mar-2023.) |
EXMID Omni | ||
Theorem | fodjuomnilemdc 6984* | Lemma for fodjuomni 6989. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊔ DECID inl | ||
Theorem | fodjuf 6985* | Lemma for fodjuomni 6989 and fodjumkv 7002. Domain and range of . (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊔ inl | ||
Theorem | fodjum 6986* | Lemma for fodjuomni 6989 and fodjumkv 7002. A condition which shows that is inhabited. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊔ inl | ||
Theorem | fodju0 6987* | Lemma for fodjuomni 6989 and fodjumkv 7002. A condition which shows that is empty. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊔ inl | ||
Theorem | fodjuomnilemres 6988* | Lemma for fodjuomni 6989. The final result with expressed as a local definition. (Contributed by Jim Kingdon, 29-Jul-2022.) |
Omni ⊔ inl | ||
Theorem | fodjuomni 6989* | 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 6990 | The point at infinity in ℕ∞ (the constant sequence equal to ). (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ∞ | ||
Theorem | nnnninf 6991* | 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 6990. Remark/TODO: the theorem still holds if , that is, the antecedent could be weakened to . (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ∞ | ||
Theorem | ctssexmid 6992* | The decidability condition in ctssdc 6966 is needed. More specifically, ctssdc 6966 minus that condition, plus the Limited Principle of Omniscience (LPO), implies excluded middle. (Contributed by Jim Kingdon, 15-Aug-2023.) |
⊔ Omni | ||
Syntax | cmarkov 6993 | Extend class definition to include the class of Markov sets. |
Markov | ||
Definition | df-markov 6994* |
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 6995* | The predicate of being Markov. (Contributed by Jim Kingdon, 18-Mar-2023.) |
Markov | ||
Theorem | ismkvmap 6996* | The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 18-Mar-2023.) |
Markov | ||
Theorem | ismkvnex 6997* | The predicate of being Markov stated in terms of double negation and comparison with . (Contributed by Jim Kingdon, 29-Nov-2023.) |
Markov | ||
Theorem | omnimkv 6998 | 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 6999 | Excluded middle implies Markov's Principle (MP). (Contributed by Jim Kingdon, 4-Apr-2023.) |
EXMID Markov | ||
Theorem | mkvprop 7000* | 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 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |