This text explains how the description of mathematical theorems is actually carried out using Mizar with set theory as the subject matter. In Mizar, texts written in its mathematical description language are called articles. The Mizar system and the grammar of the mathematical language it uses are explained in the \emph{Mizar Lecture Notes, Third Edition} by Professor Yatsusaku Nakamura http://markun.cs.shinshu-u.ac.jp/kiso/projects2/proofchecker/mizar/Mizar-J/Miz-tit.html. Moreover, the Mizar system for PC download as well as the web-based Mizar system can be found at　http://markun.cs.shinshu-u.ac.jp/kiso/projects2/proofchecker/mizar/index-j.html.

In this text, we describe the basic articles on set theory from the Mizar library (a database of mathematical theorems written in Mizar), namely TARSKI.miz, XBOOLl0.miz, and XBOOLl1.miz.

From now on, we will begin to decipher TARSKI.miz.
First, there is the following environment section. This section declares that the vocabulary used in this article is specified in a file called TARSKI.voc$.
Then, starting with the declaration of begin, the content of this article begins.

reserve indicates the type of the variables that follow. In this example, \(x, y, z, u, N, M, X, Y, Z\) are arbitrary sets. In set theory, the objects under consideration are either sets or their elements; however, sets and elements are not formally distinguished. Thus, the term ``set'' denotes an arbitrary object.

(Definition of the equality of two sets)
First, we have the following description.

In symbolic logic, this is written as \[ ((\forall x)(x \in X \Leftrightarrow x \in Y)) \Rightarrow X = Y. \] This is known as the \textbf{Axiom of Extensionality}. It states that if, for every \(x\), \[ x \in X \Leftrightarrow x \in Y, \] then the two sets \(X\) and \(Y\) are equal (i.e., \(X = Y\)).

The following description defines the singleton set $\{x\}$ (a set containing only $x$) and the unordered pair (a set containing two elements, $x$ and $y$) denoted as $\{x, y\}$.

For any $y$, the singleton set $\{y\}$ is defined as the set that satisfies, for every $x$ $$x \in \{y\} \Leftrightarrow x = y.$$ For any $y$ and $z$, the unordered pair $\{y, z\}$ is defined as the set that satisfies, for every $x$, $$x \in \{y, z\} \Leftrightarrow x = y \lor x = z.$$ Furthermore, commutativity is expressed by the equality $$\{y, z\} = \{z, y\}.$$

Below is the definition of the predicate stating that “set $X$ is a subset of set $Y$” or equivalently, “set $X$ is contained in set $Y$”.

For any sets $X$ and $Y$, we say that $$X \subseteq Y$$ if and only if, for every $x$, the implication $$x \in X \Rightarrow x \in Y$$ holds. Reflexivity means that for any set $X$, it holds that $$X \subseteq X.$$

For any family of sets (i.e., a set of sets) $X$, the union of all sets belonging to　$X$ is defined as the functor (operation) that maps $X$ to $\cup X$.

For any $X$, the functor (operation) $\cup X$ is defined as the mapping that associates to $X$ the set satisfying, for any $x$ に対して

$$(x \in \cup X) \Leftrightarrow((\exists Y)(x \in Y \land Y \in X)).$$

The following is stated as a theorem with its proof omitted; however, it is known as the Axiom of Regularity.

In symbolic logic, for any set $X$, it is written as $$(x \in X) \Rightarrow (\exists Y)(Y \in X \land \neg (\exists x)(x \in X \land x \in Y)).$$ This expresses the claim that if $x$ is an element of the set $X$, then there does not exist any $Y$ that is both an element of $X$ and contains $x$ as one of its elements.

The following is an axiom schema that describes the procedure for constructing a set $X$ from a set $A$ and a relational formula $P[x, y]$.

For any set \(A\) and any relation \(P\) satisfying \[ (\forall x, y, z)(P[x,y] \land P[x,z] \Rightarrow y=z), \] there exists a set \(X\) such that \[ (\forall x)(x \in X \Leftrightarrow (\exists y)(y \in A \land P[y,x])). \]

For any \(x\) and \(y\), the ordered pair \([x, y]\) is defined by \[ [x, y] := \{\{x, y\}, \{x\}\}. \] This definition treats the mapping from \(x\) and \(y\) to \([x, y]\) as a functor (operation) that constructs the ordered pair from \(x\) and \(y\).

The following definition states that two sets \(X\) and \(Y\) are said to be equipotent (i.e., have equal cardinalities) if there exists a bijection (a one-to-one and onto mapping) between them.

Namely, for any sets \(X\) and \(Y\), we say that \(X\) and \(Y\) are equipotent (i.e., have equal cardinalities) if and only if there exists a set \(Z\) such that \[ \exists Z \left\{ \begin{aligned} &\forall x \in X\, \exists y \in Y\, \bigl([x, y] \in Z\bigr) \land \\ &\forall y \in Y\, \exists x \in X\, \bigl([x, y] \in Z\bigr) \land \\ &\forall x, y, z, u\, \Bigl( \bigl([x, y] \in Z \land [z, u] \in Z\bigr) \implies (x = z \Leftrightarrow y = u) \Bigr) \end{aligned} \right\} \] holds.

Shitama, Yasunari. Mizar and Set Theory Accessed on March 25, 2017.