HomeHome New Foundations Explorer
Theorem List (p. 58 of 64)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 5701-5800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremfvmpts 5701* Value of a function given in maps-to notation, using explicit class substitution. (Contributed by Scott Fenton, 17-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
   =>   
 
Theoremfvmptd 5702* Deduction version of fvmpt 5700. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
   &       &       &       =>   
 
Theoremfvmpt2i 5703* Value of a function given by the "maps to" notation. (Contributed by Mario Carneiro, 23-Apr-2014.)
   =>   
 
Theoremfvmpt2 5704* Value of a function given by the "maps to" notation. (Contributed by FL, 21-Jun-2010.)
   =>   
 
Theoremfvmptss 5705* If all the values of the mapping are subsets of a class , then so is any evaluation of the mapping, even if is not in the base set . (Contributed by Mario Carneiro, 13-Feb-2015.)
   =>   
 
Theoremdffn5v 5706* Representation of a function in terms of its values. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
 
Theoremfnov2 5707* Representation of a function in terms of its values. (Contributed by Mario Carneiro, 23-Dec-2013.)
 
Theoremmpt2mptx 5708* Express a two-argument function as a one-argument function, or vice-versa. In this version is not assumed to be constant w.r.t . (Contributed by Mario Carneiro, 29-Dec-2014.)
   =>   
 
Theoremmpt2mpt 5709* Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013.) (Revised by Mario Carneiro, 29-Dec-2014.)
   =>   
 
Theoremovmpt4g 5710* Value of a function given by the "maps to" notation. (This is the operation analog of fvmpt2 5704.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)
   =>   
 
Theoremov2gf 5711* The value of an operation class abstraction. A version of ovmpt2g 5715 using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 19-Dec-2013.)
 F/_   &     F/_   &     F/_   &     F/_   &     F/_   &       &       &       =>   
 
Theoremovmpt2x 5712* The value of an operation class abstraction. Variant of ovmpt2ga 5713 which does not require and to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
   &       &       =>   
 
Theoremovmpt2ga 5713* Value of an operation given by a maps-to rule. Equivalent to ov2ag 5598. (Contributed by Mario Carneiro, 19-Dec-2013.)
   &       =>   
 
Theoremovmpt2a 5714* Value of an operation given by a maps-to rule. Equivalent to ov2ag 5598. (Contributed by set.mm contributors, 19-Dec-2013.)
   &       &       =>   
 
Theoremovmpt2g 5715* Value of an operation given by a maps-to rule. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 2-Oct-2007.) (Revised by set.mm contributors, 24-Jul-2012.)
   &       &       =>   
 
Theoremovmpt2 5716* Value of an operation given by a maps-to rule. Equivalent to ov2 in set.mm. (Contributed by set.mm contributors, 12-Sep-2011.)
   &       &       &       =>   
 
Theoremrnmpt2 5717* The range of an operation given by the "maps to" notation. (Contributed by FL, 20-Jun-2011.)
   =>   
 
Theoremmptv 5718* Function with universal domain in maps-to notation. (Contributed by set.mm contributors, 16-Aug-2013.)
 
Theoremmpt2v 5719* Operation with universal domain in maps-to notation. (Contributed by set.mm contributors, 16-Aug-2013.)
 
Theoremmptresid 5720* The restricted identity expressed with the "maps to" notation. (Contributed by FL, 25-Apr-2012.)
 
Theoremfvmptex 5721* Express a function whose value may not always be a set in terms of another function for which sethood is guaranteed. (Note that is just shorthand for , and it is always a set by fvex 5339.) Note also that these functions are not the same; wherever is not a set, is not in the domain of (so it evaluates to the empty set), but is in the domain of , and is defined to be the empty set. (Contributed by Mario Carneiro, 14-Jul-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
   &       =>   
 
Theoremfvmptf 5722* Value of a function given by an ordered-pair class abstraction. This version of fvmptg 5698 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)
 F/_   &     F/_   &       &       =>   
 
Theoremfvmptnf 5723* The value of a function given by an ordered-pair class abstraction is the empty set when the class it would otherwise map to is a proper class. This version of fvmptn 5724 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
 F/_   &     F/_   &       &       =>   
 
Theoremfvmptn 5724* This somewhat non-intuitive theorem tells us the value of its function is the empty set when the class it would otherwise map to is a proper class. This is a technical lemma that can help eliminate redundant sethood antecedents otherwise required by fvmptg 5698. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 9-Sep-2013.)
   &       =>   
 
Theoremfvmptss2 5725* A mapping always evaluates to a subset of the substituted expression in the mapping, even if this is a proper class, or we are out of the domain. (Contributed by Mario Carneiro, 13-Feb-2015.)
   &       =>   
 
