2 Elementary set functions

2.1 Extensional notation

Formel can also use word families. They make a set having exactly the specified elements. For a natural number \({\tt n}\) ≥ 1,
word(s\(^{\tt n}\),s)F … \(\mathsf{set}_{\tt n}\)
where s\(^{\tt n}\) is s repeated \({\tt n}\) times.
abbr … \(\{ x_{1} , \cdots , x_{\tt n} \}\) ≈ \(\mathsf{set}_{\tt n} ( x_{1} , \cdots , x_{\tt n} )\)
Formel handles \(\cdots\) and \({\tt n}\) appropriately. Example　 \(\{ x , \{ x , y \} \}\) ≈ \(\mathsf{set}_{2} ( x , \mathsf{set}_{2} ( x , y ) )\)

Definition families can also be used. When the following set\({\tt n}\). is introduced in a Book, \(\mathbb{W}.\) becomes an infinite sequence.
set\({\tt n}\). … \(\{ x_{1} , \cdots , x_{\tt n} \} = \{ v \mid v = x_{1} \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} v = x_{\tt n} \}\)
Source line 98 also has a hidden prop, containing \({\tt n}\). at \n=1..4 means "show it for each of \({\tt n}\)=1,2,3,4". The /1 =. in the prf means "expand only the 1st element by =.".
Axiom of pairing
ax_set2 … \(\dot\exists \{ a \mid a = x \mathbin{\rm o\!r} a = y \}\) \(\blacktriangleleft\) set2.

2.2 Power set

word(s,s) … \(\wp\)
℘. … \(\wp X = \{ A \mid A \subset X \}\)
Power set axiom
ax_℘ … \(\dot\exists \{ A \mid A \subset X \}\) \(\blacktriangleleft\) ℘.

Source line 118 has the prf of the following elementary theorem.
\({\tt P}\) / W. was "\({\tt P}\) expanded by 〇.", while \({\tt P}\) / W.' is "expanded by 〇.' if there is 〇.', otherwise by 〇.".
/ W.'!=. does / W.' but does not use =. (expanding down to = is expanding too far, and the proof does not go through).
// W.'!=. is / W.'!=. / W.'!=..
\(\wp \emptyset = \{ \emptyset \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

2.3 Union and intersection

word(c,c) … \(\bigcup\)  \(\bigcap\)
⋃_. … \(\bigcup \mathcal{X} = \{ x \mid \exists X \in \mathcal{X} . x \in X \}\)
⋂_. … \(\bigcap \mathcal{X} = \{ x \mid \forall X \in \mathcal{X} . x \in X \}\)
\(\bigcap \emptyset = \mathbb{V}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

The union and intersection of classes can be defined cleanly, and those of sets are derived from them.
word(s,s)R … \(\bigcup\)  \(\bigcap\)
⋃. … \(\bigcup \mathcal{X} = \bigcup \mathcal{X}\)
⋂. … \(\mathcal{X} \neq \emptyset \Longrightarrow \bigcap \mathcal{X} = \bigcap \mathcal{X}\)
Axiom of union
ax_⋃ … \(\dot\exists \{ x \mid \exists X \in \mathcal{X} . x \in X \}\) \(\blacktriangleleft\) ⋃.

⋂.|cvt … \(\mathcal{X} \neq \emptyset \Longrightarrow \forall x ( x \in \bigcap \mathcal{X} \Longleftrightarrow \forall X \in \mathcal{X} . x \in X )\) .
For a definition of the form \(P \Longrightarrow ( Q \Longleftrightarrow R )\) like ⋂., / first transforms it into the equivalent \(Q \Longleftrightarrow ( P \Longrightarrow R ) , ( \neg P \Longrightarrow Q )\) and then computes.
/ ⋂. gives \(x \in \bigcap \mathcal{X} \Longleftrightarrow ( \mathcal{X} \neq \emptyset \Longrightarrow \forall X \in \mathcal{X} . x \in X ) , ( \mathcal{X} = \emptyset \Longrightarrow x \in \bigcap \mathcal{X} )\) .
Precisely, to prevent re-expansion, the last \(\bigcap\) is temporarily made \(\bigcap\) and turned back into \(\bigcap\) in the final result.

The union and intersection of two sets are often used.
word(ss,s) … \(\cup\)  \(\cap\)
∪. … \(X \cup Y = \{ x \mid x \in X \mathbin{\rm o\!r} x \in Y \}\)
∩. … \(X \cap Y = \{ x \mid x \in X , x \in Y \}\)
\(X \cup Y = \bigcup \{ X , Y \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(X \cap Y = \bigcap \{ X , Y \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

2.4 Extending comprehension notation

The following is a special example in which the source $_X on the left side is not shown in tex notation (and it is commonly used in ordinary mathematics).
abbr … \(\{ T \mid P \}\) ≈ \(\{ x \mid \exists \mathop{{\sf X}} ( ( P ) , x = T ) \}\)
abbr … \(_{ P } T\) ≈ \(\{ T \mid P \}\)
\(X = \bigcup _{ x \in X } \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)