1 Basics of sets and classes

1.1 Preparation: things introduced in book4

word(sc,p) … \(\in\)
word(vp,c)F … \(\mathsf{cls}\)
abbr … \(\{ x \mid P \}\) ≈ \(\mathsf{cls} ( x , P )\)
=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)

1.2 Membership and equality

The set can be called the basic concept of modern abstract mathematics, and ZF (Zermelo-Fraenkel) is a famous axiom system for it.
Mathelia describes the ZF axiom system easily too, making the start of mathematics smooth.
There are two kinds of membership. Besides "belongs (to a class)", "belongs (to a set)" appears.
word(ss,p) … \(\in\)

Sets and classes can be treated as (if they were) identified.
An s-Form \({\tt X}\) in a place in a Form where a c-Form should be is replaced by Formel with \(\{x \mid x \in {\tt X}\}\) (the sc conversion).
The following seemingly trivial theorems arise.
\(X \in Y \Longleftrightarrow X \in Y\) \(\blacktriangleleft\) O
\(X = \{ x \mid x \in X \}\) \(\blacktriangleleft\) O

(Contrary to ordinary math textbooks) it is natural to derive the definition of \(=\) from the definition of \(=\).
=. … \(X = Y \Longleftrightarrow X = Y\)
=.|cvt … \(X = Y \Longleftrightarrow \forall x ( x \in X \Longleftrightarrow x \in Y )\) .　Its \(\Longleftarrow\) is the "axiom of extensionality" (one of the ZF axioms).

1.3 Inclusion

Here too there are two: "inclusion of sets" and "inclusion of classes".
word(cc,p) … \(\subset\)
word(ss,p) … \(\subset\)
⊂_. … \(X \subset Y \Longleftrightarrow \forall x \in X . x \in Y\)
⊂. … \(X \subset Y \Longleftrightarrow X \subset Y\)

\({\tt A}\) / \({\tt P}\) is "\({\tt A}\)|cvt expanded by \({\tt P}\)|cvt". / W. is used on source line 39. Here \(\mathbb{W}.\) is =. and ⊂. .
\(X = Y \Longleftrightarrow X \subset Y \subset X\) \(\blacktriangleleft\) \(\mathbb{W}.\)

1.4 The universe and the empty set

word(,c) … \(\mathbb{V}\)
𝕍. … \(\mathbb{V} = \{ x \mid \top \}\)
\(x \in \mathbb{V}\) \(\blacktriangleleft\) O
\(X \subset \mathbb{V}\) \(\blacktriangleleft\) O

word(,s) … \(\emptyset\)
∅. … \(\emptyset = \{ x \mid {\perp} \}\)
\(x \notin \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(\emptyset \subset X\) \(\blacktriangleleft\) \(\mathbb{W}.\)

A Book can also use hidden props (lemmas that, to keep the Book beautiful, we do not want to display but which are used many times in prfs).
Introduce one by writing !prop/thm as on source line 58. Click the review and check what kind of prop is hidden.

1.5 Whether a class is a set

It is natural to introduce the following predicate (taking a class as its argument).
word(c,p) … \(\dot\exists\)
Exi. … \(\dot\exists C \Longleftrightarrow \exists X \, ( X = C )\)

A class that is not a set is called a proper class. The first example is the Russell class (in Mathelia, "Russell's paradox" also becomes a theorem).
word(,c) … \(\mathbb{V}_0\)
𝕍0. … \(\mathbb{V}_0 = \{ x \mid x \notin x \}\)
\(\neg \dot\exists \mathbb{V}_0\) \(\blacktriangleleft\) O

Many ZF axioms claim that the collection of things satisfying some condition is a set. In Mathelia, for example, the "empty set axiom" is often made a theorem as follows.
ax_∅ … \(\dot\exists \{ x \mid {\perp} \}\) \(\blacktriangleleft\) ∅.

The axiom of separation claims that "a class contained in a set is a set". In Mathelia it can be expressed by one Form as follows.
ax_s … \(\exists X \, C \subset X \Longrightarrow \dot\exists C\)
It follows that the universe is also a proper class.
\(\neg \dot\exists \mathbb{V}\) \(\blacktriangleleft\) ax_s
The empty set axiom is also derived from ax_s.
ax_∅ \(\blacktriangleleft\) ax_s