2. Set theory (continued)
Having introduced
both set theory and model theory in the first part, we continue
developing set theory in second part.
2.1. Tuples, families
Tuples
Formalization of operations and currying
The notion of nary operation, objects acting as nary
operators between n sets, would be formalized by:
 n domain functors (of little practical use);
 an (n+1)ary operator of evaluation (evaluator) written in filled form as
f(x_{1},…,x_{n}),
with arguments an nary operation f and its
n arguments x_{1},…,x_{n};
 an operation definer, binding n variables to their respective
ranges on a term.
The notion of operation can be represented as a class of functions,
in the following way called currying. The role of operation
definer (binding n variables) is played by the succession of
n uses of the function definer (one for each bound variable);
and similarly as an evaluator, n uses of the function
evaluator. For example (n=2), the binary operation f
defined by the term (binary predicate) t with arguments x
in E and y in F, may be formalized by
f ≈ (E ∋ x ↦
(F ∋ y ↦ t(x,y))) = g
f(x,y) = g(x)(y) = t(x,y)
The intermediate function g(x) = (F ∋ y
↦ t(x,y)) with argument y, sees x
as fixed and y as bound. But this breaks the symmetry between
arguments, and loses the data of F when E is empty but not the
other way round. A
formalization without these flaws will be possible using tuples
(2.1.).
The formalization of nary relations involves an (n+1)ary
predicate of evaluation, and a definer binding n variables
on a formula. We may either see nary relations as
particular cases of nary operations (representing
Booleans as objects), or see nary operations as
particular cases of (n+1)ary relations (see 2.3). And just
like operations, relations can be reduced to the unary case in 2
ways : by currying (with n−1 uses of the function definer
and 1 use of the setbuilder, as will be done in 2.3 with n=2),
or using tuples (2.1).
Tuples
A tuple (or ntuple, for any natural number n) is an
interpretation of a list of (n) variables. It is thus a metafunction
from a finite metaset, to the universe. Tuples of a given kind (list of
variables with their types) can be added to any theory as a new type
of objects. Variables of this type play the role of abbreviations of packs
of n variables with old types (copies of the given list) x
= (x_{0},…, x_{n−1}).
In practice, the domain of considered ntuples will be the
(meta)set V_{n} of n
digits from 0 to n−1. Set theory can represent its own ntuples
as functions, figuring V_{n}
as a set of objects all named by constants. A 2tuple is called an oriented
pair, a 3tuple is a triple, a 4tuple is a quadruple...
The ntuple definer is not a binder but an nary
operator, placing its n arguments in a parenthesis and
separated by commas: ( ,…, ). The evaluator appears,
curried by fixing the metaargument, as a list of n functors
called projections: for each i∈V_{n}, the ith
projection π_{i} gives the value π_{i}(x)
= x_{i} of each tuple
x=(x_{0},…,x_{n−1})
at i (value of the ith variable inside x).
They are subject to the following axioms (where the first sums up
the next ones) : for any x_{0},…, x_{n−1}
and any ntuple x,
x = (x_{0},…,x_{n−1})
⇔ (π_{0}(x)=x_{0} ∧ …
∧ π_{n−1}(x)=x_{n−1})
x_{i}= π_{i}((x_{0},…,
x_{n−1})) for each i
∈ V_{n}
x = (π_{0}(x),…, π_{n−1}(x))
Oriented pairs suffice to build a representation of tuples of any
arity n > 2, in the sense that we can define operators to
play the roles of definer and projections, satisfying the same
axioms. For example, triples t = (x,y,z)
can be defined as t = ((x,y),z)) and
evaluated by x = π_{0}(π_{0}(t)),
y=π_{1}(π_{0}(t)),
z=π_{1}(t).
Conditional connective
The 3ary connective «If A then B otherwise C», is written as
follows (applying (C,B) to A ∈ V_{2}): (A ? B : C) ⇔
(¬C⇒A⇒B) ⇔ ((A⇒B)∧(¬A⇒C))
⇔ (¬A ? C : B) ⇔ (C,B)(A)
⇔ ((A∧B)∨(¬A∧C)) ⇔
((C⇒A)⇒(A∧B))
⇎ (A ? ¬B : ¬C)
Any n+1ary connective K amounts to two nary
ones: K(A) ⇔ (A ? K(1): K(0)).
Thus, ¬A ⇔ (A ? 0 : 1)
(A⇒B) ⇔ (A
? B : 1)
(A∨B) ⇔ (A ? 1: B)
(A ⇔ B) ⇔ (A ? B : ¬B).
Families
A family is a function intuitively seen as a generalized
tuple: its domain (a set) is seen as simple, fixed, outside the main
studied system, as if it was a set of metaobjects. A «family of...
» is a family whose image is a «set of... » (included in the range of
these things).
Families use the formalism of functions disguised in the style of
tuples (whose tools cannot apply due to the finiteness of symbols).
The evaluator (evaluating u at i), instead of u(i)
or π_{i}(u), is written u_{i}
(looking like a metavariable symbol of variable). A family defined
by a term t, is written (t(i))_{i∈I}
instead of (I ∋ i ↦ t(i)) or
(t(0),…,t(n−1)).
The argument i is called index, and the family is
said indexed by its domain I.
As we described the content
of a theory, a "list" basically means a family. But more precisely:
 The list of types is best seen as a set of pure elements, usable as indexing
set of possible families
 The list of symbols can be formalized as a family of tuples
of types
 Of the list of axioms, only its image matters, which is a subset of the set of all
expressible statements.
Structures and binders
Each nary structure can be seen as a unary structure with
domain a class of ntuples, like a binder can be seen as a
unary structure on a class of functions or subsets of a given set:
binders are the generalization of structures when families replace tuples.
In particular, ∀ and ∃ generalize the chains of
conjunctions and disjunctions: (B_{0}∧…∧B_{n−1}) ⇔
(∀i∈V_{n}, B_{i}).
The equality condition between ordered pairs,
(x,y)=(z,t) ⇔ (x=z
∧ y=t), is similar to the one for functions.
Let R a unary predicate definite on E, and C
a boolean. We have distributivities
(C ∧ ∃x∈E, R(x))
⇔ (∃x∈E, C ∧ R(x))
(C ∨ ∀x∈E, R(x))
⇔ (∀x∈E, C ∨ R(x))
(C ⇒ ∀x∈E, R(x)) ⇔ (∀x∈E,
C ⇒ R(x))
((∃x∈E, R(x)) ⇒ C) ⇔
(∀x∈E, R(x) ⇒ C)
(∃x∈E, C) ⇔ (C ∧ E≠∅) ⇒
C ⇒ (C ∨ E=∅) ⇔ (∀x∈E, C)
Extensional definitions of sets
The functor Im defines the binder
{T(x) x∈E} =
{T(x)}_{x∈E} = Im(E ∋ x
↦ T(x))
As this notation looks similar to the set builder, we can combine both :
{T(x) x∈E ∧ R(x)}
= {T(x) x∈{y∈ER(y)}}
Applying Im to tuples, defines the
operator symbols of exensional definition of sets (listing
their elements): Im(a,b,…) = {a,b,…}.
Those of arity 0,1,2 were presented in
1.11: the empty set ∅, the singleton {a} and the
pairing {a,b}. We defined V_{n}
as {0,…,n−1}. Images of tuples are finite sets.
2.2. Boolean operators on sets
Union of a family of sets
For any family of unary predicates A_{i} with
index i ∈ I, all definite in (at least) a common
class C, their application to the same variable x
with range C reduces this to a family of Boolean variables
depending on x (their parameter, see 1.5). This way, any
operation Q on these variables (a quantifier with range I,
which becomes a connective when I is finite) defines a
metaoperation between unary predicates, with result a unary
predicate ℛ, defined for x in C as Qi, A_{i}(x).
When C is a set E, this operates between subsets of
E (through ∈ and the set builder).
For example, the existential quantifier (Q = ∃) defines the
union of a family of sets:
x ∈ ⋃
i∈I
F_{i} ⇔ ∃i∈I, x∈F_{i}
This class is a set independent of E, as it can also be
defined from the union of a set of sets (1.11):
⋃
i∈I
F_{i} = ⋃{F_{i}
 i ∈ I}