Theoremf1od 5726* Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
   &       &       &       =>   
 
Theoremf1o2d 5727* Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
   &       &       &       =>   
 
Theoremdfswap3 5728* Alternate definition of Swap as an operator abstraction. (Contributed by SF, 23-Feb-2015.)
Swap
 
Theoremdfswap4 5729* Alternate definition of Swap as an operator mapping. (Contributed by SF, 23-Feb-2015.)
Swap
 
Theoremfmpt2x 5730* 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.)
   =>   
 
Theoremfmpt2 5731* Functionality, domain and range of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
   =>   
 
Theoremfnmpt2 5732* Functionality and domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
   =>   
 
Theoremfnmpt2i 5733* Functionality and domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
   &       =>   
 
Theoremdmmpt2 5734* Domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
   &       =>   
 
2.3.10  Set construction lemmas
 
Syntaxctxp 5735 Extend the definition of a class to include the tail cross product.
 
Definitiondf-txp 5736 Define the tail cross product of two classes. Definition from [Holmes] p. 40. See brtxp 5783 for membership. (Contributed by SF, 9-Feb-2015.)
 
Syntaxcpprod 5737 Extend the definition of a class to include the parallel product operation.
PProd
 
Definitiondf-pprod 5738 Define the parallel product operation. (Contributed by SF, 9-Feb-2015.)
PProd
 
Syntaxcfix 5739 Extend the definition of a class to include the fixed points of a relationship.
 
Definitiondf-fix 5740 Define the fixed points of a relationship. (Contributed by SF, 9-Feb-2015.)
 
Syntaxccup 5741 Extend the definition of a class to include the cup function.
Cup
 
Definitiondf-cup 5742* Define the cup function. (Contributed by SF, 9-Feb-2015.)
Cup
 
Syntaxcdisj 5743 Extend the definition of a class to include the disjoint relationship.
Disj
 
Definitiondf-disj 5744* Define the relationship of all disjoint sets. (Contributed by SF, 9-Feb-2015.)
Disj
 
Syntaxcaddcfn 5745 Extend the definition of a class to include the cardinal sum function.
AddC
 
Definitiondf-addcfn 5746* Define the function representing cardinal sum. (Contributed by SF, 9-Feb-2015.)
AddC
 
Syntaxccompose 5747 Extend the definition of a class to include the compostion function.
Compose
 
Definitiondf-compose 5748* Define the composition function. (Contributed by Scott Fenton, 19-Apr-2021.)
Compose
 
Syntaxcins2 5749 Extend the definition of a class to include the second insertion operation.
Ins2
 
Definitiondf-ins2 5750 Define the second insertion operation. (Contributed by SF, 9-Feb-2015.)
Ins2
 
Syntaxcins3 5751 Extend the definition of a class to include the third insertion operation.
Ins3
 
Definitiondf-ins3 5752 Define the third insertion operation. (Contributed by SF, 9-Feb-2015.)
Ins3
 
Syntaxcimage 5753 Extend the definition of a class to include the image function.
Image
 
Definitiondf-image 5754 Define the image function of a class. (Contributed by SF, 9-Feb-2015.) (Revised by Scott Fenton, 19-Apr-2021.)
Image Ins2 S Ins3 S SI 1c
 
Syntaxcins4 5755 Extend the definition of a class to include the fourth insertion operation.
Ins4
 
Definitiondf-ins4 5756 Define the fourth insertion operation. (Contributed by SF, 9-Feb-2015.)
Ins4
 
Syntaxcsi3 5757 Extend the definition of a class to include the triple singleton image.
SI3
 
Definitiondf-si3 5758 Define the triple singleton image. (Contributed by SF, 9-Feb-2015.)
SI3 SI SI SI 1
 
Syntaxcfuns 5759 Extend the definition of a class to include the set of all functions.
Funs
 
Definitiondf-funs 5760 Define the class of all functions. (Contributed by SF, 9-Feb-2015.)
Funs
 
Syntaxcfns 5761 Extend the definition of a class to include the function with domain relationship.
Fns
 
Definitiondf-fns 5762* Define the function with domain relationship. (Contributed by SF, 9-Feb-2015.)
Fns
 
Syntaxccross 5763 Extend the definition of a class to include the cross product function.
Cross
 
Definitiondf-cross 5764* Define the cross product function. (Contributed by SF, 9-Feb-2015.)
Cross
 
Syntaxcpw1fn 5765 Extend the definition of a class to include the unit power class function.
Pw1Fn
 
Definitiondf-pw1fn 5766 Define the function that takes a singleton to the unit power class of its member. This function is defined in such a way as to ensure stratification. (Contributed by SF, 9-Feb-2015.)
Pw1Fn 1c 1
 
