52a・52b・58 などで共通に使う準備：集合の基本・全単射と個数（=#）・集合で作る自然数と帰納法・加法と個数。

1 準備

1.1 andの縦表記

abbr … \(\begin{cases} P_{1} \\ \vdots \\ P_{\tt n} \end{cases}\) ≈ \(( P_{1} ) , \cdots , ( P_{\tt n} )\)

1.2 基本的な集合関数

word(,s) … \(\emptyset\)
∅. … \(\emptyset = \{ x \mid {\perp} \}\)

word(s\(^{\tt n}\),s)F … \(\mathsf{set}_{\tt n}\)
abbr … \(\{ x_{1} , \cdots , x_{\tt n} \}\) ≈ \(\mathsf{set}_{\tt n} ( x_{1} , \cdots , x_{\tt n} )\)
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} \}\)

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 \}\)

word(s,s) … \(\wp\)
℘. … \(\wp X = \{ A \mid A \subset X \}\)

1.3 順序対、直積

word(ss,s)F … \(\mathsf{pr}\)
abbr … \(\langle X , Y \rangle\) ≈ \(\mathsf{pr} ( X , Y )\)
word(s,s) … \(\triangleleft\)  \(\triangleright\)
◁. … \(\triangleleft \langle x , y \rangle = x\)
▷. … \(\triangleright \langle x , y \rangle = y\)
pr:0 … \(\langle x_{0} , y_{0} \rangle = \langle x_{1} , y_{1} \rangle \Longleftrightarrow x_{0} = x_{1} , y_{0} = y_{1}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

word(ss,s) … \(\times\)
^^pr. … \(X \times Y = \{ \langle x , y \rangle \mid x \in X , y \in Y \}\)
word(s,s) … \(^{\hat\leftrightarrow}\)
^sw. … \(R ^{\hat\leftrightarrow} = \{ \langle y , x \rangle \mid \langle x , y \rangle \in R \}\)
word(ss,s) … \(\circ\)
∘. … \(S \circ R = \{ \langle x , z \rangle \mid \exists y \, ( \langle x , y \rangle \in R , \langle y , z \rangle \in S ) \}\)

1.4 全単射

word(ss,s) … \(\stackrel{\rm IS}\to\)
→IS. … \(X \stackrel{\rm IS}\to Y = \{ f \subset X \times Y \mid \forall x \in X . \exists! y \, \langle x , y \rangle \in f , \forall y \in Y . \exists! x \, \langle x , y \rangle \in f \}\)
→IS^sw … \(f \in X \stackrel{\rm IS}\to Y \Longrightarrow f ^{\hat\leftrightarrow} \in Y \stackrel{\rm IS}\to X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
→IS∘ … \(f \in X \stackrel{\rm IS}\to Y , g \in Y \stackrel{\rm IS}\to Z \Longrightarrow g \circ f \in X \stackrel{\rm IS}\to Z\) \(\blacktriangleleft\) \(\mathbb{W}.\)
→IS∪ … \(\begin{cases} f \in X \stackrel{\rm IS}\to X' \\ g \in Y \stackrel{\rm IS}\to Y' \end{cases} , \begin{cases} X \cap Y = \emptyset \\ X' \cap Y' = \emptyset \end{cases} \Longrightarrow f \cup g \in X \cup Y \stackrel{\rm IS}\to X' \cup Y'\) \(\blacktriangleleft\) \(\mathbb{W}.\)

word(s,s) … \(\text{id}\)
id. … \(\text{id} _ X = \{ \langle x , x \rangle \mid x \in X \}\)
id:0 … \(\text{id} _ X \in X \stackrel{\rm IS}\to X\) \(\blacktriangleleft\) \(\mathbb{W}.\)

word(ss,p) … \(\stackrel{\#}=\)
=#. … \(X \stackrel{\#}= Y \Longleftrightarrow X \stackrel{\rm IS}\to Y \neq \emptyset\)
=#:R … \(X \stackrel{\#}= X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
=#:T … \(X \stackrel{\#}= Y \stackrel{\#}= Z \Longrightarrow X \stackrel{\#}= Z\) \(\blacktriangleleft\) \(\mathbb{W}.\)
=#:X … \(X \stackrel{\#}= Y \Longleftrightarrow Y \stackrel{\#}= X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
=#∪ … \(\begin{cases} X \stackrel{\#}= X' \\ Y \stackrel{\#}= Y' \end{cases} , \begin{cases} X \cap Y = \emptyset \\ X' \cap Y' = \emptyset \end{cases} \Longrightarrow X \cup Y \stackrel{\#}= X' \cup Y'\) \(\blacktriangleleft\) \(\mathbb{W}.\)