Type  Label  Description 
Statement 

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

Image 

Theorem  dmtxp 5802 
The domain of a tail cross product is the intersection of the domains of
its arguments. (Contributed by SF, 18Feb2015.)



Theorem  txpcofun 5803 
Composition distributes over tail cross product in the case of a
function. (Contributed by SF, 18Feb2015.)



Theorem  fntxp 5804 
If and are functions, then their
tail cross product is a
function over the intersection of their domains. (Contributed by SF,
24Feb2015.)



Theorem  otsnelsi3 5805 
Ordered triple membership in triple singleton image. (Contributed by
SF, 12Feb2015.)

SI_{3} 

Theorem  si3ex 5806 
SI_{3} preserves sethood.
(Contributed by SF, 12Feb2015.)

SI_{3} 

Theorem  releqel 5807* 
Lemma to turn a membership condition into an equality condition.
(Contributed by SF, 9Mar2015.)

∼ Ins3 S Ins2 1_{c} 

Theorem  releqmpt 5808* 
Equality condition for a mapping. (Contributed by SF, 9Mar2015.)

∼
Ins3 S Ins2 1_{c} 

Theorem  releqmpt2 5809* 
Equality condition for a mapping operation. (Contributed by SF,
13Feb2015.)

Ins2 S Ins3 1_{c} 

Theorem  mptexlem 5810 
Lemma for the existence of a mapping. (Contributed by SF,
9Mar2015.)

∼ Ins3 S Ins2 1_{c} 

Theorem  mpt2exlem 5811 
Lemma for the existence of a double mapping. (Contributed by SF,
13Feb2015.)

Ins2 S Ins3 1_{c} 

Theorem  cupvalg 5812 
The value of the little cup function. (Contributed by SF,
11Feb2015.)

Cup 

Theorem  fncup 5813 
The cup function is a function over the universe.
(Contributed by SF, 11Feb2015.) (Revised by Scott Fenton,
19Apr2021.)

Cup 

Theorem  brcupg 5814 
Binary relationship form of the cup function. (Contributed by SF,
11Feb2015.)

Cup 

Theorem  brcup 5815 
Binary relationship form of the cup function. (Contributed by SF,
11Feb2015.)

Cup


Theorem  cupex 5816 
The little cup function is a set. (Contributed by SF, 11Feb2015.)

Cup 

Theorem  composevalg 5817 
The value of the composition function. (Contributed by Scott Fenton,
19Apr2021.)

Compose 

Theorem  composefn 5818 
The compose function is a function over the universe. (Contributed
by Scott Fenton, 19Apr2021.)

Compose 

Theorem  brcomposeg 5819 
Binary relationship form of the compose function. (Contributed by Scott
Fenton, 19Apr2021.)

Compose


Theorem  composeex 5820 
The compose function is a set. (Contributed by Scott Fenton,
19Apr2021.)

Compose 

Theorem  brdisjg 5821 
The binary relationship form of the Disj
relationship. (Contributed
by SF, 11Feb2015.)

Disj 

Theorem  brdisj 5822 
The binary relationship form of the Disj
relationship. (Contributed
by SF, 11Feb2015.)

Disj 

Theorem  disjex 5823 
The disjointedness relationship is a set. (Contributed by SF,
11Feb2015.)

Disj 

Theorem  addcfnex 5824 
The cardinal addition function exists. (Contributed by SF,
12Feb2015.)

AddC 

Theorem  addcfn 5825 
AddC is a function over the universe.
(Contributed by SF,
2Mar2015.) (Revised by Scott Fenton, 19Apr2021.)

AddC 

Theorem  braddcfn 5826 
Binary relationship form of the AddC function.
(Contributed by SF,
2Mar2015.)

AddC


Theorem  epprc 5827 
The membership relationship is a proper class. This theorem together with
vvex 4109 demonstrates the basic idea behind New
Foundations: since
is not a stratified relationship, then it does
not have a
realization as a set of ordered pairs, but since
is stratified,
then it does have a realization as a set. (Contributed by SF,
20Feb2015.)



Theorem  funsex 5828 
The class of all functions forms a set. (Contributed by SF,
18Feb2015.)

Funs 

Theorem  elfuns 5829 
Membership in the set of all functions. (Contributed by SF,
23Feb2015.)

Funs 

Theorem  elfunsg 5830 
Membership in the set of all functions. (Contributed by Scott Fenton,
31Jul2019.)

Funs 

Theorem  elfunsi 5831 
Membership in the set of all functions implies functionhood. (Contributed
by Scott Fenton, 31Jul2019.)

Funs 

Theorem  fnsex 5832 
The function with domain relationship exists. (Contributed by SF,
23Feb2015.)

Fns 

Theorem  brfns 5833 
Binary relationship form of Fns relationship.
(Contributed by SF,
23Feb2015.)

Fns 

Theorem  pprodeq1 5834 
Equality theorem for parallel product. (Contributed by Scott Fenton,
31Jul2019.)

