Home | Metamath
Proof Explorer Theorem List (p. 80 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | oprabex3 7901* | Existence of an operation class abstraction (special case). (Contributed by NM, 19-Oct-2004.) |
ā¢ š» ā V & ā¢ š¹ = {āØāØš„, š¦ā©, š§ā© ā£ ((š„ ā (š» Ć š») ā§ š¦ ā (š» Ć š»)) ā§ āš¤āš£āš¢āš((š„ = āØš¤, š£ā© ā§ š¦ = āØš¢, šā©) ā§ š§ = š ))} ā ā¢ š¹ ā V | ||
Theorem | oprabrexex2 7902* | Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) |
ā¢ š“ ā V & ā¢ {āØāØš„, š¦ā©, š§ā© ā£ š} ā V ā ā¢ {āØāØš„, š¦ā©, š§ā© ā£ āš¤ ā š“ š} ā V | ||
Theorem | ab2rexex 7903* | Existence of a class abstraction of existentially restricted sets. Variables š„ and š¦ are normally free-variable parameters in the class expression substituted for š¶, which can be thought of as š¶(š„, š¦). See comments for abrexex 7886. (Contributed by NM, 20-Sep-2011.) |
ā¢ š“ ā V & ā¢ šµ ā V ā ā¢ {š§ ā£ āš„ ā š“ āš¦ ā šµ š§ = š¶} ā V | ||
Theorem | ab2rexex2 7904* | Existence of an existentially restricted class abstraction. š normally has free-variable parameters š„, š¦, and š§. Compare abrexex2 7893. (Contributed by NM, 20-Sep-2011.) |
ā¢ š“ ā V & ā¢ šµ ā V & ā¢ {š§ ā£ š} ā V ā ā¢ {š§ ā£ āš„ ā š“ āš¦ ā šµ š} ā V | ||
Theorem | xpexgALT 7905 | Alternate proof of xpexg 7675 requiring Replacement (ax-rep 5241) but not Power Set (ax-pow 5319). (Contributed by Mario Carneiro, 20-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
ā¢ ((š“ ā š ā§ šµ ā š) ā (š“ Ć šµ) ā V) | ||
Theorem | offval3 7906* | General value of (š¹ āf š šŗ) with no assumptions on functionality of š¹ and šŗ. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
ā¢ ((š¹ ā š ā§ šŗ ā š) ā (š¹ āf š šŗ) = (š„ ā (dom š¹ ā© dom šŗ) ā¦ ((š¹āš„)š (šŗāš„)))) | ||
Theorem | offres 7907 | Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
ā¢ ((š¹ ā š ā§ šŗ ā š) ā ((š¹ āf š šŗ) ā¾ š·) = ((š¹ ā¾ š·) āf š (šŗ ā¾ š·))) | ||
Theorem | ofmres 7908* | Equivalent expressions for a restriction of the function operation map. Unlike āf š which is a proper class, ( āf š ā¾ (š“ Ć šµ)) can be a set by ofmresex 7909, allowing it to be used as a function or structure argument. By ofmresval 7624, the restricted operation map values are the same as the original values, allowing theorems for āf š to be reused. (Contributed by NM, 20-Oct-2014.) |
ā¢ ( āf š ā¾ (š“ Ć šµ)) = (š ā š“, š ā šµ ā¦ (š āf š š)) | ||
Theorem | ofmresex 7909 | Existence of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.) |
ā¢ (š ā š“ ā š) & ā¢ (š ā šµ ā š) ā ā¢ (š ā ( āf š ā¾ (š“ Ć šµ)) ā V) | ||
Syntax | c1st 7910 | Extend the definition of a class to include the first member an ordered pair function. |
class 1st | ||
Syntax | c2nd 7911 | Extend the definition of a class to include the second member an ordered pair function. |
class 2nd | ||
Definition | df-1st 7912 | Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 7920 proves that it does this. For example, (1st āāØ3, 4ā©) = 3. Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 6174 and op1stb 5427). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.) |
ā¢ 1st = (š„ ā V ā¦ āŖ dom {š„}) | ||
Definition | df-2nd 7913 | Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 7921 proves that it does this. For example, (2nd āāØ3, 4ā©) = 4. Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 6177 and op2ndb 6176). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.) |
ā¢ 2nd = (š„ ā V ā¦ āŖ ran {š„}) | ||
Theorem | 1stval 7914 | The value of the function that extracts the first member of an ordered pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
ā¢ (1st āš“) = āŖ dom {š“} | ||
Theorem | 2ndval 7915 | The value of the function that extracts the second member of an ordered pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
ā¢ (2nd āš“) = āŖ ran {š“} | ||
Theorem | 1stnpr 7916 | Value of the first-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
ā¢ (Ā¬ š“ ā (V Ć V) ā (1st āš“) = ā ) | ||
Theorem | 2ndnpr 7917 | Value of the second-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
ā¢ (Ā¬ š“ ā (V Ć V) ā (2nd āš“) = ā ) | ||
Theorem | 1st0 7918 | The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.) |
ā¢ (1st āā ) = ā | ||
Theorem | 2nd0 7919 | The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.) |
ā¢ (2nd āā ) = ā | ||
Theorem | op1st 7920 | Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
ā¢ š“ ā V & ā¢ šµ ā V ā ā¢ (1st āāØš“, šµā©) = š“ | ||
Theorem | op2nd 7921 | Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
ā¢ š“ ā V & ā¢ šµ ā V ā ā¢ (2nd āāØš“, šµā©) = šµ | ||
Theorem | op1std 7922 | Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
ā¢ š“ ā V & ā¢ šµ ā V ā ā¢ (š¶ = āØš“, šµā© ā (1st āš¶) = š“) | ||
Theorem | op2ndd 7923 | Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
ā¢ š“ ā V & ā¢ šµ ā V ā ā¢ (š¶ = āØš“, šµā© ā (2nd āš¶) = šµ) | ||
Theorem | op1stg 7924 | Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
ā¢ ((š“ ā š ā§ šµ ā š) ā (1st āāØš“, šµā©) = š“) | ||
Theorem | op2ndg 7925 | Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
ā¢ ((š“ ā š ā§ šµ ā š) ā (2nd āāØš“, šµā©) = šµ) | ||
Theorem | ot1stg 7926 | Extract the first member of an ordered triple. (Due to infrequent usage, it isn't worthwhile at this point to define special extractors for triples, so we reuse the ordered pair extractors for ot1stg 7926, ot2ndg 7927, ot3rdg 7928.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
ā¢ ((š“ ā š ā§ šµ ā š ā§ š¶ ā š) ā (1st ā(1st āāØš“, šµ, š¶ā©)) = š“) | ||
Theorem | ot2ndg 7927 | Extract the second member of an ordered triple. (See ot1stg 7926 comment.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
ā¢ ((š“ ā š ā§ šµ ā š ā§ š¶ ā š) ā (2nd ā(1st āāØš“, šµ, š¶ā©)) = šµ) | ||
Theorem | ot3rdg 7928 | Extract the third member of an ordered triple. (See ot1stg 7926 comment.) (Contributed by NM, 3-Apr-2015.) |
ā¢ (š¶ ā š ā (2nd āāØš“, šµ, š¶ā©) = š¶) | ||
Theorem | 1stval2 7929 | Alternate value of the function that extracts the first member of an ordered pair. Definition 5.13 (i) of [Monk1] p. 52. (Contributed by NM, 18-Aug-2006.) |
ā¢ (š“ ā (V Ć V) ā (1st āš“) = ā© ā© š“) | ||
Theorem | 2ndval2 7930 | Alternate value of the function that extracts the second member of an ordered pair. Definition 5.13 (ii) of [Monk1] p. 52. (Contributed by NM, 18-Aug-2006.) |
ā¢ (š“ ā (V Ć V) ā (2nd āš“) = ā© ā© ā© ā”{š“}) | ||
Theorem | oteqimp 7931 | The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
ā¢ (š = āØš“, šµ, š¶ā© ā ((š“ ā š ā§ šµ ā š ā§ š¶ ā š) ā ((1st ā(1st āš)) = š“ ā§ (2nd ā(1st āš)) = šµ ā§ (2nd āš) = š¶))) | ||
Theorem | fo1st 7932 | The 1st function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
ā¢ 1st :VāontoāV | ||
Theorem | fo2nd 7933 | The 2nd function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
ā¢ 2nd :VāontoāV | ||
Theorem | br1steqg 7934 | Uniqueness condition for the binary relation 1st. (Contributed by Scott Fenton, 2-Jul-2020.) Revised to remove sethood hypothesis on š¶. (Revised by Peter Mazsa, 17-Jan-2022.) |
ā¢ ((š“ ā š ā§ šµ ā š) ā (āØš“, šµā©1st š¶ ā š¶ = š“)) | ||
Theorem | br2ndeqg 7935 | Uniqueness condition for the binary relation 2nd. (Contributed by Scott Fenton, 2-Jul-2020.) Revised to remove sethood hypothesis on š¶. (Revised by Peter Mazsa, 17-Jan-2022.) |
ā¢ ((š“ ā š ā§ šµ ā š) ā (āØš“, šµā©2nd š¶ ā š¶ = šµ)) | ||
Theorem | f1stres 7936 | Mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 11-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
ā¢ (1st ā¾ (š“ Ć šµ)):(š“ Ć šµ)ā¶š“ | ||
Theorem | f2ndres 7937 | Mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 7-Aug-2006.) (Revised by Mario Carneiro, 8-Sep-2013.) |
ā¢ (2nd ā¾ (š“ Ć šµ)):(š“ Ć šµ)ā¶šµ | ||
Theorem | fo1stres 7938 | Onto mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 14-Dec-2008.) |
ā¢ (šµ ā ā ā (1st ā¾ (š“ Ć šµ)):(š“ Ć šµ)āontoāš“) | ||
Theorem | fo2ndres 7939 | Onto mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 14-Dec-2008.) |
ā¢ (š“ ā ā ā (2nd ā¾ (š“ Ć šµ)):(š“ Ć šµ)āontoāšµ) | ||
Theorem | 1st2val 7940* | Value of an alternate definition of the 1st function. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 30-Dec-2014.) |
ā¢ ({āØāØš„, š¦ā©, š§ā© ā£ š§ = š„}āš“) = (1st āš“) | ||
Theorem | 2nd2val 7941* | Value of an alternate definition of the 2nd function. (Contributed by NM, 10-Aug-2006.) (Revised by Mario Carneiro, 30-Dec-2014.) |
ā¢ ({āØāØš„, š¦ā©, š§ā© ā£ š§ = š¦}āš“) = (2nd āš“) | ||
Theorem | 1stcof 7942 | Composition of the first member function with another function. (Contributed by NM, 12-Oct-2007.) |
ā¢ (š¹:š“ā¶(šµ Ć š¶) ā (1st ā š¹):š“ā¶šµ) | ||
Theorem | 2ndcof 7943 | Composition of the second member function with another function. (Contributed by FL, 15-Oct-2012.) |
ā¢ (š¹:š“ā¶(šµ Ć š¶) ā (2nd ā š¹):š“ā¶š¶) | ||
Theorem | xp1st 7944 | Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
ā¢ (š“ ā (šµ Ć š¶) ā (1st āš“) ā šµ) | ||
Theorem | xp2nd 7945 | Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
ā¢ (š“ ā (šµ Ć š¶) ā (2nd āš“) ā š¶) | ||
Theorem | elxp6 7946 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7850. (Contributed by NM, 9-Oct-2004.) |
ā¢ (š“ ā (šµ Ć š¶) ā (š“ = āØ(1st āš“), (2nd āš“)ā© ā§ ((1st āš“) ā šµ ā§ (2nd āš“) ā š¶))) | ||
Theorem | elxp7 7947 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7850. (Contributed by NM, 19-Aug-2006.) |
ā¢ (š“ ā (šµ Ć š¶) ā (š“ ā (V Ć V) ā§ ((1st āš“) ā šµ ā§ (2nd āš“) ā š¶))) | ||
Theorem | eqopi 7948 | Equality with an ordered pair. (Contributed by NM, 15-Dec-2008.) (Revised by Mario Carneiro, 23-Feb-2014.) |
ā¢ ((š“ ā (š Ć š) ā§ ((1st āš“) = šµ ā§ (2nd āš“) = š¶)) ā š“ = āØšµ, š¶ā©) | ||
Theorem | xp2 7949* | Representation of Cartesian product based on ordered pair component functions. (Contributed by NM, 16-Sep-2006.) |
ā¢ (š“ Ć šµ) = {š„ ā (V Ć V) ā£ ((1st āš„) ā š“ ā§ (2nd āš„) ā šµ)} | ||
Theorem | unielxp 7950 | The membership relation for a Cartesian product is inherited by union. (Contributed by NM, 16-Sep-2006.) |
ā¢ (š“ ā (šµ Ć š¶) ā āŖ š“ ā āŖ (šµ Ć š¶)) | ||
Theorem | 1st2nd2 7951 | Reconstruction of a member of a Cartesian product in terms of its ordered pair components. (Contributed by NM, 20-Oct-2013.) |
ā¢ (š“ ā (šµ Ć š¶) ā š“ = āØ(1st āš“), (2nd āš“)ā©) | ||
Theorem | 1st2ndb 7952 | Reconstruction of an ordered pair in terms of its components. (Contributed by NM, 25-Feb-2014.) |
ā¢ (š“ ā (V Ć V) ā š“ = āØ(1st āš“), (2nd āš“)ā©) | ||
Theorem | xpopth 7953 | An ordered pair theorem for members of Cartesian products. (Contributed by NM, 20-Jun-2007.) |
ā¢ ((š“ ā (š¶ Ć š·) ā§ šµ ā (š Ć š)) ā (((1st āš“) = (1st āšµ) ā§ (2nd āš“) = (2nd āšµ)) ā š“ = šµ)) | ||
Theorem | eqop 7954 | Two ways to express equality with an ordered pair. (Contributed by NM, 3-Sep-2007.) (Proof shortened by Mario Carneiro, 26-Apr-2015.) |
ā¢ (š“ ā (š Ć š) ā (š“ = āØšµ, š¶ā© ā ((1st āš“) = šµ ā§ (2nd āš“) = š¶))) | ||
Theorem | eqop2 7955 | Two ways to express equality with an ordered pair. (Contributed by NM, 25-Feb-2014.) |
ā¢ šµ ā V & ā¢ š¶ ā V ā ā¢ (š“ = āØšµ, š¶ā© ā (š“ ā (V Ć V) ā§ ((1st āš“) = šµ ā§ (2nd āš“) = š¶))) | ||
Theorem | op1steq 7956* | Two ways of expressing that an element is the first member of an ordered pair. (Contributed by NM, 22-Sep-2013.) (Revised by Mario Carneiro, 23-Feb-2014.) |
ā¢ (š“ ā (š Ć š) ā ((1st āš“) = šµ ā āš„ š“ = āØšµ, š„ā©)) | ||
Theorem | opreuopreu 7957* | There is a unique ordered pair fulfilling a wff iff its components fulfil a corresponding wff. (Contributed by AV, 2-Jul-2023.) |
ā¢ ((š = (1st āš) ā§ š = (2nd āš)) ā (š ā š)) ā ā¢ (ā!š ā (š“ Ć šµ)š ā ā!š ā (š“ Ć šµ)āšāš(š = āØš, šā© ā§ š)) | ||
Theorem | el2xptp 7958* | A member of a nested Cartesian product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
ā¢ (š“ ā ((šµ Ć š¶) Ć š·) ā āš„ ā šµ āš¦ ā š¶ āš§ ā š· š“ = āØš„, š¦, š§ā©) | ||
Theorem | el2xptp0 7959 | A member of a nested Cartesian product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
ā¢ ((š ā š ā§ š ā š ā§ š ā š) ā ((š“ ā ((š Ć š) Ć š) ā§ ((1st ā(1st āš“)) = š ā§ (2nd ā(1st āš“)) = š ā§ (2nd āš“) = š)) ā š“ = āØš, š, šā©)) | ||
Theorem | 2nd1st 7960 | Swap the members of an ordered pair. (Contributed by NM, 31-Dec-2014.) |
ā¢ (š“ ā (šµ Ć š¶) ā āŖ ā”{š“} = āØ(2nd āš“), (1st āš“)ā©) | ||
Theorem | 1st2nd 7961 | Reconstruction of a member of a relation in terms of its ordered pair components. (Contributed by NM, 29-Aug-2006.) |
ā¢ ((Rel šµ ā§ š“ ā šµ) ā š“ = āØ(1st āš“), (2nd āš“)ā©) | ||
Theorem | 1stdm 7962 | The first ordered pair component of a member of a relation belongs to the domain of the relation. (Contributed by NM, 17-Sep-2006.) |
ā¢ ((Rel š ā§ š“ ā š ) ā (1st āš“) ā dom š ) | ||
Theorem | 2ndrn 7963 | The second ordered pair component of a member of a relation belongs to the range of the relation. (Contributed by NM, 17-Sep-2006.) |
ā¢ ((Rel š ā§ š“ ā š ) ā (2nd āš“) ā ran š ) | ||
Theorem | 1st2ndbr 7964 | Express an element of a relation as a relationship between first and second components. (Contributed by Mario Carneiro, 22-Jun-2016.) |
ā¢ ((Rel šµ ā§ š“ ā šµ) ā (1st āš“)šµ(2nd āš“)) | ||
Theorem | releldm2 7965* | Two ways of expressing membership in the domain of a relation. (Contributed by NM, 22-Sep-2013.) |
ā¢ (Rel š“ ā (šµ ā dom š“ ā āš„ ā š“ (1st āš„) = šµ)) | ||
Theorem | reldm 7966* | An expression for the domain of a relation. (Contributed by NM, 22-Sep-2013.) |
ā¢ (Rel š“ ā dom š“ = ran (š„ ā š“ ā¦ (1st āš„))) | ||
Theorem | releldmdifi 7967* | One way of expressing membership in the difference of domains of two nested relations. (Contributed by AV, 26-Oct-2023.) |
ā¢ ((Rel š“ ā§ šµ ā š“) ā (š¶ ā (dom š“ ā dom šµ) ā āš„ ā (š“ ā šµ)(1st āš„) = š¶)) | ||
Theorem | funfv1st2nd 7968 | The function value for the first component of an ordered pair is the second component of the ordered pair. (Contributed by AV, 17-Oct-2023.) |
ā¢ ((Fun š¹ ā§ š ā š¹) ā (š¹ā(1st āš)) = (2nd āš)) | ||
Theorem | funelss 7969 | If the first component of an element of a function is in the domain of a subset of the function, the element is a member of this subset. (Contributed by AV, 27-Oct-2023.) |
ā¢ ((Fun š“ ā§ šµ ā š“ ā§ š ā š“) ā ((1st āš) ā dom šµ ā š ā šµ)) | ||
Theorem | funeldmdif 7970* | Two ways of expressing membership in the difference of domains of two nested functions. (Contributed by AV, 27-Oct-2023.) |
ā¢ ((Fun š“ ā§ šµ ā š“) ā (š¶ ā (dom š“ ā dom šµ) ā āš„ ā (š“ ā šµ)(1st āš„) = š¶)) | ||
Theorem | sbcopeq1a 7971 | Equality theorem for substitution of a class for an ordered pair (analogue of sbceq1a 3749 that avoids the existential quantifiers of copsexg 5446). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
ā¢ (š“ = āØš„, š¦ā© ā ([(1st āš“) / š„][(2nd āš“) / š¦]š ā š)) | ||
Theorem | csbopeq1a 7972 | Equality theorem for substitution of a class š“ for an ordered pair āØš„, š¦ā© in šµ (analogue of csbeq1a 3868). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
ā¢ (š“ = āØš„, š¦ā© ā ā¦(1st āš“) / š„ā¦ā¦(2nd āš“) / š¦ā¦šµ = šµ) | ||
Theorem | dfopab2 7973* | A way to define an ordered-pair class abstraction without using existential quantifiers. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
ā¢ {āØš„, š¦ā© ā£ š} = {š§ ā (V Ć V) ā£ [(1st āš§) / š„][(2nd āš§) / š¦]š} | ||
Theorem | dfoprab3s 7974* | A way to define an operation class abstraction without using existential quantifiers. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
ā¢ {āØāØš„, š¦ā©, š§ā© ā£ š} = {āØš¤, š§ā© ā£ (š¤ ā (V Ć V) ā§ [(1st āš¤) / š„][(2nd āš¤) / š¦]š)} | ||
Theorem | dfoprab3 7975* | Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008.) |
ā¢ (š¤ = āØš„, š¦ā© ā (š ā š)) ā ā¢ {āØš¤, š§ā© ā£ (š¤ ā (V Ć V) ā§ š)} = {āØāØš„, š¦ā©, š§ā© ā£ š} | ||
Theorem | dfoprab4 7976* | Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
ā¢ (š¤ = āØš„, š¦ā© ā (š ā š)) ā ā¢ {āØš¤, š§ā© ā£ (š¤ ā (š“ Ć šµ) ā§ š)} = {āØāØš„, š¦ā©, š§ā© ā£ ((š„ ā š“ ā§ š¦ ā šµ) ā§ š)} | ||
Theorem | dfoprab4f 7977* | Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 20-Dec-2008.) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 31-Aug-2015.) |
ā¢ ā²š„š & ā¢ ā²š¦š & ā¢ (š¤ = āØš„, š¦ā© ā (š ā š)) ā ā¢ {āØš¤, š§ā© ā£ (š¤ ā (š“ Ć šµ) ā§ š)} = {āØāØš„, š¦ā©, š§ā© ā£ ((š„ ā š“ ā§ š¦ ā šµ) ā§ š)} | ||
Theorem | opabex2 7978* | Condition for an operation to be a set. (Contributed by Thierry Arnoux, 25-Jun-2019.) |
ā¢ (š ā š“ ā š) & ā¢ (š ā šµ ā š) & ā¢ ((š ā§ š) ā š„ ā š“) & ā¢ ((š ā§ š) ā š¦ ā šµ) ā ā¢ (š ā {āØš„, š¦ā© ā£ š} ā V) | ||
Theorem | opabn1stprc 7979* | An ordered-pair class abstraction which does not depend on the first abstraction variable is a proper class. There must be, however, at least one set which satisfies the restricting wff. (Contributed by AV, 27-Dec-2020.) |
ā¢ (āš¦š ā {āØš„, š¦ā© ā£ š} ā V) | ||
Theorem | opiota 7980* | The property of a uniquely specified ordered pair. The proof uses properties of the ā© description binder. (Contributed by Mario Carneiro, 21-May-2015.) |
ā¢ š¼ = (ā©š§āš„ ā š“ āš¦ ā šµ (š§ = āØš„, š¦ā© ā§ š)) & ā¢ š = (1st āš¼) & ā¢ š = (2nd āš¼) & ā¢ (š„ = š¶ ā (š ā š)) & ā¢ (š¦ = š· ā (š ā š)) ā ā¢ (ā!š§āš„ ā š“ āš¦ ā šµ (š§ = āØš„, š¦ā© ā§ š) ā ((š¶ ā š“ ā§ š· ā šµ ā§ š) ā (š¶ = š ā§ š· = š))) | ||
Theorem | cnvoprab 7981* | The converse of a class abstraction of nested ordered pairs. (Contributed by Thierry Arnoux, 17-Aug-2017.) (Proof shortened by Thierry Arnoux, 20-Feb-2022.) |
ā¢ (š = āØš„, š¦ā© ā (š ā š)) & ā¢ (š ā š ā (V Ć V)) ā ā¢ ā”{āØāØš„, š¦ā©, š§ā© ā£ š} = {āØš§, šā© ā£ š} | ||
Theorem | dfxp3 7982* | Define the Cartesian product of three classes. Compare df-xp 5637. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 3-Nov-2015.) |
ā¢ ((š“ Ć šµ) Ć š¶) = {āØāØš„, š¦ā©, š§ā© ā£ (š„ ā š“ ā§ š¦ ā šµ ā§ š§ ā š¶)} | ||
Theorem | elopabi 7983* | A consequence of membership in an ordered-pair class abstraction, using ordered pair extractors. (Contributed by NM, 29-Aug-2006.) |
ā¢ (š„ = (1st āš“) ā (š ā š)) & ā¢ (š¦ = (2nd āš“) ā (š ā š)) ā ā¢ (š“ ā {āØš„, š¦ā© ā£ š} ā š) | ||
Theorem | eloprabi 7984* | A consequence of membership in an operation class abstraction, using ordered pair extractors. (Contributed by NM, 6-Nov-2006.) (Revised by David Abernethy, 19-Jun-2012.) |
ā¢ (š„ = (1st ā(1st āš“)) ā (š ā š)) & ā¢ (š¦ = (2nd ā(1st āš“)) ā (š ā š)) & ā¢ (š§ = (2nd āš“) ā (š ā š)) ā ā¢ (š“ ā {āØāØš„, š¦ā©, š§ā© ā£ š} ā š) | ||
Theorem | mpomptsx 7985* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016.) |
ā¢ (š„ ā š“, š¦ ā šµ ā¦ š¶) = (š§ ā āŖ š„ ā š“ ({š„} Ć šµ) ā¦ ā¦(1st āš§) / š„ā¦ā¦(2nd āš§) / š¦ā¦š¶) | ||
Theorem | mpompts 7986* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Sep-2015.) |
ā¢ (š„ ā š“, š¦ ā šµ ā¦ š¶) = (š§ ā (š“ Ć šµ) ā¦ ā¦(1st āš§) / š„ā¦ā¦(2nd āš§) / š¦ā¦š¶) | ||
Theorem | dmmpossx 7987* | The domain of a mapping is a subset of its base class. (Contributed by Mario Carneiro, 9-Feb-2015.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ dom š¹ ā āŖ š„ ā š“ ({š„} Ć šµ) | ||
Theorem | fmpox 7988* | Functionality, domain and codomain of a class given by the maps-to notation, where šµ(š„) is not constant but depends on š„. (Contributed by NM, 29-Dec-2014.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ (āš„ ā š“ āš¦ ā šµ š¶ ā š· ā š¹:āŖ š„ ā š“ ({š„} Ć šµ)ā¶š·) | ||
Theorem | fmpo 7989* | Functionality, domain and range of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ (āš„ ā š“ āš¦ ā šµ š¶ ā š· ā š¹:(š“ Ć šµ)ā¶š·) | ||
Theorem | fnmpo 7990* | Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ (āš„ ā š“ āš¦ ā šµ š¶ ā š ā š¹ Fn (š“ Ć šµ)) | ||
Theorem | fnmpoi 7991* | Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) & ā¢ š¶ ā V ā ā¢ š¹ Fn (š“ Ć šµ) | ||
Theorem | dmmpo 7992* | Domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) & ā¢ š¶ ā V ā ā¢ dom š¹ = (š“ Ć šµ) | ||
Theorem | ovmpoelrn 7993* | An operation's value belongs to its range. (Contributed by AV, 27-Jan-2020.) |
ā¢ š = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ ((āš„ ā š“ āš¦ ā šµ š¶ ā š ā§ š ā š“ ā§ š ā šµ) ā (ššš) ā š) | ||
Theorem | dmmpoga 7994* | Domain of an operation given by the maps-to notation, closed form of dmmpo 7992. (Contributed by Alexander van der Vekens, 10-Feb-2019.) (Proof shortened by Lammen, 29-May-2024.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ (āš„ ā š“ āš¦ ā šµ š¶ ā š ā dom š¹ = (š“ Ć šµ)) | ||
Theorem | dmmpogaOLD 7995* | Obsolete version of dmmpoga 7994 as of 29-May-2024. (Contributed by Alexander van der Vekens, 10-Feb-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ (āš„ ā š“ āš¦ ā šµ š¶ ā š ā dom š¹ = (š“ Ć šµ)) | ||
Theorem | dmmpog 7996* | Domain of an operation given by the maps-to notation, closed form of dmmpo 7992. Caution: This theorem is only valid in the very special case where the value of the mapping is a constant! (Contributed by Alexander van der Vekens, 1-Jun-2017.) (Proof shortened by AV, 10-Feb-2019.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ (š¶ ā š ā dom š¹ = (š“ Ć šµ)) | ||
Theorem | mpoexxg 7997* | Existence of an operation class abstraction (version for dependent domains). (Contributed by Mario Carneiro, 30-Dec-2016.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ ((š“ ā š ā§ āš„ ā š“ šµ ā š) ā š¹ ā V) | ||
Theorem | mpoexg 7998* | Existence of an operation class abstraction (special case). (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 1-Sep-2015.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ ((š“ ā š ā§ šµ ā š) ā š¹ ā V) | ||
Theorem | mpoexga 7999* | If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by NM, 12-Sep-2011.) |
ā¢ ((š“ ā š ā§ šµ ā š) ā (š„ ā š“, š¦ ā šµ ā¦ š¶) ā V) | ||
Theorem | mpoexw 8000* | Weak version of mpoex 8001 that holds without ax-rep 5241. If the domain and codomain of an operation given by maps-to notation are sets, the operation is a set. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
ā¢ š“ ā V & ā¢ šµ ā V & ā¢ š· ā V & ā¢ āš„ ā š“ āš¦ ā šµ š¶ ā š· ā ā¢ (š„ ā š“, š¦ ā šµ ā¦ š¶) ā V |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |