Type  Label  Description 
Statement 

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

⊢ A ∈ V ⇒ ⊢ ImageA
∈ V 

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

⊢ dom (R
⊗ S) = (dom R ∩ dom S) 

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

⊢ Fun F ⇒ ⊢ ((R
⊗ S) ∘ F) =
((R ∘
F) ⊗ (S ∘ F)) 

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

⊢ ((F Fn
A ∧
G Fn B) → (F
⊗ G) Fn (A ∩ B)) 

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

⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V ⇒ ⊢ (⟨{A}, ⟨{B}, {C}⟩⟩ ∈ SI_{3} R ↔ ⟨A, ⟨B, C⟩⟩ ∈ R) 

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

⊢ A ∈ V ⇒ ⊢ SI_{3} A ∈
V 

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

⊢ T ∈ V
& ⊢ (⟨{y}, T⟩ ∈ R ↔ y
∈ A) ⇒ ⊢ (⟨x, T⟩ ∈ ∼ ((
Ins3 S ⊕
Ins2 R)
“ 1_{c}) ↔ x =
A) 

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

⊢ (⟨{y}, x⟩ ∈ R ↔ y
∈ V) ⇒ ⊢ ((A ×
V) ∩ ^{◡} ∼ (( Ins3 S ⊕ Ins2 R) “
1_{c})) = (x ∈ A ↦ V) 

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

⊢ (⟨{z}, ⟨x, y⟩⟩ ∈ R ↔
z ∈
V) ⇒ ⊢ (((A
× B) × V) ∖ (( Ins2 S ⊕ Ins3 R) “ 1_{c})) = (x ∈ A, y ∈ B ↦ V) 

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

⊢ A ∈ V
& ⊢ R ∈ V ⇒ ⊢ ((A ×
V) ∩ ^{◡} ∼ (( Ins3 S ⊕ Ins2 R) “
1_{c})) ∈ V 

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

⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ R ∈ V ⇒ ⊢ (((A
× B) × V) ∖ (( Ins2 S ⊕ Ins3 R) “ 1_{c})) ∈ V 

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

⊢ ((A ∈ V ∧ B ∈ W) →
(A Cup
B) = (A ∪ B)) 

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

⊢ Cup Fn
V 

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

⊢ ((A ∈ V ∧ B ∈ W) →
(⟨A,
B⟩ Cup C ↔
C = (A
∪ B))) 

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

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (⟨A, B⟩ Cup C ↔ C =
(A ∪ B)) 

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

⊢ Cup ∈ V 

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

⊢ ((A ∈ V ∧ B ∈ W) →
(A Compose
B) = (A ∘ B)) 

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

⊢ Compose Fn
V 

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

⊢ ((A ∈ V ∧ B ∈ W) →
(⟨A,
B⟩ Compose C ↔
(A ∘
B) = C)) 

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

⊢ Compose ∈ V 

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

⊢ ((A ∈ V ∧ B ∈ W) →
(A Disj
B ↔ (A ∩ B) =
∅)) 

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

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (A Disj B ↔
(A ∩ B) = ∅) 

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

⊢ Disj ∈ V 

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

⊢ AddC ∈ V 

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

⊢ AddC Fn
V 

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

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (⟨A, B⟩ AddC C ↔ (A
+_{c} B) = C) 

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

⊢ ¬ E ∈
V 

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

⊢ Funs ∈ V 

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

⊢ F ∈ V ⇒ ⊢ (F ∈ Funs ↔ Fun
F) 

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

⊢ (F ∈ V →
(F ∈
Funs ↔ Fun F)) 

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

⊢ (F ∈ Funs → Fun
F) 

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

⊢ Fns ∈ V 

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

⊢ F ∈ V ⇒ ⊢ (F Fns A ↔
F Fn A) 

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

⊢ (A =
B → PProd (A, C) = PProd (B, C)) 

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

⊢ (A =
B → PProd (C, A) = PProd (C, B)) 

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

⊢ (⟨A, B⟩ PProd (R, S)⟨C, D⟩ ↔
(ARC ∧ BSD)) 

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

⊢ ((A ∈ V ∧ B ∈ W) →
PProd (A,
B) ∈
V) 

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

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ PProd (A, B) ∈ V 

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

⊢ (A PProd (R, S)B ↔
∃x∃y∃z∃w(A = ⟨x, y⟩ ∧ B = ⟨z, w⟩ ∧ (xRz ∧ ySw))) 

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

⊢ dom PProd
(A, B)
= (dom A × dom B) 

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

⊢ ^{◡} PProd (A, B) = PProd (^{◡}A,
^{◡}B) 

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

⊢ ran PProd
(A, B)
= (ran A × ran B) 

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

⊢ ((F Fn
A ∧
G Fn B) → PProd
(F, G)
Fn (A × B)) 

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

⊢ ((F:A–11onto→C ∧ G:B–11onto→D) →
PProd (F,
G):(A
× B)–11onto→(C
× D)) 

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

⊢ ((A ∈ V ∧ B ∈ W) →
(A Cross
B) = (A × B)) 

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

⊢ Cross Fn
V 

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

⊢ dom Cross =
V 

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