PProd PProd 

Theorem  pprodeq2 5835 
Equality theorem for parallel product. (Contributed by Scott Fenton,
31Jul2019.)

PProd PProd 

Theorem  qrpprod 5836 
A quadratic relationship over a parallel product. (Contributed by SF,
24Feb2015.)

PProd 

Theorem  pprodexg 5837 
The parallel product of two sets is a set. (Contributed by SF,
24Feb2015.)

PProd 

Theorem  pprodex 5838 
The parallel product of two sets is a set. (Contributed by SF,
24Feb2015.)

PProd 

Theorem  brpprod 5839* 
Binary relationship over a parallel product. (Contributed by SF,
24Feb2015.)

PProd


Theorem  dmpprod 5840 
The domain of a parallel product. (Contributed by SF, 24Feb2015.)

PProd 

Theorem  cnvpprod 5841 
The converse of a parallel product. (Contributed by SF, 24Feb2015.)

PProd PProd 

Theorem  rnpprod 5842 
The range of a parallel product. (Contributed by SF, 24Feb2015.)

PProd 

Theorem  fnpprod 5843 
Functionhood law for parallel product. (Contributed by SF,
24Feb2015.)

PProd 

Theorem  f1opprod 5844 
The parallel product of two bijections is a bijection. (Contributed by
SF, 24Feb2015.)

PProd 

Theorem  ovcross 5845 
The value of the cross product function. (Contributed by SF,
24Feb2015.)

Cross 

Theorem  fncross 5846 
The cross product function is a function over
(Contributed by SF, 24Feb2015.)

Cross 

Theorem  dmcross 5847 
The domain of the cross product function. (Contributed by SF,
24Feb2015.)

Cross 

Theorem  brcrossg 5848 
Binary relationship over the cross product function. (Contributed by SF,
24Feb2015.)

Cross 

Theorem  brcross 5849 
Binary relationship over the cross product function. (Contributed by
SF, 24Feb2015.)

Cross


Theorem  crossex 5850 
The function mapping
and to their cross
product is a set.
(Contributed by SF, 11Feb2015.)

Cross 

Theorem  pw1fnval 5851 
The value of the unit power class function. (Contributed by SF,
25Feb2015.)

Pw1Fn _{1} 

Theorem  pw1fnex 5852 
The unit power class function is a set. (Contributed by SF,
25Feb2015.)

Pw1Fn 

Theorem  fnpw1fn 5853 
Functionhood statement for Pw1Fn (Contributed by
SF, 25Feb2015.)

Pw1Fn
1_{c} 

Theorem  brpw1fn 5854 
Binary relationship form of Pw1Fn (Contributed by
SF,
25Feb2015.)

Pw1Fn _{1} 

Theorem  pw1fnf1o 5855 
Pw1Fn is a onetoone function with domain
1_{c} and range
1_{c}. (Contributed by SF, 26Feb2015.)

Pw1Fn 1_{c}1_{c} 

Theorem  fnfullfunlem1 5856* 
Lemma for fnfullfun 5858. Binary relationship over part one of the
full
function definition. (Contributed by SF, 9Mar2015.)

∼ 

Theorem  fnfullfunlem2 5857 
Lemma for fnfullfun 5858. Part one of the full function operator
yields a
function. (Contributed by SF, 9Mar2015.)

∼ 

Theorem  fnfullfun 5858 
The full function operator yields a function over . (Contributed
by SF, 9Mar2015.)

FullFun 

Theorem  fullfunexg 5859 
The full function of a set is a set. (Contributed by SF, 9Mar2015.)

FullFun 

Theorem  fullfunex 5860 
The full function of a set is a set. (Contributed by SF,
9Mar2015.)

FullFun 

Theorem  fvfullfunlem1 5861* 
Lemma for fvfullfun 5864. Calculate the domain of part one of the
full
function definition. (Contributed by SF, 9Mar2015.)

∼


Theorem  fvfullfunlem2 5862 
Lemma for fvfullfun 5864. Part one of the full function definition is
a
subset of the function. (Contributed by SF, 9Mar2015.)

∼ 

Theorem  fvfullfunlem3 5863 
Lemma for fvfullfun 5864. Part one of the full function definition
agrees
with the set itself over its domain. (Contributed by SF,
9Mar2015.)

∼
∼


Theorem  fvfullfun 5864 
The value of the full function definition agrees with the function value
everywhere. (Contributed by SF, 9Mar2015.)

FullFun 

Theorem  brfullfung 5865 
Binary relationship of the full function operation. (Contributed by SF,
9Mar2015.)

FullFun 

Theorem  brfullfun 5866 
Binary relationship of the full function operation. (Contributed by SF,
9Mar2015.)

FullFun 

Theorem  brfullfunop 5867 
Binary relationship of the full function operation over an ordered
pair. (Contributed by SF, 9Mar2015.)

FullFun


Theorem  fvdomfn 5868 
Calculate the value of the domain function. (Contributed by Scott
Fenton, 9Aug2019.)

