![]() |
Metamath
Proof Explorer Theorem List (p. 75 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eusvobj2 7401* | 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.) |
โข ๐ต โ V โ โข (โ!๐ฅโ๐ฆ โ ๐ด ๐ฅ = ๐ต โ (โ๐ฆ โ ๐ด ๐ฅ = ๐ต โ โ๐ฆ โ ๐ด ๐ฅ = ๐ต)) | ||
Theorem | eusvobj1 7402* | 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.) |
โข ๐ต โ V โ โข (โ!๐ฅโ๐ฆ โ ๐ด ๐ฅ = ๐ต โ (โฉ๐ฅโ๐ฆ โ ๐ด ๐ฅ = ๐ต) = (โฉ๐ฅโ๐ฆ โ ๐ด ๐ฅ = ๐ต)) | ||
Theorem | f1ofveu 7403* | There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.) |
โข ((๐น:๐ดโ1-1-ontoโ๐ต โง ๐ถ โ ๐ต) โ โ!๐ฅ โ ๐ด (๐นโ๐ฅ) = ๐ถ) | ||
Theorem | f1ocnvfv3 7404* | 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.) |
โข ((๐น:๐ดโ1-1-ontoโ๐ต โง ๐ถ โ ๐ต) โ (โก๐นโ๐ถ) = (โฉ๐ฅ โ ๐ด (๐นโ๐ฅ) = ๐ถ)) | ||
Theorem | riotaund 7405* | 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 7406* | The restricted iota class is limited in size by the base set. (Contributed by Mario Carneiro, 24-Dec-2016.) |
โข (โฉ๐ฅ โ ๐ด ๐) โ (๐ซ โช ๐ด โช โช ๐ด) | ||
Theorem | riotaclb 7407* | 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.) |
โข (ยฌ โ โ ๐ด โ (โ!๐ฅ โ ๐ด ๐ โ (โฉ๐ฅ โ ๐ด ๐) โ ๐ด)) | ||
Theorem | riotarab 7408* | Restricted iota of a restricted abstraction. (Contributed by Scott Fenton, 8-Aug-2024.) |
โข (๐ฅ = ๐ฆ โ (๐ โ ๐)) โ โข (โฉ๐ฅ โ {๐ฆ โ ๐ด โฃ ๐}๐) = (โฉ๐ฅ โ ๐ด (๐ โง ๐)) | ||
Syntax | co 7409 | 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 11445.) |
class (๐ด๐น๐ต) | ||
Syntax | coprab 7410 | Extend class notation to include class abstraction (class builder) of nested ordered pairs. |
class {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} | ||
Syntax | cmpo 7411 | Extend the definition of a class to include maps-to notation for defining an operation via a rule. |
class (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) | ||
Definition | df-ov 7412 | 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 3 and 2, the expression (3 + 2) can be proved to equal 5 (see 3p2e5 12363). This definition is well-defined, although not very meaningful, when classes ๐ด and/or ๐ต are proper classes (i.e. are not sets); see ovprc1 7448 and ovprc2 7449. On the other hand, we often find uses for this definition when ๐น is a proper class, such as +o in oav 8511. ๐น is normally equal to a class of nested ordered pairs of the form defined by df-oprab 7413. (Contributed by NM, 28-Feb-1995.) |
โข (๐ด๐น๐ต) = (๐นโโจ๐ด, ๐ตโฉ) | ||
Definition | df-oprab 7413* | 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 7412 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 an operation given by a class abstraction is given by ovmpo 7568. (Contributed by NM, 12-Mar-1995.) |
โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {๐ค โฃ โ๐ฅโ๐ฆโ๐ง(๐ค = โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โง ๐)} | ||
Definition | df-mpo 7414* | 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 5233 for two arguments. (Contributed by NM, 17-Feb-2008.) |
โข (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โง ๐ง = ๐ถ)} | ||
Theorem | oveq 7415 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
โข (๐น = ๐บ โ (๐ด๐น๐ต) = (๐ด๐บ๐ต)) | ||
Theorem | oveq1 7416 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
โข (๐ด = ๐ต โ (๐ด๐น๐ถ) = (๐ต๐น๐ถ)) | ||
Theorem | oveq2 7417 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
โข (๐ด = ๐ต โ (๐ถ๐น๐ด) = (๐ถ๐น๐ต)) | ||
Theorem | oveq12 7418 | Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.) |
โข ((๐ด = ๐ต โง ๐ถ = ๐ท) โ (๐ด๐น๐ถ) = (๐ต๐น๐ท)) | ||
Theorem | oveq1i 7419 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
โข ๐ด = ๐ต โ โข (๐ด๐น๐ถ) = (๐ต๐น๐ถ) | ||
Theorem | oveq2i 7420 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
โข ๐ด = ๐ต โ โข (๐ถ๐น๐ด) = (๐ถ๐น๐ต) | ||
Theorem | oveq12i 7421 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
โข ๐ด = ๐ต & โข ๐ถ = ๐ท โ โข (๐ด๐น๐ถ) = (๐ต๐น๐ท) | ||
Theorem | oveqi 7422 | Equality inference for operation value. (Contributed by NM, 24-Nov-2007.) |
โข ๐ด = ๐ต โ โข (๐ถ๐ด๐ท) = (๐ถ๐ต๐ท) | ||
Theorem | oveq123i 7423 | Equality inference for operation value. (Contributed by FL, 11-Jul-2010.) |
โข ๐ด = ๐ถ & โข ๐ต = ๐ท & โข ๐น = ๐บ โ โข (๐ด๐น๐ต) = (๐ถ๐บ๐ท) | ||
Theorem | oveq1d 7424 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐ด๐น๐ถ) = (๐ต๐น๐ถ)) | ||
Theorem | oveq2d 7425 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐ถ๐น๐ด) = (๐ถ๐น๐ต)) | ||
Theorem | oveqd 7426 | Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.) |
โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐ถ๐ด๐ท) = (๐ถ๐ต๐ท)) | ||
Theorem | oveq12d 7427 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
โข (๐ โ ๐ด = ๐ต) & โข (๐ โ ๐ถ = ๐ท) โ โข (๐ โ (๐ด๐น๐ถ) = (๐ต๐น๐ท)) | ||
Theorem | oveqan12d 7428 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
โข (๐ โ ๐ด = ๐ต) & โข (๐ โ ๐ถ = ๐ท) โ โข ((๐ โง ๐) โ (๐ด๐น๐ถ) = (๐ต๐น๐ท)) | ||
Theorem | oveqan12rd 7429 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
โข (๐ โ ๐ด = ๐ต) & โข (๐ โ ๐ถ = ๐ท) โ โข ((๐ โง ๐) โ (๐ด๐น๐ถ) = (๐ต๐น๐ท)) | ||
Theorem | oveq123d 7430 | Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.) |
โข (๐ โ ๐น = ๐บ) & โข (๐ โ ๐ด = ๐ต) & โข (๐ โ ๐ถ = ๐ท) โ โข (๐ โ (๐ด๐น๐ถ) = (๐ต๐บ๐ท)) | ||
Theorem | fvoveq1d 7431 | Equality deduction for nested function and operation value. (Contributed by AV, 23-Jul-2022.) |
โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ (๐นโ(๐ด๐๐ถ)) = (๐นโ(๐ต๐๐ถ))) | ||
Theorem | fvoveq1 7432 | Equality theorem for nested function and operation value. Closed form of fvoveq1d 7431. (Contributed by AV, 23-Jul-2022.) |
โข (๐ด = ๐ต โ (๐นโ(๐ด๐๐ถ)) = (๐นโ(๐ต๐๐ถ))) | ||
Theorem | ovanraleqv 7433* | Equality theorem for a conjunction with an operation values within a restricted universal quantification. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.) |
โข (๐ต = ๐ โ (๐ โ ๐)) โ โข (๐ต = ๐ โ (โ๐ฅ โ ๐ (๐ โง (๐ด ยท ๐ต) = ๐ถ) โ โ๐ฅ โ ๐ (๐ โง (๐ด ยท ๐) = ๐ถ))) | ||
Theorem | imbrov2fvoveq 7434 | Equality theorem for nested function and operation value in an implication for a binary relation. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 17-Aug-2022.) |
โข (๐ = ๐ โ (๐ โ ๐)) โ โข (๐ = ๐ โ ((๐ โ (๐นโ((๐บโ๐) ยท ๐))๐ ๐ด) โ (๐ โ (๐นโ((๐บโ๐) ยท ๐))๐ ๐ด))) | ||
Theorem | ovrspc2v 7435* | 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 7436* | Restricted specialization of operands, using implicit substitution. (Contributed by Mario Carneiro, 6-Dec-2014.) |
โข ((๐ โง (๐ฅ โ ๐ด โง ๐ฆ โ ๐ต)) โ (๐ฅ๐น๐ฆ) = (๐ฅ๐บ๐ฆ)) โ โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ (๐๐น๐) = (๐๐บ๐)) | ||
Theorem | oveqdr 7437 | Equality of two operations for any two operands. Useful in proofs using *propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.) |
โข (๐ โ ๐น = ๐บ) โ โข ((๐ โง ๐) โ (๐ฅ๐น๐ฆ) = (๐ฅ๐บ๐ฆ)) | ||
Theorem | nfovd 7438 | Deduction version of bound-variable hypothesis builder nfov 7439. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
โข (๐ โ โฒ๐ฅ๐ด) & โข (๐ โ โฒ๐ฅ๐น) & โข (๐ โ โฒ๐ฅ๐ต) โ โข (๐ โ โฒ๐ฅ(๐ด๐น๐ต)) | ||
Theorem | nfov 7439 | Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.) |
โข โฒ๐ฅ๐ด & โข โฒ๐ฅ๐น & โข โฒ๐ฅ๐ต โ โข โฒ๐ฅ(๐ด๐น๐ต) | ||
Theorem | oprabidw 7440* | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of oprabid 7441 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Mario Carneiro, 20-Mar-2013.) Avoid ax-13 2372. (Revised by Gino Giotto, 26-Jan-2024.) |
โข (โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โ ๐) | ||
Theorem | oprabid 7441 | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker oprabidw 7440 when possible. (Contributed by Mario Carneiro, 20-Mar-2013.) (New usage is discouraged.) |
โข (โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โ ๐) | ||
Theorem | ovex 7442 | The result of an operation is a set. (Contributed by NM, 13-Mar-1995.) |
โข (๐ด๐น๐ต) โ V | ||
Theorem | ovexi 7443 | The result of an operation is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข ๐ด = (๐ต๐น๐ถ) โ โข ๐ด โ V | ||
Theorem | ovexd 7444 | The result of an operation is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
โข (๐ โ (๐ด๐น๐ต) โ V) | ||
Theorem | ovssunirn 7445 | The result of an operation value is always a subset of the union of the range. (Contributed by Mario Carneiro, 12-Jan-2017.) |
โข (๐๐น๐) โ โช ran ๐น | ||
Theorem | 0ov 7446 | Operation value of the empty set. (Contributed by AV, 15-May-2021.) |
โข (๐ดโ ๐ต) = โ | ||
Theorem | ovprc 7447 | 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.) |
โข Rel dom ๐น โ โข (ยฌ (๐ด โ V โง ๐ต โ V) โ (๐ด๐น๐ต) = โ ) | ||
Theorem | ovprc1 7448 | The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.) |
โข Rel dom ๐น โ โข (ยฌ ๐ด โ V โ (๐ด๐น๐ต) = โ ) | ||
Theorem | ovprc2 7449 | The value of an operation when the second argument is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.) |
โข Rel dom ๐น โ โข (ยฌ ๐ต โ V โ (๐ด๐น๐ต) = โ ) | ||
Theorem | ovrcl 7450 | Reverse closure for an operation value. (Contributed by Mario Carneiro, 5-May-2015.) |
โข Rel dom ๐น โ โข (๐ถ โ (๐ด๐น๐ต) โ (๐ด โ V โง ๐ต โ V)) | ||
Theorem | csbov123 7451 | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Revised by NM, 23-Aug-2018.) |
โข โฆ๐ด / ๐ฅโฆ(๐ต๐น๐ถ) = (โฆ๐ด / ๐ฅโฆ๐ตโฆ๐ด / ๐ฅโฆ๐นโฆ๐ด / ๐ฅโฆ๐ถ) | ||
Theorem | csbov 7452* | Move class substitution in and out of an operation. (Contributed by NM, 23-Aug-2018.) |
โข โฆ๐ด / ๐ฅโฆ(๐ต๐น๐ถ) = (๐ตโฆ๐ด / ๐ฅโฆ๐น๐ถ) | ||
Theorem | csbov12g 7453* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
โข (๐ด โ ๐ โ โฆ๐ด / ๐ฅโฆ(๐ต๐น๐ถ) = (โฆ๐ด / ๐ฅโฆ๐ต๐นโฆ๐ด / ๐ฅโฆ๐ถ)) | ||
Theorem | csbov1g 7454* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
โข (๐ด โ ๐ โ โฆ๐ด / ๐ฅโฆ(๐ต๐น๐ถ) = (โฆ๐ด / ๐ฅโฆ๐ต๐น๐ถ)) | ||
Theorem | csbov2g 7455* | Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) |
โข (๐ด โ ๐ โ โฆ๐ด / ๐ฅโฆ(๐ต๐น๐ถ) = (๐ต๐นโฆ๐ด / ๐ฅโฆ๐ถ)) | ||
Theorem | rspceov 7456* | A frequently used special case of rspc2ev 3625 for operation values. (Contributed by NM, 21-Mar-2007.) |
โข ((๐ถ โ ๐ด โง ๐ท โ ๐ต โง ๐ = (๐ถ๐น๐ท)) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ = (๐ฅ๐น๐ฆ)) | ||
Theorem | elovimad 7457 | Elementhood of the image set of an operation value. (Contributed by Thierry Arnoux, 13-Mar-2017.) |
โข (๐ โ ๐ด โ ๐ถ) & โข (๐ โ ๐ต โ ๐ท) & โข (๐ โ Fun ๐น) & โข (๐ โ (๐ถ ร ๐ท) โ dom ๐น) โ โข (๐ โ (๐ด๐น๐ต) โ (๐น โ (๐ถ ร ๐ท))) | ||
Theorem | fnbrovb 7458 | Value of a binary operation expressed as a binary relation. See also fnbrfvb 6945 for functions on Cartesian products. (Contributed by BJ, 15-Feb-2022.) |
โข ((๐น Fn (๐ ร ๐) โง (๐ด โ ๐ โง ๐ต โ ๐)) โ ((๐ด๐น๐ต) = ๐ถ โ โจ๐ด, ๐ตโฉ๐น๐ถ)) | ||
Theorem | fnotovb 7459 | Equivalence of operation value and ordered triple membership, analogous to fnopfvb 6946. (Contributed by NM, 17-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) (Proof shortened by BJ, 15-Feb-2022.) |
โข ((๐น Fn (๐ด ร ๐ต) โง ๐ถ โ ๐ด โง ๐ท โ ๐ต) โ ((๐ถ๐น๐ท) = ๐ โ โจ๐ถ, ๐ท, ๐ โฉ โ ๐น)) | ||
Theorem | opabbrex 7460 | 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.) |
โข ((โ๐ฅโ๐ฆ(๐ฅ๐ ๐ฆ โ ๐) โง {โจ๐ฅ, ๐ฆโฉ โฃ ๐} โ ๐) โ {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ๐ ๐ฆ โง ๐)} โ V) | ||
Theorem | opabresex2 7461* | 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.) Add disjoint variable conditions betweem ๐, ๐บ and ๐ฅ, ๐ฆ to remove hypotheses. (Revised by SN, 13-Dec-2024.) |
โข {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ(๐โ๐บ)๐ฆ โง ๐)} โ V | ||
Theorem | opabresex2d 7462* | Obsolete version of opabresex2 7461 as of 13-Dec-2024. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 15-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ((๐ โง ๐ฅ(๐โ๐บ)๐ฆ) โ ๐) & โข (๐ โ {โจ๐ฅ, ๐ฆโฉ โฃ ๐} โ ๐) โ โข (๐ โ {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ(๐โ๐บ)๐ฆ โง ๐)} โ V) | ||
Theorem | fvmptopab 7463* | 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.) Add disjoint variable condition on ๐น, ๐ฅ, ๐ฆ to remove a sethood hypothesis. (Revised by SN, 13-Dec-2024.) |
โข (๐ง = ๐ โ (๐ โ ๐)) & โข ๐ = (๐ง โ V โฆ {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ(๐นโ๐ง)๐ฆ โง ๐)}) โ โข (๐โ๐) = {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ(๐นโ๐)๐ฆ โง ๐)} | ||
Theorem | fvmptopabOLD 7464* | Obsolete version of fvmptopab 7463 as of 13-Dec-2024. (Contributed by AV, 31-Jan-2021.) (Revised by AV, 29-Oct-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ((๐ โง ๐ง = ๐) โ (๐ โ ๐)) & โข (๐ โ {โจ๐ฅ, ๐ฆโฉ โฃ ๐ฅ(๐นโ๐)๐ฆ} โ V) & โข ๐ = (๐ง โ V โฆ {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ(๐นโ๐ง)๐ฆ โง ๐)}) โ โข (๐ โ (๐โ๐) = {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ(๐นโ๐)๐ฆ โง ๐)}) | ||
Theorem | f1opr 7465* | Condition for an operation to be one-to-one. (Contributed by Jeff Madsen, 17-Jun-2010.) |
โข (๐น:(๐ด ร ๐ต)โ1-1โ๐ถ โ (๐น:(๐ด ร ๐ต)โถ๐ถ โง โ๐ โ ๐ด โ๐ โ ๐ต โ๐ก โ ๐ด โ๐ข โ ๐ต ((๐๐น๐ ) = (๐ก๐น๐ข) โ (๐ = ๐ก โง ๐ = ๐ข)))) | ||
Theorem | brfvopab 7466 | 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.) |
โข (๐ โ V โ (๐นโ๐) = {โจ๐ฆ, ๐งโฉ โฃ ๐}) โ โข (๐ด(๐นโ๐)๐ต โ (๐ โ V โง ๐ด โ V โง ๐ต โ V)) | ||
Theorem | dfoprab2 7467* | Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.) |
โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจ๐ค, ๐งโฉ โฃ โ๐ฅโ๐ฆ(๐ค = โจ๐ฅ, ๐ฆโฉ โง ๐)} | ||
Theorem | reloprab 7468* | An operation class abstraction is a relation. (Contributed by NM, 16-Jun-2004.) |
โข Rel {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} | ||
Theorem | oprabv 7469* | If a pair and a class are in a relationship given by a class abstraction of a collection of nested ordered pairs, the involved classes are sets. (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
โข (โจ๐, ๐โฉ{โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐}๐ โ (๐ โ V โง ๐ โ V โง ๐ โ V)) | ||
Theorem | nfoprab1 7470 | The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
โข โฒ๐ฅ{โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} | ||
Theorem | nfoprab2 7471 | The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 30-Jul-2012.) |
โข โฒ๐ฆ{โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} | ||
Theorem | nfoprab3 7472 | The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.) |
โข โฒ๐ง{โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} | ||
Theorem | nfoprab 7473* | Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.) |
โข โฒ๐ค๐ โ โข โฒ๐ค{โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} | ||
Theorem | oprabbid 7474* | Equivalent wff's yield equal operation class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2014.) |
โข โฒ๐ฅ๐ & โข โฒ๐ฆ๐ & โข โฒ๐ง๐ & โข (๐ โ (๐ โ ๐)) โ โข (๐ โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐}) | ||
Theorem | oprabbidv 7475* | Equivalent wff's yield equal operation class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.) |
โข (๐ โ (๐ โ ๐)) โ โข (๐ โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐}) | ||
Theorem | oprabbii 7476* | Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.) |
โข (๐ โ ๐) โ โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} | ||
Theorem | ssoprab2 7477 | Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 5547. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
โข (โ๐ฅโ๐ฆโ๐ง(๐ โ ๐) โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐}) | ||
Theorem | ssoprab2b 7478 | Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 5550. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) (New usage is discouraged.) |
โข ({โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โ {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โ โ๐ฅโ๐ฆโ๐ง(๐ โ ๐)) | ||
Theorem | eqoprab2bw 7479* | Equivalence of ordered pair abstraction subclass and biconditional. Version of eqoprab2b 7480 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Mario Carneiro, 4-Jan-2017.) Avoid ax-13 2372. (Revised by Gino Giotto, 26-Jan-2024.) |
โข ({โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โ โ๐ฅโ๐ฆโ๐ง(๐ โ ๐)) | ||
Theorem | eqoprab2b 7480 | Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 5553. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker eqoprab2bw 7479 when possible. (Contributed by Mario Carneiro, 4-Jan-2017.) (New usage is discouraged.) |
โข ({โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} โ โ๐ฅโ๐ฆโ๐ง(๐ โ ๐)) | ||
Theorem | mpoeq123 7481* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.) |
โข ((๐ด = ๐ท โง โ๐ฅ โ ๐ด (๐ต = ๐ธ โง โ๐ฆ โ ๐ต ๐ถ = ๐น)) โ (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ฅ โ ๐ท, ๐ฆ โ ๐ธ โฆ ๐น)) | ||
Theorem | mpoeq12 7482* | An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
โข ((๐ด = ๐ถ โง ๐ต = ๐ท) โ (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ธ) = (๐ฅ โ ๐ถ, ๐ฆ โ ๐ท โฆ ๐ธ)) | ||
Theorem | mpoeq123dva 7483* | An equality deduction for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) |
โข (๐ โ ๐ด = ๐ท) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต = ๐ธ) & โข ((๐ โง (๐ฅ โ ๐ด โง ๐ฆ โ ๐ต)) โ ๐ถ = ๐น) โ โข (๐ โ (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ฅ โ ๐ท, ๐ฆ โ ๐ธ โฆ ๐น)) | ||
Theorem | mpoeq123dv 7484* | An equality deduction for the maps-to notation. (Contributed by NM, 12-Sep-2011.) |
โข (๐ โ ๐ด = ๐ท) & โข (๐ โ ๐ต = ๐ธ) & โข (๐ โ ๐ถ = ๐น) โ โข (๐ โ (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ฅ โ ๐ท, ๐ฆ โ ๐ธ โฆ ๐น)) | ||
Theorem | mpoeq123i 7485 | An equality inference for the maps-to notation. (Contributed by NM, 15-Jul-2013.) |
โข ๐ด = ๐ท & โข ๐ต = ๐ธ & โข ๐ถ = ๐น โ โข (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ฅ โ ๐ท, ๐ฆ โ ๐ธ โฆ ๐น) | ||
Theorem | mpoeq3dva 7486* | Slightly more general equality inference for the maps-to notation. (Contributed by NM, 17-Oct-2013.) |
โข ((๐ โง ๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โ ๐ถ = ๐ท) โ โข (๐ โ (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ท)) | ||
Theorem | mpoeq3ia 7487 | An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |
โข ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โ ๐ถ = ๐ท) โ โข (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ท) | ||
Theorem | mpoeq3dv 7488* | An equality deduction for the maps-to notation restricted to the value of the operation. (Contributed by SO, 16-Jul-2018.) |
โข (๐ โ ๐ถ = ๐ท) โ โข (๐ โ (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ท)) | ||
Theorem | nfmpo1 7489 | Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.) |
โข โฒ๐ฅ(๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) | ||
Theorem | nfmpo2 7490 | Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.) |
โข โฒ๐ฆ(๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) | ||
Theorem | nfmpo 7491* | Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.) |
โข โฒ๐ง๐ด & โข โฒ๐ง๐ต & โข โฒ๐ง๐ถ โ โข โฒ๐ง(๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) | ||
Theorem | 0mpo0 7492* | A mapping operation with empty domain is empty. Generalization of mpo0 7494. (Contributed by AV, 27-Jan-2024.) |
โข ((๐ด = โ โจ ๐ต = โ ) โ (๐ฅ โ ๐ด, ๐ฆ โ ๐ต โฆ ๐ถ) = โ ) | ||
Theorem | mpo0v 7493* | A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.) (Proof shortened by AV, 27-Jan-2024.) |
โข (๐ฅ โ โ , ๐ฆ โ ๐ต โฆ ๐ถ) = โ | ||
Theorem | mpo0 7494 | A mapping operation with empty domain. In this version of mpo0v 7493, the class of the second operator may depend on the first operator. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.) |
โข (๐ฅ โ โ , ๐ฆ โ ๐ต โฆ ๐ถ) = โ | ||
Theorem | oprab4 7495* | Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.) |
โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ (โจ๐ฅ, ๐ฆโฉ โ (๐ด ร ๐ต) โง ๐)} = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โง ๐)} | ||
Theorem | cbvoprab1 7496* | Rule used to change first bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 20-Dec-2008.) (Revised by Mario Carneiro, 5-Dec-2016.) |
โข โฒ๐ค๐ & โข โฒ๐ฅ๐ & โข (๐ฅ = ๐ค โ (๐ โ ๐)) โ โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ค, ๐ฆโฉ, ๐งโฉ โฃ ๐} | ||
Theorem | cbvoprab2 7497* | Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 11-Dec-2016.) |
โข โฒ๐ค๐ & โข โฒ๐ฆ๐ & โข (๐ฆ = ๐ค โ (๐ โ ๐)) โ โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ฅ, ๐คโฉ, ๐งโฉ โฃ ๐} | ||
Theorem | cbvoprab12 7498* | Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
โข โฒ๐ค๐ & โข โฒ๐ฃ๐ & โข โฒ๐ฅ๐ & โข โฒ๐ฆ๐ & โข ((๐ฅ = ๐ค โง ๐ฆ = ๐ฃ) โ (๐ โ ๐)) โ โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ค, ๐ฃโฉ, ๐งโฉ โฃ ๐} | ||
Theorem | cbvoprab12v 7499* | Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.) |
โข ((๐ฅ = ๐ค โง ๐ฆ = ๐ฃ) โ (๐ โ ๐)) โ โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ค, ๐ฃโฉ, ๐งโฉ โฃ ๐} | ||
Theorem | cbvoprab3 7500* | Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.) |
โข โฒ๐ค๐ & โข โฒ๐ง๐ & โข (๐ง = ๐ค โ (๐ โ ๐)) โ โข {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ๐} = {โจโจ๐ฅ, ๐ฆโฉ, ๐คโฉ โฃ ๐} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |