Type  Label  Description 
Statement 

Theorem  fvmpts 5701* 
Value of a function given in mapsto notation, using explicit class
substitution. (Contributed by Scott Fenton, 17Jul2013.) (Revised by
Mario Carneiro, 31Aug2015.)



Theorem  fvmptd 5702* 
Deduction version of fvmpt 5700. (Contributed by Scott Fenton,
18Feb2013.) (Revised by Mario Carneiro, 31Aug2015.)



Theorem  fvmpt2i 5703* 
Value of a function given by the "maps to" notation. (Contributed by
Mario Carneiro, 23Apr2014.)



Theorem  fvmpt2 5704* 
Value of a function given by the "maps to" notation. (Contributed by
FL, 21Jun2010.)



Theorem  fvmptss 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, 13Feb2015.)



Theorem  dffn5v 5706* 
Representation of a function in terms of its values. (Contributed by
FL, 14Sep2013.) (Revised by Mario Carneiro, 16Dec2013.)



Theorem  fnov2 5707* 
Representation of a function in terms of its values. (Contributed by
Mario Carneiro, 23Dec2013.)



Theorem  mpt2mptx 5708* 
Express a twoargument function as a oneargument function, or
viceversa. In this version is not assumed to be
constant
w.r.t .
(Contributed by Mario Carneiro, 29Dec2014.)



Theorem  mpt2mpt 5709* 
Express a twoargument function as a oneargument function, or
viceversa. (Contributed by Mario Carneiro, 17Dec2013.) (Revised by
Mario Carneiro, 29Dec2014.)



Theorem  ovmpt4g 5710* 
Value of a function given by the "maps to" notation. (This is the
operation analog of fvmpt2 5704.) (Contributed by NM, 21Feb2004.)
(Revised by Mario Carneiro, 1Sep2015.)



Theorem  ov2gf 5711* 
The value of an operation class abstraction. A version of ovmpt2g 5715
using boundvariable hypotheses. (Contributed by NM, 17Aug2006.)
(Revised by Mario Carneiro, 19Dec2013.)



Theorem  ovmpt2x 5712* 
The value of an operation class abstraction. Variant of ovmpt2ga 5713
which does not require and to be
distinct. (Contributed by
Jeff Madsen, 10Jun2010.) (Revised by Mario Carneiro, 20Dec2013.)



Theorem  ovmpt2ga 5713* 
Value of an operation given by a mapsto rule. Equivalent to ov2ag 5598.
(Contributed by Mario Carneiro, 19Dec2013.)



Theorem  ovmpt2a 5714* 
Value of an operation given by a mapsto rule. Equivalent to
ov2ag 5598. (Contributed by set.mm contributors,
19Dec2013.)



Theorem  ovmpt2g 5715* 
Value of an operation given by a mapsto rule. (Unnecessary distinct
variable restrictions were removed by David Abernethy, 19Jun2012.)
(Contributed by set.mm contributors, 2Oct2007.) (Revised by set.mm
contributors, 24Jul2012.)



Theorem  ovmpt2 5716* 
Value of an operation given by a mapsto rule. Equivalent to ov2 in
set.mm. (Contributed by set.mm contributors, 12Sep2011.)



Theorem  rnmpt2 5717* 
The range of an operation given by the "maps to" notation.
(Contributed
by FL, 20Jun2011.)



Theorem  mptv 5718* 
Function with universal domain in mapsto notation. (Contributed by
set.mm contributors, 16Aug2013.)



Theorem  mpt2v 5719* 
Operation with universal domain in mapsto notation. (Contributed by
set.mm contributors, 16Aug2013.)



Theorem  mptresid 5720* 
The restricted identity expressed with the "maps to" notation.
(Contributed by FL, 25Apr2012.)



Theorem  fvmptex 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, 14Jul2013.)
(Revised by Mario Carneiro, 23Apr2014.)



Theorem  fvmptf 5722* 
Value of a function given by an orderedpair class abstraction. This
version of fvmptg 5698 uses boundvariable hypotheses instead of
distinct
variable conditions. (Contributed by NM, 8Nov2005.) (Revised by
Mario Carneiro, 15Oct2016.)



Theorem  fvmptnf 5723* 
The value of a function given by an orderedpair class abstraction is
the empty set when the class it would otherwise map to is a proper
class. This version of fvmptn 5724 uses boundvariable hypotheses
instead
of distinct variable conditions. (Contributed by NM, 21Oct2003.)
(Revised by Mario Carneiro, 11Sep2015.)



Theorem  fvmptn 5724* 
This somewhat nonintuitive 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, 21Oct2003.) (Revised by Mario Carneiro,
9Sep2013.)



Theorem  fvmptss2 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, 13Feb2015.)