(∀x∈⋃
i∈I
F_{i}, B(x))
⇔ ∀i∈I, ∀x∈F_{i},
B(x)
x ∈ X∪Y
⇔ (x ∈ X ∨ x ∈ Y)
X ⊂ X∪Y = Y∪X
All extensional definition operators (except ∅) are definable from
pairing and binary union.
Intersection
Any family of sets (F_{i})_{i∈I}
can be seen as a family of subsets of any set E that includes their
union U = ⋃_{i∈I} F_{i} ⊂ E. Then
for any operation (quantifier) Q between Booleans indexed by
I, the predicate ℛ(x) defined as (Qi, x
∈ F_{i}) takes value (Qi, 0) for all x
∉ U. Thus Q needs to satisfy ¬(Qi,0) (to be
false when all entries are false) for the class ℛ to be a set
{x∈E ℛ(x)} = {x∈U ℛ(x)}. This
was the case for Q=∃, including on the empty family (⋃∅ =∅),
but for ∀ (that defines the intersection) it requires a nonempty
family of sets (I ≠ ∅):
∀j ∈ I, ∩
i∈I F_{i} =
{x∈F_{j}  ∀i∈I,
x∈F_{i}}
x ∈ ∩
i∈I
F_{i} ⇔ ∀i∈I, x
∈ F_{i}
x ∈ X⋂Y ⇔ (x∈X ∧ x∈Y)
X⋂Y = Y⋂X = {x∈X  x∈Y} ⊂ X
X = X∪Y ⇔ Y ⊂ X ⇔ Y
= X⋂Y
Two sets A and B are called disjoint when A⋂B=∅,
which is equivalent to ∀x∈A, x∉B.
Union and intersection have the same associativity and
distributivity properties as ∧ and ∨ : A∪B∪C = (A∪B)∪C
= A∪(B∪C) = ⋃{A,B,C}
(

⋃
i∈I 
A_{i})∩C
=

⋃
i∈I 
(A_{i}∩C) 
(

∩
i∈I 
A_{i})∪C
= 
∩
i∈I 
(A_{i}∪C) 
(A∪B)⋂C
= 
(A⋂C)∪(B⋂C)

(A⋂B)∪C
= 
(A∪C)⋂(B∪C)

Other operators
The difference is defined by A\B = {x∈A
x ∉ B} so that x ∈ A\B ⇔ x∈A
∧ x∉B.
Finally the connective ⇎ gives the symmetric difference: A∆B
= (A∪B)\(A∩B).
When (Qi,0) is true, we must choose a set E to define
operations between subsets of E:
∩
i∈I
F_{i} = ⋂{F_{i}
 i∈I} = {x∈E
 ∀i∈I, x ∈ F_{i}} =
∁_{E} ⋃
i∈I
∁_{E} F_{i}
2.3. Products, graphs and composition
Finite product
For any two sets E and F, the product E×F
is the set of (x,y) where x∈E and y∈F.
Similarly, the product of n sets E_{0}×…×E_{n−1}
is the set of ntuples (x_{0},…,x_{n−1})
where ∀i∈V_{n},
x_{i}∈E_{i}.
An nary operation is a function with domain a product of n
sets.
A relation between any two sets E and F is
formalized as a set of oriented pairs G ⊂ E×F
(the domains E and F might be specified by taking
the triple (E,F,G)). A set of oriented pairs
(such as G) is called a graph.
For any binder Q and any graph G, the formula Qx∈G,
A(x_{0},x_{1})
that binds x = (x_{0}, x_{1})
on a binary structure A with domain G, can be seen
as binding 2 variables x_{0}, x_{1}
on A(x_{0}, x_{1}), and thus
be denoted with an oriented pair of variables:
Q(y,z)∈G, A(y,z).
The existence of the product (in all arity) is justified by the set
generation principle:
(∃(x,y)∈E×F, A(x,y))
⇔ (∃x∈E, ∃y∈F, A(x,y))
⇔ (∃y∈F, ∃x∈E, A(x,y))
(∀(x,y)∈E×F, A(x,y))
⇔ (∀x∈E, ∀y∈F, A(x,y))
⇔ (∀y∈F, ∀x∈E, A(x,y))
Quantifiers Q(x,y)∈E×E will be
written Qx,y∈E, and those with domain {(x,y)∈E×E  x≠y} will be written
Qx≠y∈E.
Thus ∀x≠y∈E,... means ∀x,y∈E, x≠y⇒...,
that is ∀x∈E,∀y∈E, x≠y⇒...
With F=V_{2},
(∃x∈E, A(x)∨B(x))
⇔ ((∃x∈E, A(x)) ∨ (∃x∈E, B(x)))
(∀x∈E, A(x)∧B(x))
⇔ ((∀x∈E, A(x)) ∧ (∀x∈E, B(x)))
(∃x∈E, C∨A(x)) ⇔ ((C ∧ E≠∅) ∨ ∃x∈E, A(x))
(∀x∈E, C∧A(x)) ⇔
((C ∨ E=∅) ∧ ∀x∈E, A(x))
Sum or disjoint union
The transpose of an ordered pair is ^{t}(x,y)
= (y,x)
That of a graph R is ^{t}R =
{(y,x)(x,y) ∈ R}
Graphs can be expressed in curried forms ⃗R
and ⃖R :
y ∈ ⃗R (x) ⇔ (x,y)
∈ R ⇔ x ∈ ⃖R
(y) = ^{t}⃗R (y)
justified by defining the functor ⃗R
as
⃗R(x) = {y
 (z,y)∈R ∧ z=x}.
Inversely, any family of sets
(E_{i})_{I∈I} defines a
graph called their sum (or disjoint union)
∐_{i∈I} E_{i}:
(i∈I ∧ x∈E_{i})
⇔ (i,x) ∈ ∐
i∈I
E_{i} = ⋃
i∈I
{i}×E_{i} = ⋃
i∈I {(i,x)  x
∈ E_{i}} ⊂ I×⋃
i∈I
E_{i}
(∀
x∈∐
_{i∈I} E_{i},
A(
x)) ⇔ (∀
i∈
I,
∀
y∈
E_{i},
A(
i,
y))
E_{0}⊔…⊔
E_{n−1} =
∐
_{i∈Vn} E_{i}
E×
F = ∐
_{x∈E} F
E×∅ = ∅ = ∅×
E
(
E⊂
E′ ∧
F⊂
F′) ⇒
E×
F ⊂
E′×
F′
(∀
i∈
I,
E_{i} ⊂
E′
_{i})
⇔ ∐
_{i∈I} E_{i} ⊂
∐
_{i∈I} E′
_{i}
Composition, restriction, graph of a function
For any set E, the function identity on E is
defined by Id_{E} = (E
∋ x ↦ x).
For any functions f,g with Im f
⊂ Dom g (namely, f : E →
F and g : F → G), their composite
is
g০f = ((Dom f) ∋ x ↦
g(f(x))): E → G
The same with h : G →H, h০g০f
= (h০g)০f = h০(g০f) = (E
∋ x ↦ h(g(f(x)))) and so on.
The restriction of f to A ⊂ Dom f is f_{A} =
(A ∋ x ↦ f(x)) = f০Id_{A}.
The graph of a function f is defined by
Gr f = {(x,f(x)) 
x ∈ Dom f} = ∐_{x∈Dom f}
{f(x)}
(x,y) ∈ Gr f ⇔ (x ∈ Dom f
∧ y = f(x))
We can define domains, images and restrictions for graphs,
generalizing those for functions (i.e. Dom f
= Dom(Gr f), Im f = Im(Gr f) and Gr(f_{A})
= (Gr f)_{A}):
Dom R = {x(x,y) ∈ R} =
Im ^{t}R
∀x, x ∈ Dom R ⇔ ⃗R
(x) ≠ ∅
R ⊂ E×F ⇔ (Dom R ⊂ E ∧ Im R
⊂ F)
R_{A} = R∩(A× Im R) =
{(x,y)∈R  x∈A} = ∐_{x∈A}
⃗R(x)
Then we have R = ∐_{i∈I} E_{i}
⇔ (Dom R ⊂ I ∧ ∀i∈I,
⃗R(i)=E_{i})
⇒ Im R = ⋃_{i∈I}
E_{i}.
For any functions f,g, any graph R, and E = Dom f,
Gr f
⊂ R 
⇔ ∀x∈E, f(x) ∈ ⃗R(x) 
R ⊂ Gr f

⇔ (∀(x,y) ∈ R, x∈E
∧ y=f(x)) ⇔ (Dom R ⊂
E ∧ ∀(x,y)∈R, y = f(x)) 
Gr f ⊂ Gr g 
⇔ ((E ⊂ Dom g) ∧ f = g_{E}) 
Direct image, inverse image
The direct image of a set A by a graph R is
R_{∗}(A) = Im R_{A} =
⋃_{x∈A} ⃗R(x).
Dom
R ⊂
A ⇔
R_{A} =
R
⇒
R_{∗}(
A) = Im
R
R_{∗}(⋃
i ∈ I
A_{i}) = ⋃
i ∈ I
R_{∗}(A_{i})
R_{∗}(∩
i ∈ I
A_{i}) ⊂ ∩
i ∈ I
R_{∗}(A_{i})
A ⊂
B ⇒
R_{∗}(
A) ⊂
R_{∗}(
B)
The direct image of A ⊂ Dom f by a function f is
f[A] = f_{∗}(A)
= (Gr f)_{∗}(A) = Im(f_{A})
= {f(x)  x∈A} ⊂ Im f
For any f : E → F and B ⊂ F,
the inverse image or preimage of B by f, written f*(B),
is defined by
f*(B)=
(^{t}Gr f)_{∗}(B) = {x∈E  f(x) ∈ B} = ⋃
y∈B
f^{ •}(y)
f^{ •}(y)= ( ⃖Gr f)(y)
= f*({y}) = {x∈E  f(x)
= y}
f*(∁
_{F} B) = ∁
_{E}f*(
B)
For any family (B_{i})_{i ∈ I}
of subsets of F, f*(∩_{i∈I
}B_{i}) = ∩_{i∈I}
f*(B_{i}) where
intersections are respectively interpreted as subsets of F
and E.
2.4. Uniqueness quantifiers, functional graphs
For all sets F ⊂ E, all unary predicate A
definite on E, and all x ∈ E,
x ∈ F 
⇔ {x} ⊂ F ⇔ (∃y∈E, x=y
∧ y∈F) ⇔ (∀y∈E, x=y ⇒ y∈F) 
x ∈ F 
⇒ ((∀y∈F, A(y)) ⇒ A(x) ⇒
∃y∈F, A(y)) 
F ⊂ {x} 
⇔ (∀y∈F, x=y)
⇒ ((∃y∈F, A(y)) ⇒ A(x) ⇒
(∀y∈F, A(y))) 
F={x} 
⇔ (x∈F ∧ ∀y∈F,
x=y) ⇔ (∀y∈E, y∈F ⇔ x=y) 
Here are 3 new quantifiers: ∃2 (plurality), ! (uniqueness), and ∃!
(existence and uniqueness), whose results when applied to A
in E only depend on F={x∈E  A(x)}
(like ∃ and unlike ∀) :
(∃x∈E,
A(x)) ⇔ (F ≠ ∅) 
⇔ (∃x∈F,
1) ⇔ (∃x∈E, {x} ⊂ F) 
(∃2x∈E,
A(x)) ⇔ (∃2: F) 
⇔ (∃x,y∈F,
x ≠ y) ⇔ (∃x≠y∈E, A(x) ∧
A(y)) 
(!x∈E,
A(x)) ⇔ (!:F) 
⇔ ¬(∃2: F) ⇔
(∀x,y∈F, x=y) ⇔ ∀x∈F,
F ⊂ {x} 
(∃!x∈E,
A(x)) ⇔ (∃!:F) 
⇔ (∃x∈F, F⊂{x})
⇔ (∃x∈E, F={x}) 
F ⊂ {x} 
⇒ (∀y∈F, F⊂{y}) ⇔ (!:F) 
(∃!:F) 
⇔ (F≠∅ ∧ !: F) 
F≠∅ 
⇒ ((∀y∈F, B(y))
⇒ (∃y∈F, B(y))) 
( !: F) 
⇒ ((∃y∈F, B(y))
⇒ (∀y∈F, B(y))) 
F={x} 
⇒ ((∃y∈F, B(y))
⇔ B(x) ⇔ ∀y∈F, B(y)) 
A function f is said constant when !: Im f. The constancy of a tuple is the
chain of equalities:
x=y=z ⇔ !:{x,y,z}
⇔ ((x=y)∧(y=z)) ⇒ x=z
Translating operators into predicates
In a generic theory, any functor symbol T can be replaced by
a binary predicate symbol R (where
x R y ⇔ (y=T(x)))
with the axiom ∀x,∃!y, x R y,
replacing any formula A(T(x)) (where x
is a term) by (∃y, xRy ∧ A(y)),
or by (∀y, xRy ⇒ A(y))
(while terms cannot be translated). This way, any predicate R
such that ∀x,∃! y, x R y
implicitly defines an operator symbol T. We can extend this
to other arities by replacing x by a tuple.
But the use of open quantifiers in this construction makes it
unacceptable in our set theory. Instead, let us introduce a new
operator ϵ on the class (Set(E) ∧ ∃!:E)
of singletons, giving their element according to the axiom (∀x)
ϵ{x}=x, or equivalently (Set E ∧
∃!:E) ⇒ ϵE ∈ E. Then for every unary predicate
A and every singleton E, A(ϵE) ⇔ (∃x∈E,
A(x)) ⇔ (∀x∈E, A(x)).
Conditional operator
Like the conditional connective, it
chooses between two objects x,y depending on the boolean B:
(B ? x : y) = (y,x)_{B}
= ϵ{z∈{x,y} B ? z=x :
z=y}
so that for any predicate A we have A(B ? x : y) ⇔
(B ? A(x) : A(y)). All paraoperators other
than connectives but with at least a Boolean argument, are naturally
expressed as composed of the conditional operator with operators, or
the conditional connective with predicates, which is why they did
not need an explicit presence in the language of a theory.
Functional graphs
A graph R is said functional if ∀x ∈ Dom R, !: ⃗R(x),
or equivalently ∀x,y∈R, x_{0}=y_{0} ⇒
x_{1}=y_{1}.
This is the condition for it to be the graph of a function. Namely,
R = Gr(ϵ⃗R)
where
ϵ⃗R = ((Dom R)
∋ x ↦ ϵ(⃗R(x)))
2.5. The powerset
Let us extend set theory by 3 new symbols (powerset, exponentiation,
product) with axioms, that will declare given classes C to
be sets K. These extensions are similar to those provided by
the set generation principle (1.11), but no more satisfy its
requirement.
In the traditional ZF formalization of set theory only accepting ∈
as primitive stucture, such a declaration is done purely by the
axiom (or theorem) (∀ parameters), ∃K, ∀x, x ∈
K ⇔ C(x). Then, the operator symbol K
taking the parameters of C as its arguments, represents the
following abbreviations: ∀x∈K means ∀x, C(x)⇒
; the equality X=K means (∀x,
x ∈ X ⇔ C(x)),
and any other A(K) means
∃X, (X=K)∧A(X).
But these formulas use open quantifiers, forbidden in our framework.
For what the set generation principle justified, ∀_{C}
could be replaced by formulas, while the above ∃X could be
treated by existential elimination (1.9). But otherwise without open
quantifiers, even a given set K identical to a class C,
would not be recognizable as such, so that the very statement that C
coincides with a set remains practically meaningless.
Thus, our set theoretical framework requires the operator symbol K
to be regarded as primitive in the language (instead of a defined
abbreviation), with argument the tuple y of parameters of C,
and the axiom
(∀y…), Set(K(y))∧(∀x,
x ∈ K(y) ⇔ C_{y}(x))
Powerset. ∀_{Set} E, Set(℘(E))
∧ (∀F, F∈℘(E) ⇔ (Set(F) ∧ F
⊂ E)).
We shall also shorten ∈ ℘ into ⊂ in binders: (∀A⊂E,…) ⇔ (∀A∈℘(E),…).
Exponentiation. ∀_{Set} E,F,
Set(F^{E})∧(∀f, f ∈ F^{E} ⇔
f : E → F).
Product of a family of sets. This binder
generalizes the finite product operators (2.3):
∀x, x ∈ ∏
i∈I E_{i}
⇔ (Fnc(x) ∧ Dom x = I ∧ ∀i∈I,
x_{i} ∈ E_{i}).
For all i ∈ I, the ith projection is
the function π_{i} from ∏_{j∈I}
E_{j} to E_{i}
evaluating every family x at i : π_{i}(x)=x_{i}.
This is the function evaluator curried in the unnatural order.
These operators are «equivalent» in the sense that they are
definable from each other:
℘(E)={f^{•}(1)  f
∈ V_{2}^{E}}
F^{E}= ∏_{x∈E} F =
{(ϵ
⃗R(x))_{x∈E}
 R ⊂ E×F ∧ ∀x∈E, ∃!: ⃗R(x)}
{x ∈ (⋃
i∈I E_{i})^{I}∀i∈I,
x_{i} ∈ E_{i}} =
{(ϵ ⃗R(i))_{i∈I}
 R ⊂ ∐
i∈I
E_{i} ∧ ∀x∈E, ∃!: ⃗R(x)}
Even some cases are expressible from previous tools:
F^{{a}}= {{a}∋x↦y
 y ∈ F}
F^{∅}= {∅}
℘({a}) = {∅,{a}}
∏
i∈I∪J
E_{i}={(i∈I ? x_{i}
: y_{i})_{i∈I∪J}
 (x,y) ∈ ∏
i∈IE_{i} × ∏
i∈JE_{i}}
(∃i∈I, E_{i}=∅) ⇒ ∏
i∈IE_{i} =∅
(∀i∈I, ∃!:E_{i}) ⇒ ∏
i∈IE_{i}
= {(ϵE_{i})_{i∈ I}}
If F ⊂ F′ then ℘(F) ⊂ ℘(F′), F^{E}
⊂ F′^{E}, and (∀i∈I, E_{i}
⊂ E′_{i}) ⇒ ∏_{i∈I} E_{i}
⊂ ∏_{i∈I} E′_{i} .
Cantor's Theorem. ∀_{Set}
E, ∀_{Fnc} f, Dom f = E ⇒ ℘(E) ⊄ Im f.
Proof: F = {x∈E x ∉ f(x)}
⇒ (∀x∈E, x ∈ F ⇎ x ∈ f(x))
⇒ (∀x∈E, F ≠ f(x)) ⇒ F
∉ Im f.∎
(Russell's
paradox may be seen as a particular case)
2.6. Injectivity and inversion
A function f : E → F is called injective
(or : an injection ), which we write Inj f or f : E ↪ F, if
^{t}Gr f is a functional graph:
Inj f ⇔

(∀y∈F, !:f^{•}(y)) 
⇔ 
(∀x,x′∈E, f(x)=f(x′)
⇒ x=x′) 
⇔ 
(∀x≠x′∈E, f(x) ≠ f(x′)) 
Then its inverse is defined by f^{ 1} = ϵf^{•}
= (Imf ∋ y ↦ ϵf^{•}(y))
so that Gr(f^{ 1}) = ^{t}Gr f.
A function f : E → F is said bijective
(or a bijection) from E onto F, and we write
f : E ↔ F, if it is injective and surjective:
∀y ∈ F, ∃!: f^{•}(y), in which
case f^{ 1}: F ↔ E.
Proposition. Let f : E → F and g : F →
G.
1. (Inj f ∧ Inj g) ⇒ Inj(g০f)
2. Inj(g০f) ⇒ Inj f
3. Im(g০f) = g[Im f] ⊂ Im g.
4. Im(g০f) = G ⇒ Im g = G.
5. Im f = F ⇒ Im(g০f) = Im g,
so that ((f:E ↠ F) ∧ (g:F
↠ G)) ⇒ (g০f:E ↠ G)
Proofs:
1. (Inj f ∧ Inj g) ⇒ ∀x,y∈E,
g(f(x)) = g(f(y)) ⇒
f(x) = f(y) ⇒ x = y.
2. ∀x,y ∈ E, f(x) = f(y)
⇒ g(f(x)) = (g(f(y)) ⇒
x = y.
3. ∀z∈G, z ∈ Im(g০f) ⇔
(∃x∈E, g(f(x))=z) ⇔
(∃y∈ Imf, g(y)=z) ⇔ z
∈ g[Imf].
3.⇒ 4. and 3.⇒5. are obvious.∎
Proposition. For any sets E,F,G
and any f ∈ F^{E},
Im f = F 
⇒ Inj(G^{F} ∋ g ↦ g০f)
⇒ (Im f = F ∨ !:G)

(Inj f ∧ G ≠ ∅) 
⇒ {g০f 
g∈G^{F}} = G^{E}
⇒ (Inj f ∨ !: G) 
(E ⊂ F ∧
G ≠ ∅) 
⇒ {g_{E} 
g∈G^{F}} = G^{E} 
(Inj f ∧ E ≠ ∅) 
⇒ ∃g∈E^{F},
g০f = Id_{E} 
Proofs :
Im f = F ⇒ ∀g,h∈G^{F},
((∀x∈E, g(f(x)) = h(f(x)))
⇔ (∀y∈F, g(y) = h(y) ⇔ g=h)).
∀z,z′∈G, (y ↦ z)০f = (y
↦ (y ∈ Im f ? z : z′))০f
∴ (Inj(g ↦ g০f) ⇒
(z=z′ ∨ Im f=F))
∀z∈G,∀h∈G^{E}, Inj f
⇒ (F ∋ y ↦ (y ∈ Im f ?
h০f^{1}(y):z))০f=h.
∀z,z′∈G, ∀x∈E, ∀g∈G^{F},
g০f = (E∋y↦
(y=x ? z : z′)) ⇒ ∀y∈E, f(y) = f(x) ⇒ g(f(y))
= g(f(x)) = z ⇒ (y=x ∨ z=z′).
The last formulas are particular cases of the second one.∎
Let f : E → F and f*_{F}:
℘(F) → ℘(E) defined by f*.
Then (by G=V_{2} and ∀B
⊂ Imf, f[f*(B)]=B),
Inj f ⇔ Im f*_{F}
= ℘(E)
Im f = F ⇔ Inj f*_{F}
Im f_{∗} = {f[A]A ⊂ E} = ℘(Im
f)
Proposition. Let F = Dom g. Then Inj g ⇒
Inj(F^{E}
∋ f ↦ g০f) ⇒ (Inj g ∨ E=∅).
Proofs: ∀f,f′∈F^{E}, (Inj g ∧
∀x∈E, g(f(x)) = g(f′(x)))
⇒ (∀x∈E, f(x)=f'(x)).
Then from the middle formula, ∀y,z∈F,
g(y) = g(z) ⇒ g০(E ∋ x
↦ y) = g০(E ∋ x ↦ z) ⇒ (∀x∈E,
y=z) ⇒ (y=z ∨ E=∅).∎
Proposition. Let f: E → F
and Dom g=F.
Then
g০f
= Id_{E} 
⇔ (∀x∈E, ∀y∈F,
f(x)=y ⇒ g(y)=x)


⇔ (Gr f ⊂ ^{t}Gr
g) ⇔ (∀y∈F, f^{•}(y)⊂{g(y)}) 

⇔ (∀x∈E, f(x)∈g^{•}(x))
⇔ (Inj f ∧ g_{Imf} = f^{1}) 

⇒ E ⊂ Im g 
(g:F
→E ∧ g০f= Id_{E}) 
⇒ (Im f = F ⇔
Inj g ⇔ f০g = Id_{F} ⇔ g=f^{ 1}). 
Proof of the last formula: (Inj g
∧ g০f০g = g০Id_{F})
⇒ f০g=Id_{F}.
∎
Proposition. 1) If f,g are injective and Im f = Dom g,
then (g০f)^{1} = f^{ 1}০g^{1}.
2) If f,h : E→F and g : F→E then
(g০f = Id_{E} ∧ h০g = Id_{F})
⇔ ((g:F↔E) ∧ f=h=g^{−1}).
Proofs:
1) ∀x∈ Dom f, ∀y∈ Im g, (g০f)(x)=y
⇔ f(x)=g^{1}(y) ⇔ x=
(f^{ 1}০g^{1})(y).
Other method: (g০f)^{1}= (g০f)^{1}০g০g^{1}=
(g০f)^{1}০g০f০f^{ 1}০g^{1}
= f^{ 1}০g^{1}.
2) We deduce f=h from f = h০g০f
= h, or from Gr f ⊂ ^{t}Gr g
⊂ Gr h. The rest is obvious.∎
2.7. Binary relations, ordered sets
A binary relation on E is a graph R ⊂ E×E.
Denoting x R y ⇔ (x,y)
∈ R and letting the domain E of quantifiers
implicit, it will be said
reflexive ⇔ 
∀x, xRx 
irreflexive ⇔ 
∀x, ¬(xRx) 
symmetric ⇔ 
R ⊂ ^{t}R
⇔ R = ^{t}R ⇔ ⃗R
= ⃖R 
antisymmetric ⇔ 
∀x,y, (xRy ∧
yRx) ⇒ x=y 
transitive ⇔ 
∀x,y,z, (xRy
∧ yRz) ⇒ xRz 
For any transitive binary relation R we denote x R y R z ⇔ ((x R y)∧(y R z))⇒x R z.
Example. Let A ⊂ E^{E} and R = ⋃_{f∈A}
Gr f. Then
(Id_{E}
∈ A) ⇒ 
R is reflexive 
(∀f,g ∈ A, g০f
∈ A) ⇒ 
R is transitive 
(∀f∈A, f:E↔
E ∧ f^{−1}∈A) ⇒ 
R is symmetric 
Preorder. A preorder R on a set E
is a reflexive and transitive binary relation on E.
Equivalently,
∀x,y ∈ E, x R y ⇔
⃖R(x) ⊂ ⃖R(y)
Proof: ∀x,y ∈ E, x ∈ ⃖R(x)
⊂ ⃖R(y) ⇒ x R y
;
transitivity says x R y ⇒
⃖R^{}(x) ⊂ ⃖R(y).
∎
Then ^{t}R is also a preorder: x R y ⇔
⃗R(y) ⊂ ⃗R(x).
Ordered set. An order is
an antisymmetric preorder. A preordered set
is a set E with a chosen preorder R.
An ordered set is a set with an
order, usually written as ≤ .
For x,y in an ordered set E, the formula
x ≤ y can be read «x is less than y»,
or «y is greater than x». The elements x
and y are said incomparable when ¬(x≤y
∨ y≤x). (This implies x≠y).
Any subset F of a set E with an order (resp. a
preorder) R ⊂ E×E, is also ordered (resp.
preordered) by its restriction R∩(F×F) (which
is an order, resp. preorder, on F).
Strict order. It is a binary relation both
transitive and irreflexive; and thus also antisymmetric.
Strict orders < bijectively correspond to orders ≤ by
x < y ⇔ (x≤y
∧ x≠y).
The inverse correspondence is defined by x ≤ y ⇔
(x<y ∨ x=y).
Total order. A total order on a set E
is an order R on E where all elements are comparable :
∀x,y∈E,
x≤y ∨ y≤x, i.e. R∪^{t}R
= E×E.
Equivalent definitions:
 an order related with its strict order < by ∀x,y∈E,
x < y ⇎ y ≤ x.
 a transitive relation ≤ such that ∀x,y∈E,
x ≤ y ⇔ (y ≤ x ⇒ x=y).
A strict order associated with a total order, called a strict
total order, is any transitive relation < on E such
that
∀x,y∈E, x<y
⇎ (y<x ∨ x=y)
or equivalently ∀x,y∈E, x=y ⇎
(y<x ∨ x<y)).
Monotone, antitone, strictly monotone functions
Between ordered sets E and F, a function f :
E → F will be said :
 monotone if ∀x,y∈E, x ≤
y ⇒ f(x) ≤ f(y)
 antitone if ∀x,y∈E, x ≤
y ⇒ f(y) ≤ f(x)
 strictly monotone if ∀x,y∈E, x
≤ y ⇔ f(x) ≤ f(y)
 strictly antitone if ∀x,y∈E, x
≤ y ⇔ f(y) ≤ f(x).
Any composite of a chain of monotone or antitone functions, is
monotone if the number of antitone functions in the chain is even,
or antitone if it is odd. Any strictly monotone or strictly antitone
function is injective. If f ∈ F^{E}
and g ∈ E^{F} are both monotone
(resp. both antitone) and g০f=Id_{E},
then f is strictly monotone (resp. strictly antitone).
Order on sets of functions
For all sets E, F where F is ordered, the
set F^{E} (and thus any subset of F^{E})
is ordered by
f ≤ g ⇔ (∀x∈E, f(x)
≤ g(x))
Then, ∀f,g∈F^{E},
∀h∈E^{G}, f ≤ g ⇒ f০h
≤ g০h, i.e. f ↦ f০h is always
monotone.
The particular case F=V_{2}
is that ℘(E) (and thus any set of sets) is naturally ordered
by ⊂ , and that h^{*} is monotone from ℘(E)
to ℘(G).
If F and G are ordered and u ∈ G^{F}
is monotone (resp. antitone) then F^{E} ∋ f
↦ u০f ∈ G^{E} is monotone
(resp. antitone).
In an ordered set E, a function f ∈ E^{E}
is said extensive if Id_{E} ≤ f i.e. ∀x∈E, x ≤ f(x).
The composite of two extensive functions is extensive.
2.8. Canonical bijections
For all objects x,y we shall say that x
determines y if there is an invariant functor T such
that T(x) = y. Then the role of y as
free variable can be played by the term T(x), thus by
the use of x. This is a metapreorder on the universe, but
not a predicate of set theory as it involves a metaconcept. Rather,
it is meant to abbreviate the use of T.
Similarly, a function f : E → F will be said canonical
if it is defined as E ∋ x ↦ T(x) for some invariant functor
T. In particular for E ⊂ F we have the canonical injection
Id_{E} : E → F, and any set E has a
canonical injection to ℘(E) defined by x ↦ {x}.
A bijection f will be
said bicanonical if both f and f^{−1}
are canonical. When a bijection f : E ↔ F
is canonical (resp. bicanonical), we write f : E ≅ F
(resp. f : E ≡ F); or, with its defining
functor, T : E ≅ F which means that (E
∋ x ↦ T(x)) is injective with image F.
We shall write E ≅ F (resp. E ≡ F)
to mean the existence of a canonical (resp. bicanonical) bijection,
that is kept implicit.
More generally we shall write E ≅_{x} F to mean a bijection defined using
the parameter x.
Canonical bijections can fail to be bicanonical especially when
their defining functor is not injective:
V_{2}^{E} ≅ ℘(E), {x}^{E}
≅ {x} and E×{x} ≅ E, whereas {x}×E
≡ E^{{x}} and E ≡ {0}×E.
This is a metapreorder on the class of sets, preserved by
constructions: for example if E ≅ E′ and F ≅
F′ then E×F ≅ E′×F′ and F^{E}
≅ F′^{E′} using the direct image of the graph
(while we may not have F^{E′} ≅ F′^{E}
when E′ does not determine E). It will often look
like a property of numbers as the existence of a bijection between
finite sets implies the equality of their numbers of elements.
The transposition of oriented pairs (E×F ≡ F×E)
extends to graphs (℘(E×F) ≡ ℘(F×E)) and
to operations: G^{E×F} ≡ G^{F×E}
where f ∈ G^{E×F} is
transposed by ^{t}f(x,y)=f(y,x).
Sums of sets, sums of functions
If S=∐_{i∈I} E_{i}
then the sum ∐ defines a canonical bijection
∏_{i∈I} ℘(E_{i})
≅ ℘(S), whose inverse S ⊃ R ↦ ⃗R_{I}
= (I ∋ i ↦ ⃗R(i))
depends on I. In particular for two sets E and F
we have (℘(F))^{E} ≅ ℘(E×F).
The sum over I of functions f_{i}
where ∀i∈I, E_{i} = Dom f_{i} is defined,
using the canonical injections j_{i} = (E_{i}
∋ x ↦ (i,x)) by
∐_{i∈I} f_{i}
= (S ∋ (i,x) ↦ f_{i}(x))
f = ∐_{i∈I }f_{i} ⇔
(Dom f = S ∧ ∀i∈I, f_{i} =
⃗f(i) = f০j_{i})
Thus the canonical bijections (bicanonical if I= Dom S, thus if E ≠ ∅ in the
case I×E)
∏
i∈I
F_{i}^{E} ≅ F^{S}
(F^{E})^{I} ≅ F^{I×E}
∏
i∈I
∏
x∈E_{i}
F_{(i,x)} ≅ ∏
c∈SF_{c}
(E×F)×G ≡ E×F×G
(f_{i})_{i∈I} ∈
(F^{E})^{I} ⇒ ∐
i∈I
Gr f_{i} ⊂ ℘(I×(E×F))
≡ ℘((I×E)×F) ⊃ Gr ∐
i∈I
f_{i}
Product of functions or recurrying
Transposing a relation R exchanges its curried forms ⃗R
and ⃖R, by a bijection (℘(F))^{E}
↔ (℘(E))^{F} with parameter F.
Similarly we have a bijection (F^{E})^{I} ↔
(F^{I})^{E}, canonical if I
≠ ∅ (to let (F^{E})^{I}
determine E), defined by a binder ∏ called the product
of the functions f_{i} ∈ F^{E}
for i ∈ I:
(f_{i})_{i∈I}
∈ ∏
i∈I
F_{i}^{E} ≅ (∏
i∈I
F_{i})^{E} ∋ ∏
i∈I
f_{i} = (E ∋ x ↦ (f_{i}(x))_{i
∈ I})
∀g, g = ∏
i∈I
f_{i} ⇔ (g : E →
∏
i∈I
Im f_{i} ∧ ∀i∈I, f_{i}
= π_{i}০g)
Dom f = Dom g = E ⇒ f×g =
(E ∋ x ↦ (f(x),g(x)))
I^{E}×F^{E} ≡
(I×F)^{E}
∐
ϕ∈I^{E} ∏
x∈E
F_{ϕ(x) }≡ (∐
i∈I
F_{i})^{E}.
2.9. Equivalence relations and partitions
Indexed partitions
A family of sets (A_{i})_{i∈I}
is called pairwise disjoint when any pair of them is
disjoint : ∀i,j∈I, i≠j ⇒
A_{i}∩A_{j} = ∅
Equivalently, (∀(i,x),(j,y) ∈
∐_{k∈I }A_{k}, x=y ⇒ i=j),
thus ∃f, Gr f = ^{t}∐_{i∈I} A_{i} with
Dom f = Im ∐_{i∈I }
A_{i} = ⋃_{i∈I}A_{i}
Im f = {i∈I  A_{i} ≠ ∅}
Inversely, any f ∈ F^{E} defines a
family f^{ •}_{F} = (f^{ •}(y))_{y∈F}
∈ ℘(E)^{F} of pairwise disjoint sets :
∀y,z∈F, f^{ •}(y)⋂f^{ •}(z)
≠ ∅ ⇒ ∃x∈ f^{ •}(y)⋂f^{ •}(z),
y = f(x) = z
An indexed partition of a set E is a family of
nonempty, pairwise disjoint subsets of E, whose union is E.
It is always injective :
∀i,j ∈ I, A_{i}
= A_{j} ⇒ A_{i}⋂A_{j}=A_{i}≠∅
⇒ i=j.
Equivalence relation defined by a function
An equivalence relation is a symmetric preorder. Any f
: E → F defines an equivalence relation on E
by
∼_{f} = {(x,y)∈E 
f(x)=f(y)} = ∐(f^{ •}০f)
Its composite g = h০f with any h ∈ G^{F}
satisfies ∼_{f} ⊂ ∼_{g}, with
∼_{f} = ∼_{g}
⇔ Inj h_{Im f} ⇒
f= (h_{Im f})^{−1}০g
In particular, ∼_{f} coincides with the equality
relation Gr Id_{E}
on E when f is injective. As ⃗∼_{f}
= f^{ •}০f, the injectivity of the indexed
partition f^{ •}_{Im f}
(that we will abusively denote as f^{ •}) gives the
characteristic identity of equivalence relations : x ∼_{f} y ⇔
⃗∼_{f}(x)= ⃗∼_{f}(y).
If F = Im f, the injection (2.6) G^{F}
∋ h ↦ h০f has image {g∈G^{E}
 ∼_{f} ⊂ ∼_{g}}: letting H = Im(f×g),
∼_{f} ⊂ ∼_{g} ⇔ ∀(y,z),
(y′,z′) ∈ H, y=y′⇒ z=z′
Dom H = F
∀h ∈ G^{F}, g = h০f ⇔ H
⊂ Gr h.
For any functions f,g such that Dom f = Dom g ∧ ∼_{f}
⊂ ∼_{g}, the function with graph Im (f×g)
is called the quotient g/f: Im f ↠ Im g,
and is the only function h such that
Dom h = Im f ∧ g = h০f.
Inversion comes as a particular case: Inj f ⇒ f^{−1} =
Id_{Dom f }/f.
Remark. If R is reflexive and ∀x,y,z,
(xRy ∧ zRy) ⇒ zRx then R is an equivalence relation.
Proof : symmetry is verified as: ∀x,y, (xRy ∧ yRy) ⇒
yRx.
Then comes transitivity.∎
Partition, canonical surjection
A partition of E is a set of nonempty, pairwise disjoint sets whose
union is E, thus the image P of any indexed partition f^{ •}
of E (where f is any function with domain E):
P = Im f^{ •} = Im(f^{ •}০f).
∀R ⊂ E×E, ∀P ⊂ ℘(E), if P
= Im ⃗R_{E} then
(∀x,y∈E,
x∈⃗R(y) ⇔
⃗R(x)=⃗R(y))
⇔ (∀x∈E, ∀A∈P, x∈A ⇔
⃗R(x)=A) ⇔
Id_{P}=(⃗R_{E})^{•}
Thus if R is an equivalence relation then P is a
partition.
Conversely for any partition P of E,
∃!g∈P^{E}, Id_{P} = g^{•}
thus P = Dom g^{•} = Im g and
R=∐g ⊂ E×E⇒
Id_{P}= (⃗R_{E})^{•}
thus R is an equivalence relation, where
x R y ⇔ (∃A∈P,
x∈A ∧ y∈A) ⇔ (∀A∈P,
x∈A ⇒ y∈A).
For any equivalence relation R on E, the partition
Im ⃗R is
called the quotient of E by R, written E/R.
The function ⃗R is the canonical
surjection from E to E/R.
For all x ∈ E, ⃗R(x)
is the only element of E/R containing x, and
called the class of x by R.
For any function f such that Dom f = E ∧ R
⊂ ∼_{f}, we can also write f/R for the function
f / ⃗R.
Order quotient of a preorder
Any preordered set (E,R) is reflected through ⃖R
by the ordered set (Im ⃖R,
⊂ ), with
⃖R(x) = ⃖R(y) ⇔ (⃖R(x)
⊂⃖R(y)∧⃖R(y)
⊂⃖R(x)) ⇔ (xRy
∧ yRx)
so that ⃖R^{} is injective if
and only if R is an order. Through ⃖R^{},
the preorder R is reduced to the order relation ⊂ in Im ⃖R^{},
which plays the role of the quotient of R in the quotient
set E/(R⋂^{t}R).
On each (ordered) set E, only one order will usually be
considered, denoted ≤_{E}, or abusively ≤ . This may
be justified by defining ordered sets as sets of sets, ordered by ⊂
, ignoring their elements.
2.10. Axiom of choice
The axiom of choice is a statement with several equivalent
formulations, named as an «axiom» because it cannot be deduced
from other axioms of set theory but it «feels true» and, when
taken as an axiom, it does not increase the risk of contradictions
but has convenient consequences. But we will actually not need it
in the rest of this work.
Axiom of choice (AC). It says ∀_{Set}X,
AC_{X}, where AC_{X}
names the following equivalent statements
(1) ∀_{Set}E,∀R⊂X×E,
(∀x∈X, ∃y∈E, xRy) ⇒ (∃f∈
E^{X}, ∀x∈X, xRf(x)).
Or in short : for any graph R, X = Dom R
⇒ ∃f ∈ (Im R)^{X}, Gr f
⊂ R.
(2) Any product over X of nonempty sets is
nonempty : (∀x∈X, A_{x}
≠ ∅) ⇒ ∏_{x∈X }A_{x} ≠
∅.
(3) ∀_{Fnc} g, Im g = X ⇒ ∃f ∈
(Dom g)^{X}, g০f=Id_{X}.
Proof of equivalence :
(1)⇒(2) by R = ∐_{x∈X}
A_{x} ;
(2)⇒(3) by A_{x}=g^{•}(x)
;
(3)⇒(1) Im π_{0R} = DomR = X
⇒ ∃(h×f) ∈ R^{X},
h=Id_{X} ∧Gr f ⊂ R. ∎
(We also have (2)⇒(1) by A_{x} = ⃗R(x),
and (1)⇒(3) by R = ^{t}Gr g)
Finite choice theorem. If X is finite then AC_{X}.
A rigorous proof for the general case will need a formal definition of finiteness. Now
let us only give a schema of proofs, one for each explicit number of
elements of X, using expression (2): for example with 3 elements, for
each triple of sets (A,B,C),
(A≠∅∧B≠∅∧C≠∅) ⇒ (∃x∈A, ∃y∈B,
∃z∈C, (x,y,z)∈A×B×C)
⇒ A×B×C ≠ ∅.∎
The different statements AC_{X} are related by the following implications:
 If there is an injection from Y to X then AC_{X}
implies AC_{Y};
 If both AC_{X} and AC_{Y} hold then
AC_{X∪Y} and AC_{X×Y} also hold;
 For any family of sets (A_{n}) indexed by I, if AC_{I}
and all AC_{An} hold then
AC_{∐i∈I Ai} holds.

If moreover U=⋃_{i∈I} A_{i} satisfies ∃f ∈ I^{U}, ^{t}Gr f
⊂ ∐_{i∈I} A_{i} then AC_{U} holds.
The proofs are easy and left as an exercise to the reader.
Theorem. The following statements are equivalent
to the axiom of choice:
(4) Any set E of nonempty sets has a choice function: ∅ ∉ E
⇒ ∏_{A∈E} A ≠ ∅.
(5) For any partition P of a set E,
∃K⊂E, ∀A∈P, ∃! : K∩A
(6) For any sets E,F,G and any
g: F ↠ G, {g০f  f
∈ F^{E}}=G^{E}.
Proofs:
(2)⇒(4) is obvious ;
(4)⇒(5) (x∈∏_{A∈P} A ∧ K
= Im x) ⇒ (K⊂E ∧∀A∈P,
x_{A}∈A ∧ ∀B∈P,
x_{B} ∈ A∩B ⇒ A=B)
(5)⇒(3) Let P = Im g^{•}. Then f =
(X∋x ↦ ϵ(K∩g^{•}(x)))
= g_{K}^{−1} ⇒ g০f =
Id_{X}.
(AC_{E} 1)⇒(6) ∀h∈G^{E},
(∀x∈E, ∃y∈F,
g(y)=h(x)) ⇒ (∃f∈F^{E},
∀x∈E, g(f(x))=h(x))
(AC_{G} 3)⇒(6) : ∃i∈F^{G},
g০i=Id_{G} ∧ ∀h∈G^{E},
i০h ∈ F^{E}∧ g০i০h=h.
(6)⇒(3) : E=G ⇒ Id_{E}
∈ {g০f  f ∈ F^{E}}. ∎
Remarks:
 (4) ⇒(2) is also easy : ∅ ∉ {A_{x}
x∈X} = E, then f ∈ ∏_{A∈E} A
⇒ (f(A_{x}))_{x∈X}
∈ ∏_{x∈X} A_{x}.
 (6) has a converse : (Dom g =F ∧ E≠∅ ∧
{g০f  f∈F^{E}} =
G^{E}) ⇒ Im g = G.
2.11. Notion of Galois connection
The set of fixed points of a function f is written
Fix f = {x∈Dom f  f(x)=x}
⊂ Im f
Then,
Im f ⊂ Fix g ⇔ (Im f ⊂ Dom g ∧ g০f=f)
Im f = Fix f ⇔ (Im f ⊂ Dom f ∧ f০f=f)
: such a function f is called idempotent.
Definition. For any ordered sets E, F,
denoting F^{−} the set F with the
transposed order, the sets of (antitone) Galois connections
between E and F, and monotone Galois connections
from E to F, are defined by
Gal(E,F)
= {(⊥,⊤) ∈ F^{E}×E^{F}∀x∈E,
∀y∈F, x ≤_{E}⊤(y) ⇔ y ≤_{F}
⊥(x)} = ^{t}Gal(F,E)
Gal^{+}(E,F)
= {(u,v) ∈ F^{E}×E^{F}∀x∈E,
∀y∈F, x ≤_{E} v(y) ⇔ u(x)
≤_{F} y} = Gal(E,F^{−})
General example. Any relation R ⊂ X×Y
defines a (⊥,⊤) ∈ Gal(℘(X),℘(Y)) by
∀A⊂X, ⊥(A) ={y∈Y 
∀x∈A, x R y} = ∩_{x∈A}
⃗R(x)
∀B⊂Y, ⊤(B) = {x∈X
 ∀y∈B, x R y} = {x∈X
 B ⊂ ⃗R(x)}
Then, ⊥(∅)=Y and ⊤(∅)=X.
Proof :
∀A⊂X, ∀B⊂F, A ⊂ ⊤(B) ⇔ A×B⊂R ⇔ B ⊂ ⊥(A).∎
This will later be shown to be a bijection : Gal(℘(X),℘(Y))
≅ ℘(X×Y).
Lemma. ∀⊥ ∈ F^{E}, !⊤ ∈
E^{F},(⊥,⊤) ∈ Gal(E,F).
Proof: ∀⊤ ∈ E^{F},
(⊥,⊤) ∈ Gal(E,F) ⇔ ⃖≤_{E}০⊤
=⊥^{*}০
⃗≤_{F}, but ⃖≤_{E}
is injective.∎
Properties. For all (⊥,⊤) ∈ Gal(E,F), the closures
Cl =⊤০⊥ ∈ E^{E} and Cl′=⊥০⊤ ∈ F^{F} satisfy
 Cl and Cl′ are extensive.

⊥ and ⊤ are antitone

Cl and Cl′ are monotone

⊥০⊤০⊥ = ⊥, and similarly ⊤০⊥০⊤ = ⊤

Im ⊤ = Im Cl = Fix Cl, called the set of closed elements of E

Cl০Cl = Cl

(⊥ strictly antitone) ⇔ Inj⊥ ⇔ Cl = Id_{E} ⇔ Im⊤ =E

∀x,x′ ∈ E, ⊥(x) ≤ ⊥(x′) ⇔ (Im⊤∩ ⃗≤(x) ⊂ ⃗≤(x′)).
 Denoting K=Im⊤, ⊤০⊥_{K}=
Id_{K} thus ⊥_{K}
is strictly antitone and ⊥_{K}^{−1} = ⊤_{Im⊥}.
Proofs:
1. ⊥(x) ≤ ⊥(x) ∴ x ≤ ⊤(⊥(x)).
1. ⇒ 2. ∀x,y ∈ E, x ≤ y ≤ ⊤(⊥(y))⇒⊥(y) ≤ ⊥(x).
1.∧2. ⇒ 4. Id_{E} ≤ Cl ⇒⊥০Cl ≤ ⊥ ≤ Cl′০⊥ = ⊥০⊤০⊥.
4.⇒5. Cl = ⊤০⊥ ∴ Im Cl ⊂ Im⊤ ;
Cl০⊤ = ⊤ ∴ Im⊤ ⊂ Fix Cl ⊂ Im Cl.
2. ⇒ 3. and 4. ⇒ 6. are obvious.
7. (Inj⊥∧⊥০Cl =⊥) ⇔ Cl = Id_{E} ⇔ (Im⊤ =E∧Cl০⊤ = ⊤);
Cl = Id_{E} ⇒ ⊥ strictly antitone ⇒ Inj ⊥.
8. ⊥(x) ≤ ⊥(x′) ⇔ (∀y∈F, x≤⊤(y)
⇒ x′≤ ⊤(y)).
9. K= Fix(⊤০⊥)
⇒ ⊤০⊥০Id_{K}=Id_{K}.
Other proof : (⊥_{K},⊤) ∈ Gal(K,F) with ⊤ surjective.
In ⊤_{Im⊥}০⊥_{K} = Id_{K} the roles of ⊤
and ⊥ are symmetrical. ∎
Remark. Properties 1. and 2. conversely imply that (⊥,⊤) ∈ Gal(E,F).
Proof: ∀x∈E, ∀y∈F, x ≤ ⊤(y) ⇒ y ≤
⊥(⊤(y)) ≤ ⊥(x).∎
Analogues of the above properties for monotone Galois connections
are obtained by reversing the order in F: if (u,v) ∈
Gal^{+}(E,F) then u and v are monotone,
v০u is extensive and u০v ≤ Id_{F}.
Closure. A closure of an ordered set E is an f
∈ E^{E} such that, equivalently:
 There exists a set F and an (u,v) ∈
Gal(E,F) or Gal^{+}(E,F)
such that v০u=f

f is monotone, idempotent and extensive

∀x∈E,∀y∈ Im f, x ≤ y
⇔ f(x) ≤ y, i.e. (f, Id_{K})
∈ Gal^{+}(E,K)
where K=Im f
Proof of equivalence:
3.⇒1. ⇒2.;
for 2. ⇒3., ∀x∈E,∀y∈K, x ≤ f(x)
≤ y ⇒ x ≤ y ⇒ f(x) ≤ f(y)
= y. ∎
Notes:
 2.⇒3. is a particular case of the remark: f০f =
f ⇒ f০Id_{K}
≤ Id_{K} (extensivity of f০Id_{K}
in K^{−}).
 ∀K⊂E, ∀f∈K^{E},
(f,Id_{K}) ∈ Gal^{+}(E,K) ⇒
Im f = K from 7) with Id_{K} injective.
More on Galois
connections