Home | Intuitionistic Logic Explorer Theorem List (p. 68 of 116) | < 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 | infminti 6701* | The smallest element of a set is its infimum. Note that the converse is not true; the infimum might not be an element of the set considered. (Contributed by Jim Kingdon, 18-Dec-2021.) |
inf | ||
Theorem | infmoti 6702* | Any class has at most one infimum in (where is interpreted as 'less than'). (Contributed by Jim Kingdon, 18-Dec-2021.) |
Theorem | infeuti 6703* | An infimum is unique. (Contributed by Jim Kingdon, 19-Dec-2021.) |
Theorem | infsnti 6704* | The infimum of a singleton. (Contributed by Jim Kingdon, 19-Dec-2021.) |
inf | ||
Theorem | inf00 6705 | The infimum regarding an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
inf | ||
Theorem | infisoti 6706* | Image of an infimum under an isomorphism. (Contributed by Jim Kingdon, 19-Dec-2021.) |
inf inf | ||
Theorem | ordiso2 6707 | Generalize ordiso 6708 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.) |
Theorem | ordiso 6708* | Order-isomorphic ordinal numbers are equal. (Contributed by Jeff Hankins, 16-Oct-2009.) (Proof shortened by Mario Carneiro, 24-Jun-2015.) |
Syntax | cdju 6709 | Extend class notation to include disjoint union of two classes. |
⊔ | ||
Definition | df-dju 6710 | Disjoint union of two classes. This is a way of creating a class which contains elements corresponding to each element of or , tagging each one with whether it came from or . (Contributed by Jim Kingdon, 20-Jun-2022.) |
⊔ | ||
Theorem | djueq12 6711 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊔ ⊔ | ||
Theorem | djueq1 6712 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊔ ⊔ | ||
Theorem | djueq2 6713 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊔ ⊔ | ||
Theorem | nfdju 6714 | Bound-variable hypothesis builder for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊔ | ||
Theorem | djuex 6715 | The disjoint union of sets is a set. (Contributed by AV, 28-Jun-2022.) |
⊔ | ||
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 6716 | Extend class notation to include left injection of a disjoint union. |
inl | ||
Syntax | cinr 6717 | Extend class notation to include right injection of a disjoint union. |
inr | ||
Definition | df-inl 6718 | Left injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
inl | ||
Definition | df-inr 6719 | Right injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
inr | ||
Theorem | djulclr 6720 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
inl ⊔ | ||
Theorem | djurclr 6721 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
inr ⊔ | ||
Theorem | djulcl 6722 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
inl ⊔ | ||
Theorem | djurcl 6723 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
inr ⊔ | ||
Theorem | djuf1olem 6724* | Lemma for djulf1o 6729 and djurf1o 6730. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
Theorem | djuf1olemr 6725* | Lemma for djulf1or 6727 and djurf1or 6728. Remark: maybe a version of this lemma with defined on and no restriction in the conclusion would be more usable. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
Theorem | djulclb 6726 | Left biconditional closure of disjoint union. (Contributed by Jim Kingdon, 2-Jul-2022.) |
inl ⊔ | ||
Theorem | djulf1or 6727 | 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 6728 | 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 6729 | The left injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.) |
inl | ||
Theorem | djurf1o 6730 | The right injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.) |
inr | ||
Theorem | inresflem 6731* | Lemma for inlresf1 6732 and inrresf1 6733. (Contributed by BJ, 4-Jul-2022.) |
Theorem | inlresf1 6732 | 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 6733 | 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 6734 | The ranges of any left and right injections are disjoint. Remark: the restrictions seem not necessary, but the proof is not much longer than the proof of inl inr (which is easily recovered from it, as in the proof of casefun 6755). (Contributed by BJ and Jim Kingdon, 21-Jun-2022.) |
inl inr | ||
Theorem | djuin 6735 | The images of any classes under right and left injection produce disjoint sets. (Contributed by Jim Kingdon, 21-Jun-2022.) |
inl inr | ||
Theorem | djur 6736* | A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊔ inl inr | ||
Theorem | djuunr 6737 | 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 | eldju 6738* | Element of a disjoint union. (Contributed by BJ and Jim Kingdon, 23-Jun-2022.) |
⊔ inl inr | ||
Theorem | djuun 6739 | 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 | djuss 6740 | A disjoint union is a subset of a Cartesian product. (Contributed by AV, 25-Jun-2022.) |
⊔ | ||
Theorem | eldju1st 6741 | The first component of an element of a disjoint union is either or . (Contributed by AV, 26-Jun-2022.) |
⊔ | ||
Theorem | eldju2ndl 6742 | 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 6743 | 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 6744 | The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.) |
inl | ||
Theorem | 2ndinl 6745 | The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.) |
inl | ||
Theorem | 1stinr 6746 | The first component of the value of a right injection is . (Contributed by AV, 27-Jun-2022.) |
inr | ||
Theorem | 2ndinr 6747 | The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.) |
inr | ||
Theorem | djune 6748 | Left and right injection never produce equal values. (Contributed by Jim Kingdon, 2-Jul-2022.) |
inl inr | ||
Theorem | updjudhf 6749* | 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 6750* | 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 6751* | 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 6752* | Universal property of the disjoint union. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.) |
⊔ inl inr | ||
Syntax | cdjucase 6753 | Syntax for the "case" construction. |
case | ||
Definition | df-case 6754 | 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. 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 6755 | The "case" construction of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
case | ||
Theorem | casedm 6756 | 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 6757 | 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 6758 | 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 6759 | The "case" construction of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.) |
case | ||
Theorem | casef1 6760 | The "case" construction of two injective functions with disjoint ranges is an injective function. (Contributed by BJ, 10-Jul-2022.) |
case ⊔ | ||
Syntax | cdjud 6761 | Syntax for the domain-disjoint-union of two relations. |
⊔d | ||
Definition | df-djud 6762 |
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.
Remark: the restrictions to (resp. ) are not necessary since extra stuff would be thrown away in the post-composition with (resp. ), but they are explicitly written for clarity. (Contributed by MC and BJ, 10-Jul-2022.) |
⊔d inl inr | ||
Theorem | djufun 6763 | The "domain-disjoint-union" of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
⊔d | ||
Theorem | djudm 6764 | 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 6765 | The "domain-disjoint-union" of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.) |
⊔d | ||
Theorem | djudom 6766 | Dominance law for disjoint union. (Contributed by Jim Kingdon, 25-Jul-2022.) |
⊔ ⊔ | ||
Syntax | comni 6767 | Extend class definition to include the class of omniscient sets. |
Omni | ||
Syntax | xnninf 6768 | Set of nonincreasing sequences in . |
ℕ_{∞} | ||
Definition | df-omni 6769* |
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 Lesser Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 28-Jun-2022.) |
Omni | ||
Definition | df-nninf 6770* | 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 8707 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 6177) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ_{∞} | ||
Theorem | isomni 6771* | The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.) |
Omni | ||
Theorem | isomnimap 6772* | The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni | ||
Theorem | enomnilem 6773 | Lemma for enomni 6774. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni Omni | ||
Theorem | enomni 6774 | Omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Lesser Principle of Omniscience as either Omni or Omni. The former is a better match to conventional notation in the sense that df2o3 6177 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni Omni | ||
Theorem | finomni 6775 | 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 6776 | Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 6777. (Contributed by Jim Kingdon, 29-Jun-2022.) |
EXMID Omni | ||
Theorem | exmidomni 6777 | Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.) |
EXMID Omni | ||
Theorem | fodjuomnilemdc 6778* | Lemma for fodjuomni 6783. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊔ DECID inl | ||
Theorem | fodjuomnilemf 6779* | Lemma for fodjuomni 6783. Domain and range of . (Contributed by Jim Kingdon, 27-Jul-2022.) |
Omni ⊔ inl | ||
Theorem | fodjuomnilemm 6780* | Lemma for fodjuomni 6783. The case where A is inhabited. (Contributed by Jim Kingdon, 27-Jul-2022.) |
Omni ⊔ inl | ||
Theorem | fodjuomnilem0 6781* | Lemma for fodjuomni 6783. The case where A is empty. (Contributed by Jim Kingdon, 27-Jul-2022.) |
Omni ⊔ inl | ||
Theorem | fodjuomnilemres 6782* | Lemma for fodjuomni 6783. The final result with broken out into a hypothesis. (Contributed by Jim Kingdon, 29-Jul-2022.) |
Omni ⊔ inl | ||
Theorem | fodjuomni 6783* | 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 6784 | The point at infinity in ℕ_{∞} (the constant sequence equal to ). (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ_{∞} | ||
Theorem | nnnninf 6785* | 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 6784. Remark/TODO: the theorem still holds if , that is, the antecedent could be weakened to . (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ_{∞} | ||
Syntax | ccrd 6786 | Extend class definition to include the cardinal size function. |
Definition | df-card 6787* | 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 6788* | The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | isnumi 6789 | A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | finnum 6790 | Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
Theorem | onenon 6791 | Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | cardval3ex 6792* | The value of . (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | oncardval 6793* | 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 6794 | 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 6795 | The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.) |
Theorem | carden2bex 6796* | If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | pm54.43 6797 | Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.) |
Theorem | pr2nelem 6798 | Lemma for pr2ne 6799. (Contributed by FL, 17-Aug-2008.) |
Theorem | pr2ne 6799 | If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.) |
Theorem | en2eleq 6800 | 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.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |