Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
Zermelo Theorem and Axiom of Choice

Grzegorz Bancerek

Warsaw University, Bialystok
Summary.

The article is continuation of [2] and [1],
and the goal of it is show that Zermelo theorem (every set has a relation
which well orders it  proposition (26)) and axiom of choice (for every
nonempty family of nonempty and separate sets there is set which has
exactly one common element with arbitrary family member  proposition (27))
are true. It is result of the Tarski's axiom A introduced in [5]
and repeated in [6]. Inclusion as a settheoretical binary relation
is introduced, the correspondence of well ordering relations
to ordinal numbers is shown, and basic properties of
equinumerosity are presented. Some facts are based on [4].
The terminology and notation used in this paper have been
introduced in the following articles
[6]
[7]
[8]
[3]
[2]
[1]
Contents (PDF format)
Bibliography
 [1]
Grzegorz Bancerek.
The ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Grzegorz Bancerek.
The well ordering relations.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Kazimierz Kuratowski and Andrzej Mostowski.
\em Teoria mnogosci.
PTM, Wroc\law, 1952.
 [5]
Alfred Tarski.
\"Uber Unerreichbare Kardinalzahlen.
\em Fundamenta Mathematicae, 30:176183, 1938.
 [6]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [7]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [8]
Edmund Woronowicz and Anna Zalewska.
Properties of binary relations.
Journal of Formalized Mathematics,
1, 1989.
Received June 26, 1989
[
Download a postscript version,
MML identifier index,
Mizar home page]