Home | Metamath
Proof Explorer Theorem List (p. 67 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | f1oiso 6601* | Any one-to-one onto function determines an isomorphism with an induced relation . Proposition 6.33 of [TakeutiZaring] p. 34. (Contributed by NM, 30-Apr-2004.) |
Theorem | f1oiso2 6602* | Any one-to-one onto function determines an isomorphism with an induced relation . (Contributed by Mario Carneiro, 9-Mar-2013.) |
Theorem | f1owe 6603* | Well-ordering of isomorphic relations. (Contributed by NM, 4-Mar-1997.) |
Theorem | weniso 6604 | A set-like well-ordering has no nontrivial automorphisms. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.) |
Se | ||
Theorem | weisoeq 6605 | Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso 7153. (Contributed by Mario Carneiro, 25-Jun-2015.) |
Se | ||
Theorem | weisoeq2 6606 | Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso2 7154. (Contributed by Mario Carneiro, 25-Jun-2015.) |
Se | ||
Theorem | knatar 6607* | The Knaster-Tarski theorem says that every monotone function over a complete lattice has a (least) fixpoint. Here we specialize this theorem to the case when the lattice is the powerset lattice . (Contributed by Mario Carneiro, 11-Jun-2015.) |
Theorem | canth 6608 | No set is equinumerous to its power set (Cantor's theorem), i.e. no function can map it onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. For the equinumerosity version, see canth2 8113. Note that must be a set: this theorem does not hold when is too large to be a set; see ncanth 6609 for a counterexample. (Use nex 1731 if you want the form .) (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mario Carneiro, 7-Jun-2016.) |
Theorem | ncanth 6609 | Cantor's theorem fails for the universal class (which is not a set but a proper class by vprc 4796). Specifically, the identity function maps the universe onto its power class. Compare canth 6608 that works for sets. See also the remark in ru 3434 about NF, in which Cantor's theorem fails for sets that are "too large." This theorem gives some intuition behind that failure: in NF the universal class is a set, and it equals its own power set. (Contributed by NM, 29-Jun-2004.) |
Syntax | crio 6610 | Extend class notation with restricted description binder. |
Definition | df-riota 6611 | Define restricted description binder. In case there is no unique such that holds, it evaluates to the empty set. See also comments for df-iota 5851. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.) |
Theorem | riotaeqdv 6612* | Formula-building deduction rule for iota. (Contributed by NM, 15-Sep-2011.) |
Theorem | riotabidv 6613* | Formula-building deduction rule for restricted iota. (Contributed by NM, 15-Sep-2011.) |
Theorem | riotaeqbidv 6614* | Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.) |
Theorem | riotaex 6615 | Restricted iota is a set. (Contributed by NM, 15-Sep-2011.) |
Theorem | riotav 6616 | An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.) |
Theorem | riotauni 6617 | Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.) |
Theorem | nfriota1 6618* | The abstraction variable in a restricted iota descriptor isn't free. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | nfriotad 6619 | Deduction version of nfriota 6620. (Contributed by NM, 18-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | nfriota 6620* | A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.) |
Theorem | cbvriota 6621* | Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | cbvriotav 6622* | Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | csbriota 6623* | Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 2-Sep-2018.) |
Theorem | riotacl2 6624 |
Membership law for "the unique element in such that ."
(Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
Theorem | riotacl 6625* | Closure of restricted iota. (Contributed by NM, 21-Aug-2011.) |
Theorem | riotasbc 6626 | Substitution law for descriptions. Compare iotasbc 38620. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
Theorem | riotabidva 6627* | Equivalent wff's yield equal restricted class abstractions (deduction rule). (rabbidva 3188 analog.) (Contributed by NM, 17-Jan-2012.) |
Theorem | riotabiia 6628 | Equivalent wff's yield equal restricted iotas (inference rule). (rabbiia 3185 analog.) (Contributed by NM, 16-Jan-2012.) |
Theorem | riota1 6629* | Property of restricted iota. Compare iota1 5865. (Contributed by Mario Carneiro, 15-Oct-2016.) |
Theorem | riota1a 6630 | Property of iota. (Contributed by NM, 23-Aug-2011.) |
Theorem | riota2df 6631* | A deduction version of riota2f 6632. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | riota2f 6632* | This theorem shows a condition that allows us to represent a descriptor with a class expression . (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | riota2 6633* | This theorem shows a condition that allows us to represent a descriptor with a class expression . (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.) |
Theorem | riotaeqimp 6634* | If two restricted iota descriptors for an equality are equal, then the terms of the equality are equal. (Contributed by AV, 6-Dec-2020.) |
Theorem | riotaprop 6635* | Properties of a restricted definite description operator. TODO (df-riota 6611 update): can some uses of riota2f 6632 be shortened with this? (Contributed by NM, 23-Nov-2013.) |
Theorem | riota5f 6636* | A method for computing restricted iota. (Contributed by NM, 16-Apr-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | riota5 6637* | A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.) |
Theorem | riotass2 6638* | Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011.) (Revised by NM, 22-Mar-2013.) |
Theorem | riotass 6639* | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.) |
Theorem | moriotass 6640* | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.) |
Theorem | snriota 6641 | A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006.) |
Theorem | riotaxfrd 6642* | Change the variable in the expression for "the unique such that " to another variable contained in expression . Use reuhypd 4895 to eliminate the last hypothesis. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | eusvobj2 6643* | Specify the same property in two ways when class is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
Theorem | eusvobj1 6644* | Specify the same object in two ways when class is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
Theorem | f1ofveu 6645* | There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.) |
Theorem | f1ocnvfv3 6646* | Value of the converse of a one-to-one onto function. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
Theorem | riotaund 6647* | Restricted iota equals the empty set when not meaningful. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 13-Sep-2018.) |
Theorem | riotassuni 6648* | The restricted iota class is limited in size by the base set. (Contributed by Mario Carneiro, 24-Dec-2016.) |
Theorem | riotaclb 6649* | Bidirectional closure of restricted iota when domain is not empty. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.) (Revised by NM, 13-Sep-2018.) |
Syntax | co 6650 | Extend class notation to include the value of an operation (such as ) for two arguments and . Note that the syntax is simply three class symbols in a row surrounded by parentheses. Since operation values are the only possible class expressions consisting of three class expressions in a row surrounded by parentheses, the syntax is unambiguous. (For an example of how syntax could become ambiguous if we are not careful, see the comment in cneg 10267.) |
Syntax | coprab 6651 | Extend class notation to include class abstraction (class builder) of nested ordered pairs. |
Syntax | cmpt2 6652 | Extend the definition of a class to include maps-to notation for defining an operation via a rule. |
Definition | df-ov 6653 | Define the value of an operation. Definition of operation value in [Enderton] p. 79. Note that the syntax is simply three class expressions in a row bracketed by parentheses. There are no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation and its arguments and - will be useful for proving meaningful theorems. For example, if class is the operation and arguments and are and , the expression can be proved to equal (see 3p2e5 11160). This definition is well-defined, although not very meaningful, when classes and/or are proper classes (i.e. are not sets); see ovprc1 6684 and ovprc2 6685. On the other hand, we often find uses for this definition when is a proper class, such as in oav 7591. is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6654. (Contributed by NM, 28-Feb-1995.) |
Definition | df-oprab 6654* | Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally , , and are distinct, although the definition doesn't strictly require it. See df-ov 6653 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by ovmpt2 6796. (Contributed by NM, 12-Mar-1995.) |
Definition | df-mpt2 6655* | Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from (in ) to ." An extension of df-mpt 4730 for two arguments. (Contributed by NM, 17-Feb-2008.) |
Theorem | oveq 6656 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq1 6657 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq2 6658 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq12 6659 | Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.) |
Theorem | oveq1i 6660 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq2i 6661 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
Theorem | oveq12i 6662 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | oveqi 6663 | Equality inference for operation value. (Contributed by NM, 24-Nov-2007.) |
Theorem | oveq123i 6664 | Equality inference for operation value. (Contributed by FL, 11-Jul-2010.) |
Theorem | oveq1d 6665 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
Theorem | oveq2d 6666 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
Theorem | oveqd 6667 | Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.) |
Theorem | oveq12d 6668 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | oveqan12d 6669 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
Theorem | oveqan12rd 6670 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
Theorem | oveq123d 6671 | Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.) |
Theorem | ovrspc2v 6672* | If an operation value is element of a class for all operands of two classes, then the operation value is an element of the class for specific operands of the two classes. (Contributed by Mario Carneiro, 6-Dec-2014.) |
Theorem | oveqrspc2v 6673* | Restricted specialization of operands, using implicit substitution. (Contributed by Mario Carneiro, 6-Dec-2014.) |
Theorem | oveqdr 6674 | Equality of two operations for any two operands. Useful in proofs using *propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.) |
Theorem | nfovd 6675 | Deduction version of bound-variable hypothesis builder nfov 6676. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | nfov 6676 | Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.) |
Theorem | oprabid 6677 | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 20-Mar-2013.) |
Theorem | ovex 6678 | The result of an operation is a set. (Contributed by NM, 13-Mar-1995.) |
Theorem | ovexi 6679 | The result of an operation is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Theorem | ovexd 6680 | The result of an operation is a set (common case). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
Theorem | ovssunirn 6681 | The result of an operation value is always a subset of the union of the range. (Contributed by Mario Carneiro, 12-Jan-2017.) |
Theorem | 0ov 6682 | Operation value of the empty set. (Contributed by AV, 15-May-2021.) |
Theorem | ovprc 6683 | The value of an operation when the one of the arguments is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | ovprc1 6684 | The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.) |
Theorem | ovprc2 6685 | The value of an operation when the second argument is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | ovrcl 6686 | Reverse closure for an operation value. (Contributed by Mario Carneiro, 5-May-2015.) |
Theorem | csbov123 6687 | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Revised by NM, 23-Aug-2018.) |
Theorem | csbov 6688* | Move class substitution in and out of an operation. (Contributed by NM, 23-Aug-2018.) |
Theorem | csbov12g 6689* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
Theorem | csbov1g 6690* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
Theorem | csbov2g 6691* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
Theorem | rspceov 6692* | A frequently used special case of rspc2ev 3324 for operation values. (Contributed by NM, 21-Mar-2007.) |
Theorem | elovimad 6693 | Elementhood of the image set of an operation value. (Contributed by Thierry Arnoux, 13-Mar-2017.) |
Theorem | fnotovb 6694 | Equivalence of operation value and ordered triple membership, analogous to fnopfvb 6237. (Contributed by NM, 17-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | opabbrex 6695 | A collection of ordered pairs with an extension of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by BJ/AV, 20-Jun-2019.) (Proof shortened by OpenAI, 25-Mar-2020.) |
Theorem | opabresex2d 6696* | Restrictions of a collection of ordered pairs of related elements are sets. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 15-Jan-2021.) |
Theorem | fvmptopab 6697* | The function value of a mapping to a restricted binary relation expressed as an ordered-pair class abstraction: The restricted binary relation is a binary relation given as value of a function restricted by the condition . (Contributed by AV, 31-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
Theorem | 0neqopab 6698 | The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.) |
Theorem | brabv 6699 | If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Alexander van der Vekens, 5-Nov-2017.) |
Theorem | brfvopab 6700 | The classes involved in a binary relation of a function value which is an ordered-pair class abstraction are sets. (Contributed by AV, 7-Jan-2021.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |