Type  Label  Description 
Statement 

2.6.13 Functions (continued)


Theorem  resfunexgALT 6001 
The restriction of a function to a set exists. Compare Proposition 6.17
of [TakeutiZaring] p. 28. This
version has a shorter proof than
resfunexg 5634 but requires axpow 4093 and axun 4350. (Contributed by NM,
7Apr1995.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  cofunexg 6002 
Existence of a composition when the first member is a function.
(Contributed by NM, 8Oct2007.)



Theorem  cofunex2g 6003 
Existence of a composition when the second member is onetoone.
(Contributed by NM, 8Oct2007.)



Theorem  fnexALT 6004 
If the domain of a function is a set, the function is a set. Theorem
6.16(1) of [TakeutiZaring] p. 28.
This theorem is derived using the Axiom
of Replacement in the form of funimaexg 5202. This version of fnex 5635
uses
axpow 4093 and axun 4350, whereas fnex 5635
does not. (Contributed by NM,
14Aug1994.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  funrnex 6005 
If the domain of a function exists, so does its range. Part of Theorem
4.15(v) of [Monk1] p. 46. This theorem is
derived using the Axiom of
Replacement in the form of funex 5636. (Contributed by NM, 11Nov1995.)



Theorem  fornex 6006 
If the domain of an onto function exists, so does its codomain.
(Contributed by NM, 23Jul2004.)



Theorem  f1dmex 6007 
If the codomain of a onetoone function exists, so does its domain. This
can be thought of as a form of the Axiom of Replacement. (Contributed by
NM, 4Sep2004.)



Theorem  abrexex 6008* 
Existence of a class abstraction of existentially restricted sets.
is normally a freevariable parameter in the class expression
substituted for , which can be thought of as . This
simplelooking theorem is actually quite powerful and appears to involve
the Axiom of Replacement in an intrinsic way, as can be seen by tracing
back through the path mptexg 5638, funex 5636, fnex 5635, resfunexg 5634, and
funimaexg 5202. See also abrexex2 6015. (Contributed by NM, 16Oct2003.)
(Proof shortened by Mario Carneiro, 31Aug2015.)



Theorem  abrexexg 6009* 
Existence of a class abstraction of existentially restricted sets.
is normally a freevariable parameter in . The antecedent assures
us that is a
set. (Contributed by NM, 3Nov2003.)



Theorem  iunexg 6010* 
The existence of an indexed union. is normally a freevariable
parameter in .
(Contributed by NM, 23Mar2006.)



Theorem  abrexex2g 6011* 
Existence of an existentially restricted class abstraction.
(Contributed by Jeff Madsen, 2Sep2009.)



Theorem  opabex3d 6012* 
Existence of an ordered pair abstraction, deduction version.
(Contributed by Alexander van der Vekens, 19Oct2017.)



Theorem  opabex3 6013* 
Existence of an ordered pair abstraction. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  iunex 6014* 
The existence of an indexed union. is normally a freevariable
parameter in the class expression substituted for , which can be
read informally as . (Contributed by NM, 13Oct2003.)



Theorem  abrexex2 6015* 
Existence of an existentially restricted class abstraction. is
normally has freevariable parameters and . See also
abrexex 6008. (Contributed by NM, 12Sep2004.)



Theorem  abexssex 6016* 
Existence of a class abstraction with an existentially quantified
expression. Both and can be
free in .
(Contributed
by NM, 29Jul2006.)



Theorem  abexex 6017* 
A condition where a class builder continues to exist after its wff is
existentially quantified. (Contributed by NM, 4Mar2007.)



Theorem  oprabexd 6018* 
Existence of an operator abstraction. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  oprabex 6019* 
Existence of an operation class abstraction. (Contributed by NM,
19Oct2004.)



Theorem  oprabex3 6020* 
Existence of an operation class abstraction (special case).
(Contributed by NM, 19Oct2004.)



Theorem  oprabrexex2 6021* 
Existence of an existentially restricted operation abstraction.
(Contributed by Jeff Madsen, 11Jun2010.)



Theorem  ab2rexex 6022* 
Existence of a class abstraction of existentially restricted sets.
Variables and
are normally
freevariable parameters in the
class expression substituted for , which can be thought of as
. See comments for abrexex 6008. (Contributed by NM,
20Sep2011.)



Theorem  ab2rexex2 6023* 
Existence of an existentially restricted class abstraction.
normally has freevariable parameters , , and .
Compare abrexex2 6015. (Contributed by NM, 20Sep2011.)



Theorem  xpexgALT 6024 
The cross product of two sets is a set. Proposition 6.2 of
[TakeutiZaring] p. 23. This
version is proven using Replacement; see
xpexg 4648 for a version that uses the Power Set axiom
instead.
(Contributed by Mario Carneiro, 20May2013.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  offval3 6025* 
General value of with no assumptions on functionality
of and . (Contributed by Stefan
O'Rear, 24Jan2015.)



Theorem  offres 6026 
Pointwise combination commutes with restriction. (Contributed by Stefan
O'Rear, 24Jan2015.)



Theorem  ofmres 6027* 
Equivalent expressions for a restriction of the function operation map.
Unlike which is a proper class,
can
be a set by ofmresex 6028, allowing it to be used as a function or
structure argument. By ofmresval 5986, the restricted operation map
values are the same as the original values, allowing theorems for
to be reused. (Contributed by NM, 20Oct2014.)



Theorem  ofmresex 6028 
Existence of a restriction of the function operation map. (Contributed
by NM, 20Oct2014.)



2.6.14 First and second members of an ordered
pair


Syntax  c1st 6029 
Extend the definition of a class to include the first member an ordered
pair function.



Syntax  c2nd 6030 
Extend the definition of a class to include the second member an ordered
pair function.



Definition  df1st 6031 
Define a function that extracts the first member, or abscissa, of an
ordered pair. Theorem op1st 6037 proves that it does this. For example,
( 3 , 4 ) = 3 . Equivalent to Definition
5.13 (i) of
[Monk1] p. 52 (compare op1sta 5015 and op1stb 4394). The notation is the same
as Monk's. (Contributed by NM, 9Oct2004.)



Definition  df2nd 6032 
Define a function that extracts the second member, or ordinate, of an
ordered pair. Theorem op2nd 6038 proves that it does this. For example,
3 , 4 ) = 4 . Equivalent to Definition 5.13 (ii)
of [Monk1] p. 52 (compare op2nda 5018 and op2ndb 5017). The notation is the
same as Monk's. (Contributed by NM, 9Oct2004.)



Theorem  1stvalg 6033 
The value of the function that extracts the first member of an ordered
pair. (Contributed by NM, 9Oct2004.) (Revised by Mario Carneiro,
8Sep2013.)



Theorem  2ndvalg 6034 
The value of the function that extracts the second member of an ordered
pair. (Contributed by NM, 9Oct2004.) (Revised by Mario Carneiro,
8Sep2013.)



Theorem  1st0 6035 
The value of the firstmember function at the empty set. (Contributed by
NM, 23Apr2007.)



Theorem  2nd0 6036 
The value of the secondmember function at the empty set. (Contributed by
NM, 23Apr2007.)



Theorem  op1st 6037 
Extract the first member of an ordered pair. (Contributed by NM,
5Oct2004.)



Theorem  op2nd 6038 
Extract the second member of an ordered pair. (Contributed by NM,
5Oct2004.)



Theorem  op1std 6039 
Extract the first member of an ordered pair. (Contributed by Mario
Carneiro, 31Aug2015.)



Theorem  op2ndd 6040 
Extract the second member of an ordered pair. (Contributed by Mario
Carneiro, 31Aug2015.)



Theorem  op1stg 6041 
Extract the first member of an ordered pair. (Contributed by NM,
19Jul2005.)



Theorem  op2ndg 6042 
Extract the second member of an ordered pair. (Contributed by NM,
19Jul2005.)



Theorem  ot1stg 6043 
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 6043,
ot2ndg 6044, ot3rdgg 6045.) (Contributed by NM, 3Apr2015.) (Revised
by
Mario Carneiro, 2May2015.)



Theorem  ot2ndg 6044 
Extract the second member of an ordered triple. (See ot1stg 6043 comment.)
(Contributed by NM, 3Apr2015.) (Revised by Mario Carneiro,
2May2015.)



Theorem  ot3rdgg 6045 
Extract the third member of an ordered triple. (See ot1stg 6043 comment.)
(Contributed by NM, 3Apr2015.)



Theorem  1stval2 6046 
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, 18Aug2006.)



Theorem  2ndval2 6047 
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, 18Aug2006.)



Theorem  fo1st 6048 
The function
maps the universe onto the universe. (Contributed
by NM, 14Oct2004.) (Revised by Mario Carneiro, 8Sep2013.)



Theorem  fo2nd 6049 
The function
maps the universe onto the universe. (Contributed
by NM, 14Oct2004.) (Revised by Mario Carneiro, 8Sep2013.)



Theorem  f1stres 6050 
Mapping of a restriction of the (first member of an ordered
pair) function. (Contributed by NM, 11Oct2004.) (Revised by Mario
Carneiro, 8Sep2013.)



Theorem  f2ndres 6051 
Mapping of a restriction of the (second member of an ordered
pair) function. (Contributed by NM, 7Aug2006.) (Revised by Mario
Carneiro, 8Sep2013.)



Theorem  fo1stresm 6052* 
Onto mapping of a restriction of the (first member of an ordered
pair) function. (Contributed by Jim Kingdon, 24Jan2019.)



Theorem  fo2ndresm 6053* 
Onto mapping of a restriction of the (second member of an
ordered pair) function. (Contributed by Jim Kingdon, 24Jan2019.)



Theorem  1stcof 6054 
Composition of the first member function with another function.
(Contributed by NM, 12Oct2007.)



Theorem  2ndcof 6055 
Composition of the second member function with another function.
(Contributed by FL, 15Oct2012.)



Theorem  xp1st 6056 
Location of the first element of a Cartesian product. (Contributed by
Jeff Madsen, 2Sep2009.)



Theorem  xp2nd 6057 
Location of the second element of a Cartesian product. (Contributed by
Jeff Madsen, 2Sep2009.)



Theorem  1stexg 6058 
Existence of the first member of a set. (Contributed by Jim Kingdon,
26Jan2019.)



Theorem  2ndexg 6059 
Existence of the first member of a set. (Contributed by Jim Kingdon,
26Jan2019.)



Theorem  elxp6 6060 
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp4 5021. (Contributed by NM, 9Oct2004.)



Theorem  elxp7 6061 
Membership in a cross product. This version requires no quantifiers or
dummy variables. See also elxp4 5021. (Contributed by NM, 19Aug2006.)



Theorem  oprssdmm 6062* 
Domain of closure of an operation. (Contributed by Jim Kingdon,
23Oct2023.)



Theorem  eqopi 6063 
Equality with an ordered pair. (Contributed by NM, 15Dec2008.)
(Revised by Mario Carneiro, 23Feb2014.)



Theorem  xp2 6064* 
Representation of cross product based on ordered pair component
functions. (Contributed by NM, 16Sep2006.)



Theorem  unielxp 6065 
The membership relation for a cross product is inherited by union.
(Contributed by NM, 16Sep2006.)



Theorem  1st2nd2 6066 
Reconstruction of a member of a cross product in terms of its ordered pair
components. (Contributed by NM, 20Oct2013.)



Theorem  xpopth 6067 
An ordered pair theorem for members of cross products. (Contributed by
NM, 20Jun2007.)



Theorem  eqop 6068 
Two ways to express equality with an ordered pair. (Contributed by NM,
3Sep2007.) (Proof shortened by Mario Carneiro, 26Apr2015.)



Theorem  eqop2 6069 
Two ways to express equality with an ordered pair. (Contributed by NM,
25Feb2014.)



Theorem  op1steq 6070* 
Two ways of expressing that an element is the first member of an ordered
pair. (Contributed by NM, 22Sep2013.) (Revised by Mario Carneiro,
23Feb2014.)



Theorem  2nd1st 6071 
Swap the members of an ordered pair. (Contributed by NM, 31Dec2014.)



Theorem  1st2nd 6072 
Reconstruction of a member of a relation in terms of its ordered pair
components. (Contributed by NM, 29Aug2006.)



Theorem  1stdm 6073 
The first ordered pair component of a member of a relation belongs to the
domain of the relation. (Contributed by NM, 17Sep2006.)



Theorem  2ndrn 6074 
The second ordered pair component of a member of a relation belongs to the
range of the relation. (Contributed by NM, 17Sep2006.)



Theorem  1st2ndbr 6075 
Express an element of a relation as a relationship between first and
second components. (Contributed by Mario Carneiro, 22Jun2016.)



Theorem  releldm2 6076* 
Two ways of expressing membership in the domain of a relation.
(Contributed by NM, 22Sep2013.)



Theorem  reldm 6077* 
An expression for the domain of a relation. (Contributed by NM,
22Sep2013.)



Theorem  sbcopeq1a 6078 
Equality theorem for substitution of a class for an ordered pair (analog
of sbceq1a 2913 that avoids the existential quantifiers of copsexg 4161).
(Contributed by NM, 19Aug2006.) (Revised by Mario Carneiro,
31Aug2015.)



Theorem  csbopeq1a 6079 
Equality theorem for substitution of a class for an ordered pair
in (analog of csbeq1a 3007). (Contributed by NM,
19Aug2006.) (Revised by Mario Carneiro, 31Aug2015.)



Theorem  dfopab2 6080* 
A way to define an orderedpair class abstraction without using
existential quantifiers. (Contributed by NM, 18Aug2006.) (Revised by
Mario Carneiro, 31Aug2015.)



Theorem  dfoprab3s 6081* 
A way to define an operation class abstraction without using existential
quantifiers. (Contributed by NM, 18Aug2006.) (Revised by Mario
Carneiro, 31Aug2015.)



Theorem  dfoprab3 6082* 
Operation class abstraction expressed without existential quantifiers.
(Contributed by NM, 16Dec2008.)



Theorem  dfoprab4 6083* 
Operation class abstraction expressed without existential quantifiers.
(Contributed by NM, 3Sep2007.) (Revised by Mario Carneiro,
31Aug2015.)



Theorem  dfoprab4f 6084* 
Operation class abstraction expressed without existential quantifiers.
(Unnecessary distinct variable restrictions were removed by David
Abernethy, 19Jun2012.) (Contributed by NM, 20Dec2008.) (Revised by
Mario Carneiro, 31Aug2015.)



Theorem  dfxp3 6085* 
Define the cross product of three classes. Compare dfxp 4540.
(Contributed by FL, 6Nov2013.) (Proof shortened by Mario Carneiro,
3Nov2015.)



Theorem  elopabi 6086* 
A consequence of membership in an orderedpair class abstraction, using
ordered pair extractors. (Contributed by NM, 29Aug2006.)



Theorem  eloprabi 6087* 
A consequence of membership in an operation class abstraction, using
ordered pair extractors. (Contributed by NM, 6Nov2006.) (Revised by
David Abernethy, 19Jun2012.)



Theorem  mpomptsx 6088* 
Express a twoargument function as a oneargument function, or
viceversa. (Contributed by Mario Carneiro, 24Dec2016.)



Theorem  mpompts 6089* 
Express a twoargument function as a oneargument function, or
viceversa. (Contributed by Mario Carneiro, 24Sep2015.)



Theorem  dmmpossx 6090* 
The domain of a mapping is a subset of its base class. (Contributed by
Mario Carneiro, 9Feb2015.)



Theorem  fmpox 6091* 
Functionality, domain and codomain of a class given by the mapsto
notation, where is not constant but depends on .
(Contributed by NM, 29Dec2014.)



Theorem  fmpo 6092* 
Functionality, domain and range of a class given by the mapsto
notation. (Contributed by FL, 17May2010.)



Theorem  fnmpo 6093* 
Functionality and domain of a class given by the mapsto notation.
(Contributed by FL, 17May2010.)



Theorem  mpofvex 6094* 
Sufficient condition for an operation mapsto notation to be setlike.
(Contributed by Mario Carneiro, 3Jul2019.)



Theorem  fnmpoi 6095* 
Functionality and domain of a class given by the mapsto notation.
(Contributed by FL, 17May2010.)



Theorem  dmmpo 6096* 
Domain of a class given by the mapsto notation. (Contributed by FL,
17May2010.)



Theorem  mpofvexi 6097* 
Sufficient condition for an operation mapsto notation to be setlike.
(Contributed by Mario Carneiro, 3Jul2019.)



Theorem  ovmpoelrn 6098* 
An operation's value belongs to its range. (Contributed by AV,
27Jan2020.)



Theorem  dmmpoga 6099* 
Domain of an operation given by the mapsto notation, closed form of
dmmpo 6096. (Contributed by Alexander van der Vekens,
10Feb2019.)



Theorem  dmmpog 6100* 
Domain of an operation given by the mapsto notation, closed form of
dmmpo 6096. 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, 1Jun2017.) (Proof shortened by AV, 10Feb2019.)