Theorem  f1od 5726* 
Describe an implicit onetoone onto function. (Contributed by Mario
Carneiro, 12May2014.)



Theorem  f1o2d 5727* 
Describe an implicit onetoone onto function. (Contributed by Mario
Carneiro, 12May2014.)



Theorem  dfswap3 5728* 
Alternate definition of Swap as an operator
abstraction.
(Contributed by SF, 23Feb2015.)

Swap 

Theorem  dfswap4 5729* 
Alternate definition of Swap as an operator
mapping. (Contributed
by SF, 23Feb2015.)

Swap 

Theorem  fmpt2x 5730* 
Functionality, domain and codomain of a class given by the "maps to"
notation, where is not constant but depends on .
(Contributed by NM, 29Dec2014.)



Theorem  fmpt2 5731* 
Functionality, domain and range of a class given by the "maps to"
notation. (Contributed by FL, 17May2010.)



Theorem  fnmpt2 5732* 
Functionality and domain of a class given by the "maps to" notation.
(Contributed by FL, 17May2010.)



Theorem  fnmpt2i 5733* 
Functionality and domain of a class given by the "maps to" notation.
(Contributed by FL, 17May2010.)



Theorem  dmmpt2 5734* 
Domain of a class given by the "maps to" notation. (Contributed by
FL,
17May2010.)



2.3.10 Set construction lemmas


Syntax  ctxp 5735 
Extend the definition of a class to include the tail cross product.



Definition  dftxp 5736 
Define the tail cross product of two classes. Definition from [Holmes]
p. 40. See brtxp 5783 for membership. (Contributed by SF,
9Feb2015.)



Syntax  cpprod 5737 
Extend the definition of a class to include the parallel product
operation.

PProd 

Definition  dfpprod 5738 
Define the parallel product operation. (Contributed by SF,
9Feb2015.)

PProd


Syntax  cfix 5739 
Extend the definition of a class to include the fixed points of a
relationship.



Definition  dffix 5740 
Define the fixed points of a relationship. (Contributed by SF,
9Feb2015.)



Syntax  ccup 5741 
Extend the definition of a class to include the cup function.

Cup 

Definition  dfcup 5742* 
Define the cup function. (Contributed by SF, 9Feb2015.)

Cup 

Syntax  cdisj 5743 
Extend the definition of a class to include the disjoint relationship.

Disj 

Definition  dfdisj 5744* 
Define the relationship of all disjoint sets. (Contributed by SF,
9Feb2015.)

Disj


Syntax  caddcfn 5745 
Extend the definition of a class to include the cardinal sum function.

AddC 

Definition  dfaddcfn 5746* 
Define the function representing cardinal sum. (Contributed by SF,
9Feb2015.)

AddC 

Syntax  ccompose 5747 
Extend the definition of a class to include the compostion function.

Compose 

Definition  dfcompose 5748* 
Define the composition function. (Contributed by Scott Fenton,
19Apr2021.)

Compose 

Syntax  cins2 5749 
Extend the definition of a class to include the second insertion
operation.

Ins2 

Definition  dfins2 5750 
Define the second insertion operation. (Contributed by SF,
9Feb2015.)

Ins2


Syntax  cins3 5751 
Extend the definition of a class to include the third insertion
operation.

Ins3 

Definition  dfins3 5752 
Define the third insertion operation. (Contributed by SF, 9Feb2015.)

Ins3


Syntax  cimage 5753 
Extend the definition of a class to include the image function.

Image 

Definition  dfimage 5754 
Define the image function of a class. (Contributed by SF, 9Feb2015.)
(Revised by Scott Fenton, 19Apr2021.)

Image
∼ Ins2 S Ins3 S SI 1_{c} 

Syntax  cins4 5755 
Extend the definition of a class to include the fourth insertion
operation.

Ins4 

Definition  dfins4 5756 
Define the fourth insertion operation. (Contributed by SF,
9Feb2015.)

Ins4


Syntax  csi3 5757 
Extend the definition of a class to include the triple singleton image.

SI_{3} 

Definition  dfsi3 5758 
Define the triple singleton image. (Contributed by SF, 9Feb2015.)

SI_{3} SI
SI
SI _{1} 

Syntax  cfuns 5759 
Extend the definition of a class to include the set of all functions.

Funs 

Definition  dffuns 5760 
Define the class of all functions. (Contributed by SF, 9Feb2015.)

Funs 

Syntax  cfns 5761 
Extend the definition of a class to include the function with domain
relationship.

Fns 

Definition  dffns 5762* 
Define the function with domain relationship. (Contributed by SF,
9Feb2015.)

Fns 

Syntax  ccross 5763 
Extend the definition of a class to include the cross product function.

Cross 