⊢ ((A ∈ V ∧ B ∈ W) →
(⟨A,
B⟩ Cross C ↔
C = (A
× B))) 

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

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (⟨A, B⟩ Cross C ↔ C =
(A × B)) 

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

⊢ Cross ∈ V 

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

⊢ A ∈ V ⇒ ⊢ ( Pw1Fn
‘{A}) = ℘_{1}A 

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

⊢ Pw1Fn ∈ V 

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

⊢ Pw1Fn Fn
1_{c} 

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

⊢ A ∈ V ⇒ ⊢ ({A} Pw1Fn B ↔
B = ℘_{1}A) 

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

⊢ Pw1Fn
:1_{c}–11onto→℘1_{c} 

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

⊢ (A(( I
∘ F)
∖ ( ∼ I ∘ F))B ↔ (AFB ∧ ∀x(AFx → x =
B))) 

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

⊢ Fun (( I ∘
F) ∖ (
∼ I ∘ F)) 

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

⊢ FullFun F Fn V 

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

⊢ (F ∈ V →
FullFun F
∈ V) 

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

⊢ F ∈ V ⇒ ⊢ FullFun F ∈
V 

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

⊢ dom (( I ∘
F) ∖ (
∼ I ∘ F)) = {x ∣ ∃!y xFy} 

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

⊢ (( I ∘
F) ∖ (
∼ I ∘ F)) ⊆ F 

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

⊢ (A ∈ dom (( I ∘
F) ∖ (
∼ I ∘ F)) → ((( I ∘ F) ∖ ( ∼ I ∘
F)) ‘A) = (F
‘A)) 

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

⊢ ( FullFun F ‘A) =
(F ‘A) 

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

⊢ (A ∈ V →
(A FullFun
FB
↔ (F ‘A) = B)) 

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

⊢ A ∈ V ⇒ ⊢ (A FullFun FB ↔ (F
‘A) = B) 

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

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (⟨A, B⟩ FullFun FC ↔
(AFB) = C) 

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

⊢ (A ∈ V → (
Dom ‘A)
= dom A) 

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

⊢ (A ∈ V → (
Ran ‘A)
= ran A) 

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

⊢ Dom ∈ V 

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

⊢ Ran ∈ V 

2.3.11 Closure operation


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

class
Clos1 (A, R) 

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

⊢ Clos1 (S, R) = ∩{a ∣ (S ⊆ a ∧ (R “
a) ⊆
a)} 

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

⊢ (S =
T → Clos1
(S, R) = Clos1 (T, R)) 

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

⊢ (R =
T → Clos1
(S, R) = Clos1 (S, T)) 

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

⊢ S ∈ V
& ⊢ R ∈ V ⇒ ⊢ Clos1 (S, R) ∈ V 

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

⊢ ((S ∈ V ∧ R ∈ W) →
Clos1 (S,
R) ∈
V) 

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

⊢ C = Clos1 (S, R) ⇒ ⊢ S ⊆ C 

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

⊢ C = Clos1 (S, R) ⇒ ⊢ ((A ∈ C ∧ ARB) →
B ∈
C) 

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

⊢ S ∈ V
& ⊢ R ∈ V
& ⊢ C = Clos1 (S, R) ⇒ ⊢ ((X ∈ V ∧ S ⊆ X ∧ ∀x ∈ C ∀z((x ∈ X ∧ xRz) →
z ∈
X)) → C ⊆ X) 

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

⊢ S ∈ V
& ⊢ R ∈ V
& ⊢ C = Clos1 (S, R)
& ⊢ {x ∣ φ}
∈ V
& ⊢ (x =
y → (φ ↔ ψ))
& ⊢ (x =
z → (φ ↔ χ))
& ⊢ (x =
A → (φ ↔ θ))
& ⊢ (x ∈ S →
φ)
& ⊢ ((y ∈ C ∧ yRz ∧ ψ) →
χ) ⇒ ⊢ (A ∈ C →
θ) 

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

⊢ S ∈ V
& ⊢ R ∈ V
& ⊢ C = Clos1 (S, R) ⇒ ⊢ (A ∈ C ↔
(A ∈
S ∨ ∃x ∈ C xRA)) 

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

⊢ S ∈ V
& ⊢ R ∈ V
& ⊢ C = Clos1 (S, R) ⇒ ⊢ C =
(S ∪ (R “ C)) 

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

⊢ C = Clos1 (S, R) ⇒ ⊢ ((S ∈ V ∧ R ∈ W) →
(A ∈
C ↔ (A ∈ S ∨ ∃x ∈ C xRA))) 

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}}, (x ∈ V ↦ (x
+_{c} 1_{c}))) 

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

⊢ S ∈ V
& ⊢ R ∈ V
& ⊢ C = Clos1 (S, R) ⇒ ⊢ ((R “
S) = ∅
→ C = S) 

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

⊢ R ∈ V
& ⊢ C = Clos1 (∅, R) ⇒ ⊢ C = ∅ 

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.

class
Trans 

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

class
Ref 

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

class
Antisym 

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

class
Po 

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

class
Connex 

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

class
Or 

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

class
Fr 

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

class
We 

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

class
Ext 

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

class
Sym 

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

class
Er 

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

⊢ Trans = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) →
xrz)} 

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

⊢ Ref = {⟨r, a⟩ ∣ ∀x ∈ a xrx} 