Dom 

Theorem  fvranfn 5869 
Calculate the value of the range function. (Contributed by Scott
Fenton, 9Aug2019.)

Ran 

Theorem  domfnex 5870 
The domain function is stratified. (Contributed by Scott Fenton,
9Aug2019.)

Dom 

Theorem  ranfnex 5871 
The range function is stratified. (Contributed by Scott Fenton,
9Aug2019.)

Ran 

2.3.11 Closure operation


Syntax  cclos1 5872 
Extend the definition of a class to include the closure operation.

Clos1 

Definition  dfclos1 5873* 
Define the closure operation. A modified version of the definition from
[Rosser] p. 245. (Contributed by SF,
11Feb2015.)

Clos1 

Theorem  clos1eq1 5874 
Equality law for closure. (Contributed by SF, 11Feb2015.)

Clos1 Clos1 

Theorem  clos1eq2 5875 
Equality law for closure. (Contributed by SF, 11Feb2015.)

Clos1 Clos1 

Theorem  clos1ex 5876 
The closure of a set under a set is a set. (Contributed by SF,
11Feb2015.)

Clos1 

Theorem  clos1exg 5877 
The closure of a set under a set is a set. (Contributed by SF,
11Feb2015.)

Clos1 

Theorem  clos1base 5878 
The initial set of a closure is a subset of the closure. Theorem
IX.5.13 of [Rosser] p. 246. (Contributed
by SF, 13Feb2015.)

Clos1 

Theorem  clos1conn 5879 
If a class is connected to an element of a closure via , then it
is a member of the closure. Theorem IX.5.14 of [Rosser] p. 246.
(Contributed by SF, 13Feb2015.)

Clos1 

Theorem  clos1induct 5880* 
Inductive law for closure. If the base set is a subset of , and
is closed
under , then the
closure is a subset of .
Theorem IX.5.15 of [Rosser] p. 247.
(Contributed by SF,
11Feb2015.)

Clos1


Theorem  clos1is 5881* 
Induction scheme for closures. Hypotheses one through three set up
existence properties, hypothesis four sets up stratification, hypotheses
five through seven set up implicit substitution, and hypotheses eight
and nine set up the base and induction steps. (Contributed by SF,
13Feb2015.)

Clos1


Theorem  clos1basesuc 5882* 
A member of a closure is either in the base set or connected to another
member by .
Theorem IX.5.16 of [Rosser] p. 248.
(Contributed by
SF, 13Feb2015.)

Clos1


Theorem  clos1baseima 5883 
A closure is equal to the base set together with the image of the
closure under . Theorem X.4.37 of [Rosser] p. 303.
(Contributed
by SF, 10Mar2015.)

Clos1 

Theorem  clos1basesucg 5884* 
A member of a closure is either in the base set or connected to another
member by .
Theorem IX.5.16 of [Rosser] p. 248.
(Contributed by
Scott Fenton, 31Jul2019.)

Clos1


Theorem  dfnnc3 5885 
The finite cardinals as expressed via the closure operation. Theorem
X.1.3 of [Rosser] p. 276. (Contributed
by SF, 12Feb2015.)

Nn
Clos1 0_{c}
1_{c} 

Theorem  clos1nrel 5886 
The value of a closure when the base set is not related to anything in
.
(Contributed by SF, 13Mar2015.)

Clos1


Theorem  clos10 5887 
The value of a closure over an empty base set. (Contributed by Scott
Fenton, 31Jul2019.)

Clos1


2.4 Orderings


2.4.1 Basic ordering relationships


Syntax  ctrans 5888 
Extend the definition of a class to include the set of all transitive
relationships.

Trans 

Syntax  cref 5889 
Extend the definition of a class to include the set of all reflexive
relationships.

Ref 

Syntax  cantisym 5890 
Extend the definition of a class to include the set of all antisymmetric
relationships.

Antisym 

Syntax  cpartial 5891 
Extend the definition of a class to include the set of all partial
orderings.

Po 

Syntax  cconnex 5892 
Extend the definition of a class to include the set of all connected
relationships.

Connex 

Syntax  cstrict 5893 
Extend the definition of a class to include the set of all strict linear
orderings.

Or 

Syntax  cfound 5894 
Extend the definition of a class to include the set of all founded
relationships.

Fr 

Syntax  cwe 5895 
Extend the definition of a class to include the set of all wellordered
relationships.

We 

Syntax  cext 5896 
Extend the definition of a class to include the set of all extensional
relationships.

Ext 

Syntax  csym 5897 
Extend the definition of a class to include the symmetric
relationships.

Sym 

Syntax  cer 5898 
Extend the definition of a class to include the equivalence
relationships.

Er 

Definition  dftrans 5899* 
Define the set of all transitive relationships over a base set.
(Contributed by SF, 19Feb2015.)

Trans


Definition  dfref 5900* 
Define the set of all reflexive relationships over a base set.
(Contributed by SF, 19Feb2015.)

Ref