Syntaxcfullfun 5767 Extend the definition of a class to include the full function operation.
FullFun
 
Definitiondf-fullfun 5768 Define the full function operator. This is a function over that agrees with the function value of at every point. (Contributed by SF, 9-Feb-2015.)
FullFun
 
Syntaxcdomfn 5769 Extend the definition of a class to include the domain function.
Dom
 
Definitiondf-domfn 5770 Define the domain function. This is a function wrapper for the domain operator. (Contributed by Scott Fenton, 9-Aug-2019.)
Dom
 
Syntaxcranfn 5771 Extend the definition of a class to include the range function.
Ran
 
Definitiondf-ranfn 5772 Define the range function. This is a function wrapper for the range operator. (Contributed by Scott Fenton, 9-Aug-2019.)
Ran
 
Theorembrsnsi 5773 Binary relationship of singletons in a singleton image. (Contributed by SF, 9-Feb-2015.)
   &       =>    SI
 
Theoremopsnelsi 5774 Ordered pair membership of singletons in a singleton image. (Contributed by SF, 9-Feb-2015.)
   &       =>    SI
 
Theorembrsnsi1 5775* Binary relationship of a singleton to an arbitrary set in a singleton image. (Contributed by SF, 9-Mar-2015.)
   =>    SI
 
Theorembrsnsi2 5776* Binary relationship of an arbitrary set to a singleton in a singleton image. (Contributed by SF, 9-Mar-2015.)
   =>    SI
 
Theorembrco1st 5777 Binary relationship of composition with . (Contributed by SF, 9-Feb-2015.)
   &       =>   
 
Theorembrco2nd 5778 Binary relationship of composition with . (Contributed by SF, 9-Feb-2015.)
   &       =>   
 
Theoremtxpeq1 5779 Equality theorem for tail cross product. (Contributed by Scott Fenton, 31-Jul-2019.)
 
Theoremtxpeq2 5780 Equality theorem for tail cross product. (Contributed by Scott Fenton, 31-Jul-2019.)
 
Theoremtrtxp 5781 Trinary relationship over a tail cross product. (Contributed by SF, 13-Feb-2015.)
 
Theoremoteltxp 5782 Ordered triple membership in a tail cross product. (Contributed by SF, 13-Feb-2015.)
 
Theorembrtxp 5783* Binary relationship over a tail cross product. (Contributed by SF, 11-Feb-2015.)
 
Theoremtxpexg 5784 The tail cross product of two sets is a set. (Contributed by SF, 9-Feb-2015.)
 
Theoremtxpex 5785 The tail cross product of two sets is a set. (Contributed by SF, 9-Feb-2015.)
   &       =>   
 
Theoremrestxp 5786 Restriction distributes over tail cross product. (Contributed by SF, 24-Feb-2015.)
 
Theoremelfix 5787 Membership in the fixed points of a relationship. (Contributed by SF, 11-Feb-2015.)
 
Theoremfixexg 5788 The fixed points of a set form a set. (Contributed by SF, 11-Feb-2015.)
 
Theoremfixex 5789 The fixed points of a set form a set. (Contributed by SF, 11-Feb-2015.)
   =>   
 
Theoremop1st2nd 5790 Express equality to an ordered pair via and . (Contributed by SF, 12-Feb-2015.)
   &       =>   
 
Theoremotelins2 5791 Ordered triple membership in Ins2. (Contributed by SF, 13-Feb-2015.)
   =>    Ins2
 
Theoremotelins3 5792 Ordered triple membership in Ins3. (Contributed by SF, 13-Feb-2015.)
   =>    Ins3
 
Theorembrimage 5793 Binary relationship over the image function. (Contributed by SF, 11-Feb-2015.)
   &       =>    Image
 
Theoremoqelins4 5794 Ordered quadruple membership in Ins4. (Contributed by SF, 13-Feb-2015.)
   =>    Ins4
 
Theoremins2exg 5795 Ins2 preserves sethood. (Contributed by SF, 9-Mar-2015.)
Ins2
 
Theoremins3exg 5796 Ins3 preserves sethood. (Contributed by SF, 22-Feb-2015.)
Ins3
 
Theoremins2ex 5797 Ins2 preserves sethood. (Contributed by SF, 12-Feb-2015.)
   =>    Ins2
 
Theoremins3ex 5798 Ins3 preserves sethood. (Contributed by SF, 12-Feb-2015.)
   =>    Ins3
 
Theoremins4ex 5799 Ins4 preserves sethood. (Contributed by SF, 12-Feb-2015.)
   =>    Ins4
 
Theoremimageexg 5800 The image function of a set is a set. (Contributed by SF, 11-Feb-2015.)
Image
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6338
  Copyright terms: Public domain < Previous  Next >