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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | oprabrexex2 7901* | Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) |
ā¢ š“ ā V & ā¢ {āØāØš„, š¦ā©, š§ā© ā£ š} ā V ā ā¢ {āØāØš„, š¦ā©, š§ā© ā£ āš¤ ā š“ š} ā V | ||
Theorem | ab2rexex 7902* | 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 7885. (Contributed by NM, 20-Sep-2011.) |
ā¢ š“ ā V & ā¢ šµ ā V ā ā¢ {š§ ā£ āš„ ā š“ āš¦ ā šµ š§ = š¶} ā V | ||
Theorem | ab2rexex2 7903* | Existence of an existentially restricted class abstraction. š normally has free-variable parameters š„, š¦, and š§. Compare abrexex2 7892. (Contributed by NM, 20-Sep-2011.) |
ā¢ š“ ā V & ā¢ šµ ā V & ā¢ {š§ ā£ š} ā V ā ā¢ {š§ ā£ āš„ ā š“ āš¦ ā šµ š} ā V | ||
Theorem | xpexgALT 7904 | Alternate proof of xpexg 7674 requiring Replacement (ax-rep 5240) but not Power Set (ax-pow 5318). (Contributed by Mario Carneiro, 20-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
ā¢ ((š“ ā š ā§ šµ ā š) ā (š“ Ć šµ) ā V) | ||
Theorem | offval3 7905* | General value of (š¹ āf š šŗ) with no assumptions on functionality of š¹ and šŗ. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
ā¢ ((š¹ ā š ā§ šŗ ā š) ā (š¹ āf š šŗ) = (š„ ā (dom š¹ ā© dom šŗ) ā¦ ((š¹āš„)š (šŗāš„)))) | ||
Theorem | offres 7906 | Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
ā¢ ((š¹ ā š ā§ šŗ ā š) ā ((š¹ āf š šŗ) ā¾ š·) = ((š¹ ā¾ š·) āf š (šŗ ā¾ š·))) | ||
Theorem | ofmres 7907* | Equivalent expressions for a restriction of the function operation map. Unlike āf š which is a proper class, ( āf š ā¾ (š“ Ć šµ)) can be a set by ofmresex 7908, allowing it to be used as a function or structure argument. By ofmresval 7623, 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 7908 | Existence of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.) |
ā¢ (š ā š“ ā š) & ā¢ (š ā šµ ā š) ā ā¢ (š ā ( āf š ā¾ (š“ Ć šµ)) ā V) | ||
Syntax | c1st 7909 | Extend the definition of a class to include the first member an ordered pair function. |
class 1st | ||
Syntax | c2nd 7910 | Extend the definition of a class to include the second member an ordered pair function. |
class 2nd | ||
Definition | df-1st 7911 | Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 7919 proves that it does this. For example, (1st āāØ3, 4ā©) = 3. Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 6173 and op1stb 5426). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.) |
ā¢ 1st = (š„ ā V ā¦ āŖ dom {š„}) | ||
Definition | df-2nd 7912 | Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 7920 proves that it does this. For example, (2nd āāØ3, 4ā©) = 4. Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 6176 and op2ndb 6175). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.) |
ā¢ 2nd = (š„ ā V ā¦ āŖ ran {š„}) | ||
Theorem | 1stval 7913 | 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 7914 | 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 7915 | Value of the first-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
ā¢ (Ā¬ š“ ā (V Ć V) ā (1st āš“) = ā ) | ||
Theorem | 2ndnpr 7916 | Value of the second-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
ā¢ (Ā¬ š“ ā (V Ć V) ā (2nd āš“) = ā ) | ||
Theorem | 1st0 7917 | The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.) |
ā¢ (1st āā ) = ā | ||
Theorem | 2nd0 7918 | The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.) |
ā¢ (2nd āā ) = ā | ||
Theorem | op1st 7919 | Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
ā¢ š“ ā V & ā¢ šµ ā V ā ā¢ (1st āāØš“, šµā©) = š“ | ||
Theorem | op2nd 7920 | Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.) |
ā¢ š“ ā V & ā¢ šµ ā V ā ā¢ (2nd āāØš“, šµā©) = šµ | ||
Theorem | op1std 7921 | Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
ā¢ š“ ā V & ā¢ šµ ā V ā ā¢ (š¶ = āØš“, šµā© ā (1st āš¶) = š“) | ||
Theorem | op2ndd 7922 | Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.) |
ā¢ š“ ā V & ā¢ šµ ā V ā ā¢ (š¶ = āØš“, šµā© ā (2nd āš¶) = šµ) | ||
Theorem | op1stg 7923 | Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
ā¢ ((š“ ā š ā§ šµ ā š) ā (1st āāØš“, šµā©) = š“) | ||
Theorem | op2ndg 7924 | Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.) |
ā¢ ((š“ ā š ā§ šµ ā š) ā (2nd āāØš“, šµā©) = šµ) | ||
Theorem | ot1stg 7925 | 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 7925, ot2ndg 7926, ot3rdg 7927.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
ā¢ ((š“ ā š ā§ šµ ā š ā§ š¶ ā š) ā (1st ā(1st āāØš“, šµ, š¶ā©)) = š“) | ||
Theorem | ot2ndg 7926 | Extract the second member of an ordered triple. (See ot1stg 7925 comment.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
ā¢ ((š“ ā š ā§ šµ ā š ā§ š¶ ā š) ā (2nd ā(1st āāØš“, šµ, š¶ā©)) = šµ) | ||
Theorem | ot3rdg 7927 | Extract the third member of an ordered triple. (See ot1stg 7925 comment.) (Contributed by NM, 3-Apr-2015.) |
ā¢ (š¶ ā š ā (2nd āāØš“, šµ, š¶ā©) = š¶) | ||
Theorem | 1stval2 7928 | 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 7929 | 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 7930 | The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
ā¢ (š = āØš“, šµ, š¶ā© ā ((š“ ā š ā§ šµ ā š ā§ š¶ ā š) ā ((1st ā(1st āš)) = š“ ā§ (2nd ā(1st āš)) = šµ ā§ (2nd āš) = š¶))) | ||
Theorem | fo1st 7931 | 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 7932 | 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 7933 | 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 7934 | 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 7935 | 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 7936 | 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 7937 | 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 7938 | 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 7939* | 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 7940* | 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 7941 | Composition of the first member function with another function. (Contributed by NM, 12-Oct-2007.) |
ā¢ (š¹:š“ā¶(šµ Ć š¶) ā (1st ā š¹):š“ā¶šµ) | ||
Theorem | 2ndcof 7942 | Composition of the second member function with another function. (Contributed by FL, 15-Oct-2012.) |
ā¢ (š¹:š“ā¶(šµ Ć š¶) ā (2nd ā š¹):š“ā¶š¶) | ||
Theorem | xp1st 7943 | Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
ā¢ (š“ ā (šµ Ć š¶) ā (1st āš“) ā šµ) | ||
Theorem | xp2nd 7944 | Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
ā¢ (š“ ā (šµ Ć š¶) ā (2nd āš“) ā š¶) | ||
Theorem | elxp6 7945 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7849. (Contributed by NM, 9-Oct-2004.) |
ā¢ (š“ ā (šµ Ć š¶) ā (š“ = āØ(1st āš“), (2nd āš“)ā© ā§ ((1st āš“) ā šµ ā§ (2nd āš“) ā š¶))) | ||
Theorem | elxp7 7946 | Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp4 7849. (Contributed by NM, 19-Aug-2006.) |
ā¢ (š“ ā (šµ Ć š¶) ā (š“ ā (V Ć V) ā§ ((1st āš“) ā šµ ā§ (2nd āš“) ā š¶))) | ||
Theorem | eqopi 7947 | Equality with an ordered pair. (Contributed by NM, 15-Dec-2008.) (Revised by Mario Carneiro, 23-Feb-2014.) |
ā¢ ((š“ ā (š Ć š) ā§ ((1st āš“) = šµ ā§ (2nd āš“) = š¶)) ā š“ = āØšµ, š¶ā©) | ||
Theorem | xp2 7948* | Representation of Cartesian product based on ordered pair component functions. (Contributed by NM, 16-Sep-2006.) |
ā¢ (š“ Ć šµ) = {š„ ā (V Ć V) ā£ ((1st āš„) ā š“ ā§ (2nd āš„) ā šµ)} | ||
Theorem | unielxp 7949 | The membership relation for a Cartesian product is inherited by union. (Contributed by NM, 16-Sep-2006.) |
ā¢ (š“ ā (šµ Ć š¶) ā āŖ š“ ā āŖ (šµ Ć š¶)) | ||
Theorem | 1st2nd2 7950 | 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 7951 | Reconstruction of an ordered pair in terms of its components. (Contributed by NM, 25-Feb-2014.) |
ā¢ (š“ ā (V Ć V) ā š“ = āØ(1st āš“), (2nd āš“)ā©) | ||
Theorem | xpopth 7952 | An ordered pair theorem for members of Cartesian products. (Contributed by NM, 20-Jun-2007.) |
ā¢ ((š“ ā (š¶ Ć š·) ā§ šµ ā (š Ć š)) ā (((1st āš“) = (1st āšµ) ā§ (2nd āš“) = (2nd āšµ)) ā š“ = šµ)) | ||
Theorem | eqop 7953 | 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 7954 | Two ways to express equality with an ordered pair. (Contributed by NM, 25-Feb-2014.) |
ā¢ šµ ā V & ā¢ š¶ ā V ā ā¢ (š“ = āØšµ, š¶ā© ā (š“ ā (V Ć V) ā§ ((1st āš“) = šµ ā§ (2nd āš“) = š¶))) | ||
Theorem | op1steq 7955* | 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 7956* | 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 7957* | A member of a nested Cartesian product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
ā¢ (š“ ā ((šµ Ć š¶) Ć š·) ā āš„ ā šµ āš¦ ā š¶ āš§ ā š· š“ = āØš„, š¦, š§ā©) | ||
Theorem | el2xptp0 7958 | 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 7959 | Swap the members of an ordered pair. (Contributed by NM, 31-Dec-2014.) |
ā¢ (š“ ā (šµ Ć š¶) ā āŖ ā”{š“} = āØ(2nd āš“), (1st āš“)ā©) | ||
Theorem | 1st2nd 7960 | 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 7961 | 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 7962 | 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 7963 | 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 7964* | Two ways of expressing membership in the domain of a relation. (Contributed by NM, 22-Sep-2013.) |
ā¢ (Rel š“ ā (šµ ā dom š“ ā āš„ ā š“ (1st āš„) = šµ)) | ||
Theorem | reldm 7965* | An expression for the domain of a relation. (Contributed by NM, 22-Sep-2013.) |
ā¢ (Rel š“ ā dom š“ = ran (š„ ā š“ ā¦ (1st āš„))) | ||
Theorem | releldmdifi 7966* | 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 7967 | 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 7968 | 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 7969* | 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 7970 | Equality theorem for substitution of a class for an ordered pair (analogue of sbceq1a 3748 that avoids the existential quantifiers of copsexg 5445). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
ā¢ (š“ = āØš„, š¦ā© ā ([(1st āš“) / š„][(2nd āš“) / š¦]š ā š)) | ||
Theorem | csbopeq1a 7971 | Equality theorem for substitution of a class š“ for an ordered pair āØš„, š¦ā© in šµ (analogue of csbeq1a 3867). (Contributed by NM, 19-Aug-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
ā¢ (š“ = āØš„, š¦ā© ā ā¦(1st āš“) / š„ā¦ā¦(2nd āš“) / š¦ā¦šµ = šµ) | ||
Theorem | dfopab2 7972* | 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 7973* | 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 7974* | Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008.) |
ā¢ (š¤ = āØš„, š¦ā© ā (š ā š)) ā ā¢ {āØš¤, š§ā© ā£ (š¤ ā (V Ć V) ā§ š)} = {āØāØš„, š¦ā©, š§ā© ā£ š} | ||
Theorem | dfoprab4 7975* | Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 3-Sep-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
ā¢ (š¤ = āØš„, š¦ā© ā (š ā š)) ā ā¢ {āØš¤, š§ā© ā£ (š¤ ā (š“ Ć šµ) ā§ š)} = {āØāØš„, š¦ā©, š§ā© ā£ ((š„ ā š“ ā§ š¦ ā šµ) ā§ š)} | ||
Theorem | dfoprab4f 7976* | 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 7977* | Condition for an operation to be a set. (Contributed by Thierry Arnoux, 25-Jun-2019.) |
ā¢ (š ā š“ ā š) & ā¢ (š ā šµ ā š) & ā¢ ((š ā§ š) ā š„ ā š“) & ā¢ ((š ā§ š) ā š¦ ā šµ) ā ā¢ (š ā {āØš„, š¦ā© ā£ š} ā V) | ||
Theorem | opabn1stprc 7978* | 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 7979* | 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 7980* | 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 7981* | Define the Cartesian product of three classes. Compare df-xp 5636. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 3-Nov-2015.) |
ā¢ ((š“ Ć šµ) Ć š¶) = {āØāØš„, š¦ā©, š§ā© ā£ (š„ ā š“ ā§ š¦ ā šµ ā§ š§ ā š¶)} | ||
Theorem | elopabi 7982* | A consequence of membership in an ordered-pair class abstraction, using ordered pair extractors. (Contributed by NM, 29-Aug-2006.) |
ā¢ (š„ = (1st āš“) ā (š ā š)) & ā¢ (š¦ = (2nd āš“) ā (š ā š)) ā ā¢ (š“ ā {āØš„, š¦ā© ā£ š} ā š) | ||
Theorem | eloprabi 7983* | 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 7984* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016.) |
ā¢ (š„ ā š“, š¦ ā šµ ā¦ š¶) = (š§ ā āŖ š„ ā š“ ({š„} Ć šµ) ā¦ ā¦(1st āš§) / š„ā¦ā¦(2nd āš§) / š¦ā¦š¶) | ||
Theorem | mpompts 7985* | Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Sep-2015.) |
ā¢ (š„ ā š“, š¦ ā šµ ā¦ š¶) = (š§ ā (š“ Ć šµ) ā¦ ā¦(1st āš§) / š„ā¦ā¦(2nd āš§) / š¦ā¦š¶) | ||
Theorem | dmmpossx 7986* | The domain of a mapping is a subset of its base class. (Contributed by Mario Carneiro, 9-Feb-2015.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ dom š¹ ā āŖ š„ ā š“ ({š„} Ć šµ) | ||
Theorem | fmpox 7987* | 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 7988* | Functionality, domain and range of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ (āš„ ā š“ āš¦ ā šµ š¶ ā š· ā š¹:(š“ Ć šµ)ā¶š·) | ||
Theorem | fnmpo 7989* | Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ (āš„ ā š“ āš¦ ā šµ š¶ ā š ā š¹ Fn (š“ Ć šµ)) | ||
Theorem | fnmpoi 7990* | Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) & ā¢ š¶ ā V ā ā¢ š¹ Fn (š“ Ć šµ) | ||
Theorem | dmmpo 7991* | Domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) & ā¢ š¶ ā V ā ā¢ dom š¹ = (š“ Ć šµ) | ||
Theorem | ovmpoelrn 7992* | An operation's value belongs to its range. (Contributed by AV, 27-Jan-2020.) |
ā¢ š = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ ((āš„ ā š“ āš¦ ā šµ š¶ ā š ā§ š ā š“ ā§ š ā šµ) ā (ššš) ā š) | ||
Theorem | dmmpoga 7993* | Domain of an operation given by the maps-to notation, closed form of dmmpo 7991. (Contributed by Alexander van der Vekens, 10-Feb-2019.) (Proof shortened by Lammen, 29-May-2024.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ (āš„ ā š“ āš¦ ā šµ š¶ ā š ā dom š¹ = (š“ Ć šµ)) | ||
Theorem | dmmpogaOLD 7994* | Obsolete version of dmmpoga 7993 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 7995* | Domain of an operation given by the maps-to notation, closed form of dmmpo 7991. 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 7996* | Existence of an operation class abstraction (version for dependent domains). (Contributed by Mario Carneiro, 30-Dec-2016.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ ((š“ ā š ā§ āš„ ā š“ šµ ā š) ā š¹ ā V) | ||
Theorem | mpoexg 7997* | Existence of an operation class abstraction (special case). (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 1-Sep-2015.) |
ā¢ š¹ = (š„ ā š“, š¦ ā šµ ā¦ š¶) ā ā¢ ((š“ ā š ā§ šµ ā š) ā š¹ ā V) | ||
Theorem | mpoexga 7998* | 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 7999* | Weak version of mpoex 8000 that holds without ax-rep 5240. 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 | ||
Theorem | mpoex 8000* | If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by Mario Carneiro, 20-Dec-2013.) |
ā¢ š“ ā V & ā¢ šµ ā V ā ā¢ (š„ ā š“, š¦ ā šµ ā¦ š¶) ā V |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |