Home New Foundations ExplorerTheorem 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.)

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.)

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.)

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.

Definitiondf-addcfn 5746* Define the function representing cardinal sum. (Contributed by SF, 9-Feb-2015.)

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

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-6337
 Copyright terms: Public domain < Previous  Next >