Definition  dfcross 5764* 
Define the cross product function. (Contributed by SF, 9Feb2015.)

Cross 

Syntax  cpw1fn 5765 
Extend the definition of a class to include the unit power class
function.

Pw1Fn 

Definition  dfpw1fn 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, 9Feb2015.)

Pw1Fn
1_{c} _{1} 

Syntax  cfullfun 5767 
Extend the definition of a class to include the full function
operation.

FullFun 

Definition  dffullfun 5768 
Define the full function operator. This is a function over that
agrees with the function value of at every point. (Contributed by
SF, 9Feb2015.)

FullFun
∼ ∼ ∼ 

Syntax  cdomfn 5769 
Extend the definition of a class to include the domain function.

Dom 

Definition  dfdomfn 5770 
Define the domain function. This is a function wrapper for the domain
operator. (Contributed by Scott Fenton, 9Aug2019.)

Dom 

Syntax  cranfn 5771 
Extend the definition of a class to include the range function.

Ran 

Definition  dfranfn 5772 
Define the range function. This is a function wrapper for the range
operator. (Contributed by Scott Fenton, 9Aug2019.)

Ran 

Theorem  brsnsi 5773 
Binary relationship of singletons in a singleton image. (Contributed by
SF, 9Feb2015.)

SI 

Theorem  opsnelsi 5774 
Ordered pair membership of singletons in a singleton image.
(Contributed by SF, 9Feb2015.)

SI 

Theorem  brsnsi1 5775* 
Binary relationship of a singleton to an arbitrary set in a singleton
image. (Contributed by SF, 9Mar2015.)

SI 

Theorem  brsnsi2 5776* 
Binary relationship of an arbitrary set to a singleton in a singleton
image. (Contributed by SF, 9Mar2015.)

SI 

Theorem  brco1st 5777 
Binary relationship of composition with . (Contributed by SF,
9Feb2015.)



Theorem  brco2nd 5778 
Binary relationship of composition with . (Contributed by SF,
9Feb2015.)



Theorem  txpeq1 5779 
Equality theorem for tail cross product. (Contributed by Scott Fenton,
31Jul2019.)



Theorem  txpeq2 5780 
Equality theorem for tail cross product. (Contributed by Scott Fenton,
31Jul2019.)



Theorem  trtxp 5781 
Trinary relationship over a tail cross product. (Contributed by SF,
13Feb2015.)



Theorem  oteltxp 5782 
Ordered triple membership in a tail cross product. (Contributed by SF,
13Feb2015.)



Theorem  brtxp 5783* 
Binary relationship over a tail cross product. (Contributed by SF,
11Feb2015.)



Theorem  txpexg 5784 
The tail cross product of two sets is a set. (Contributed by SF,
9Feb2015.)



Theorem  txpex 5785 
The tail cross product of two sets is a set. (Contributed by SF,
9Feb2015.)



Theorem  restxp 5786 
Restriction distributes over tail cross product. (Contributed by SF,
24Feb2015.)



Theorem  elfix 5787 
Membership in the fixed points of a relationship. (Contributed by SF,
11Feb2015.)



Theorem  fixexg 5788 
The fixed points of a set form a set. (Contributed by SF,
11Feb2015.)



Theorem  fixex 5789 
The fixed points of a set form a set. (Contributed by SF,
11Feb2015.)



Theorem  op1st2nd 5790 
Express equality to an ordered pair via and .
(Contributed by SF, 12Feb2015.)



Theorem  otelins2 5791 
Ordered triple membership in Ins2. (Contributed
by SF,
13Feb2015.)

Ins2 

Theorem  otelins3 5792 
Ordered triple membership in Ins3. (Contributed
by SF,
13Feb2015.)

Ins3 

Theorem  brimage 5793 
Binary relationship over the image function. (Contributed by SF,
11Feb2015.)

Image


Theorem  oqelins4 5794 
Ordered quadruple membership in Ins4.
(Contributed by SF,
13Feb2015.)

Ins4


Theorem  ins2exg 5795 
Ins2 preserves sethood. (Contributed by SF,
9Mar2015.)

Ins2 

Theorem  ins3exg 5796 
Ins3 preserves sethood. (Contributed by SF,
22Feb2015.)

Ins3 

Theorem  ins2ex 5797 
Ins2 preserves sethood. (Contributed by SF,
12Feb2015.)

Ins2 

Theorem  ins3ex 5798 
Ins3 preserves sethood. (Contributed by SF,
12Feb2015.)

Ins3 

Theorem  ins4ex 5799 
Ins4 preserves sethood. (Contributed by SF,
12Feb2015.)

Ins4 

Theorem  imageexg 5800 
The image function of a set is a set. (Contributed by SF,
11Feb2015.)

Image 