Home | Intuitionistic Logic Explorer Theorem List (p. 71 of 139) | < 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 | djuexb 7001 | The disjoint union of two classes is a set iff both classes are sets. (Contributed by Jim Kingdon, 6-Sep-2023.) |
⊔ | ||
In this section, we define the left and right injections of a disjoint union and prove their main properties. These injections are restrictions of the "template" functions inl and inr, which appear in most applications in the form inl and inr . | ||
Syntax | cinl 7002 | Extend class notation to include left injection of a disjoint union. |
inl | ||
Syntax | cinr 7003 | Extend class notation to include right injection of a disjoint union. |
inr | ||
Definition | df-inl 7004 | Left injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
inl | ||
Definition | df-inr 7005 | Right injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
inr | ||
Theorem | djulclr 7006 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
inl ⊔ | ||
Theorem | djurclr 7007 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
inr ⊔ | ||
Theorem | djulcl 7008 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
inl ⊔ | ||
Theorem | djurcl 7009 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
inr ⊔ | ||
Theorem | djuf1olem 7010* | Lemma for djulf1o 7015 and djurf1o 7016. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
Theorem | djuf1olemr 7011* | Lemma for djulf1or 7013 and djurf1or 7014. For a version of this lemma with defined on and no restriction in the conclusion, see djuf1olem 7010. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
Theorem | djulclb 7012 | Left biconditional closure of disjoint union. (Contributed by Jim Kingdon, 2-Jul-2022.) |
inl ⊔ | ||
Theorem | djulf1or 7013 | 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 7014 | 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 7015 | The left injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.) |
inl | ||
Theorem | djurf1o 7016 | The right injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.) |
inr | ||
Theorem | inresflem 7017* | Lemma for inlresf1 7018 and inrresf1 7019. (Contributed by BJ, 4-Jul-2022.) |
Theorem | inlresf1 7018 | 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 7019 | 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 7020 | 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 7050 and djufun 7061) while the simpler statement inl inr is easily recovered from it by substituting for both and as done in casefun 7042). (Contributed by BJ and Jim Kingdon, 21-Jun-2022.) |
inl inr | ||
Theorem | djuin 7021 | 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 7022 | Left injection is one-to-one. (Contributed by Jim Kingdon, 12-Jul-2023.) |
inl inl | ||
Theorem | djuunr 7023 | 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 7024 | 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 7025* | Element of a disjoint union. (Contributed by BJ and Jim Kingdon, 23-Jun-2022.) |
⊔ inl inr | ||
Theorem | djur 7026* | 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 7027 | A disjoint union is a subset of a Cartesian product. (Contributed by AV, 25-Jun-2022.) |
⊔ | ||
Theorem | eldju1st 7028 | The first component of an element of a disjoint union is either or . (Contributed by AV, 26-Jun-2022.) |
⊔ | ||
Theorem | eldju2ndl 7029 | 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 7030 | 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 7031 | The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.) |
inl | ||
Theorem | 2ndinl 7032 | The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.) |
inl | ||
Theorem | 1stinr 7033 | The first component of the value of a right injection is . (Contributed by AV, 27-Jun-2022.) |
inr | ||
Theorem | 2ndinr 7034 | The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.) |
inr | ||
Theorem | djune 7035 | Left and right injection never produce equal values. (Contributed by Jim Kingdon, 2-Jul-2022.) |
inl inr | ||
Theorem | updjudhf 7036* | 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 7037* | 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 7038* | 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 7039* | Universal property of the disjoint union. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.) |
⊔ inl inr | ||
Syntax | cdjucase 7040 | Syntax for the "case" construction. |
case | ||
Definition | df-case 7041 | 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 7039. 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 7042 | The "case" construction of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
case | ||
Theorem | casedm 7043 | 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 7044 | 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 7045 | 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 7046 | The "case" construction of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.) |
case | ||
Theorem | casef1 7047 | The "case" construction of two injective functions with disjoint ranges is an injective function. (Contributed by BJ, 10-Jul-2022.) |
case ⊔ | ||
Theorem | caseinl 7048 | Applying the "case" construction to a left injection. (Contributed by Jim Kingdon, 15-Mar-2023.) |
case inl | ||
Theorem | caseinr 7049 | Applying the "case" construction to a right injection. (Contributed by Jim Kingdon, 12-Jul-2023.) |
case inr | ||
Theorem | djudom 7050 | Dominance law for disjoint union. (Contributed by Jim Kingdon, 25-Jul-2022.) |
⊔ ⊔ | ||
Theorem | omp1eomlem 7051* | Lemma for omp1eom 7052. (Contributed by Jim Kingdon, 11-Jul-2023.) |
inr inl case ⊔ | ||
Theorem | omp1eom 7052 | Adding one to . (Contributed by Jim Kingdon, 10-Jul-2023.) |
⊔ | ||
Theorem | endjusym 7053 | Reversing right and left operands of a disjoint union produces an equinumerous result. (Contributed by Jim Kingdon, 10-Jul-2023.) |
⊔ ⊔ | ||
Theorem | eninl 7054 | Equinumerosity of a set and its image under left injection. (Contributed by Jim Kingdon, 30-Jul-2023.) |
inl | ||
Theorem | eninr 7055 | Equinumerosity of a set and its image under right injection. (Contributed by Jim Kingdon, 30-Jul-2023.) |
inr | ||
Theorem | difinfsnlem 7056* | Lemma for difinfsn 7057. 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 7057* | 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 7058* | 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 7059 | Syntax for the domain-disjoint-union of two relations. |
⊔d | ||
Definition | df-djud 7060 |
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 7039 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 7041, but they are explicitly written for clarity. (Contributed by MC and BJ, 10-Jul-2022.) |
⊔d inl inr | ||
Theorem | djufun 7061 | The "domain-disjoint-union" of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
⊔d | ||
Theorem | djudm 7062 | 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 7063 | The "domain-disjoint-union" of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.) |
⊔d | ||
Theorem | 0ct 7064 | 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 7065* | Lemma for ctm 7066. One of the directions of the biconditional. (Contributed by Jim Kingdon, 16-Mar-2023.) |
⊔ | ||
Theorem | ctm 7066* | Two equivalent definitions of countable for an inhabited set. Remark of [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊔ | ||
Theorem | ctssdclemn0 7067* | Lemma for ctssdc 7070. The case. (Contributed by Jim Kingdon, 16-Aug-2023.) |
DECID ⊔ | ||
Theorem | ctssdccl 7068* | A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 7070 but expressed in terms of classes rather than . (Contributed by Jim Kingdon, 30-Oct-2023.) |
⊔ inl inl DECID | ||
Theorem | ctssdclemr 7069* | Lemma for ctssdc 7070. Showing that our usual definition of countable implies the alternate one. (Contributed by Jim Kingdon, 16-Aug-2023.) |
⊔ DECID | ||
Theorem | ctssdc 7070* | 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 7106. (Contributed by Jim Kingdon, 15-Aug-2023.) |
DECID ⊔ | ||
Theorem | enumctlemm 7071* | Lemma for enumct 7072. The case where is greater than zero. (Contributed by Jim Kingdon, 13-Mar-2023.) |
Theorem | enumct 7072* | 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 7073* | A finite set is countable. (Contributed by Jim Kingdon, 17-Mar-2023.) |
⊔ | ||
Theorem | omct 7074 | is countable. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ | ||
Theorem | ctfoex 7075* | A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.) |
⊔ | ||
This section introduces the one-point compactification of the set of natural numbers, introduced by Escardo as the set of nonincreasing sequences on with values in . The topological results justifying its name will be proved later. | ||
Syntax | xnninf 7076 | Set of nonincreasing sequences in . |
ℕ_{∞} | ||
Definition | df-nninf 7077* | 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 9170 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 6390) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ_{∞} | ||
Theorem | nninfex 7078 | ℕ_{∞} is a set. (Contributed by Jim Kingdon, 10-Aug-2022.) |
ℕ_{∞} | ||
Theorem | nninff 7079 | An element of ℕ_{∞} is a sequence of zeroes and ones. (Contributed by Jim Kingdon, 4-Aug-2022.) |
ℕ_{∞} | ||
Theorem | infnninf 7080 | The point at infinity in ℕ_{∞} is the constant sequence equal to . Note that with our encoding of functions, that constant function can also be expressed as , as fconstmpt 4646 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.) |
ℕ_{∞} | ||
Theorem | infnninfOLD 7081 | Obsolete version of infnninf 7080 as of 10-Aug-2024. (Contributed by Jim Kingdon, 14-Jul-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
ℕ_{∞} | ||
Theorem | nnnninf 7082* | 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 7083. (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ_{∞} | ||
Theorem | nnnninf2 7083* | Canonical embedding of into ℕ_{∞}. (Contributed by BJ, 10-Aug-2024.) |
ℕ_{∞} | ||
Theorem | nnnninfeq 7084* | Mapping of a natural number to an element of ℕ_{∞}. (Contributed by Jim Kingdon, 4-Aug-2022.) |
ℕ_{∞} | ||
Theorem | nnnninfeq2 7085* | Mapping of a natural number to an element of ℕ_{∞}. Similar to nnnninfeq 7084 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 7086* | Lemma for nninfisol 7089. The case where is zero. (Contributed by Jim Kingdon, 13-Sep-2024.) |
ℕ_{∞} DECID | ||
Theorem | nninfisollemne 7087* | Lemma for nninfisol 7089. A case where is a successor and and are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.) |
ℕ_{∞} DECID | ||
Theorem | nninfisollemeq 7088* | Lemma for nninfisol 7089. The case where is a successor and and are equal. (Contributed by Jim Kingdon, 13-Sep-2024.) |
ℕ_{∞} DECID | ||
Theorem | nninfisol 7089* | 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 7090 | Extend class definition to include the class of omniscient sets. |
Omni | ||
Definition | df-omni 7091* |
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 7092* | The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.) |
Omni | ||
Theorem | isomnimap 7093* | The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni | ||
Theorem | enomnilem 7094 | Lemma for enomni 7095. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni Omni | ||
Theorem | enomni 7095 | 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 6390 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni Omni | ||
Theorem | finomni 7096 | 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 7097 | Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 7098. (Contributed by Jim Kingdon, 29-Jun-2022.) |
EXMID Omni | ||
Theorem | exmidomni 7098 | Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.) |
EXMID Omni | ||
Theorem | exmidlpo 7099 | Excluded middle implies the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 29-Mar-2023.) |
EXMID Omni | ||
Theorem | fodjuomnilemdc 7100* | Lemma for fodjuomni 7105. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊔ DECID inl |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |