選択公理の集合系ver.と集合族ver.は同値
証明
$ \mathcal{A} を$ \mathcal{A}' にrenameしたあと、新しい$ \mathcal{A} を導入してして$ \mathcal{A}' に$ A'[\mathcal{A}] を代入する
集合族と選択函数の合成函数$ \varphi\circ A':\Gamma\rightarrow\bigcup\mathcal{A}'の存在を示す
https://kakeru.app/4b4b1f4ac338943e2c610e9f15f9ff70 https://i.kakeru.app/4b4b1f4ac338943e2c610e9f15f9ff70.svg
集合族で任意の集合系を表すには、値域と同濃度の添字集合が必要になる
てことは値域をそのまま定義域にして、集合族$ A'を恒等写像にすればいいのか
集合族は任意なので、自由に決めておk
うん。これならいける
$ \forall\Gamma\forall\mathcal{A}\forall A':\Gamma\rightarrow\mathcal{A}\exists\varphi:\Gamma\rightarrow\bigcup A'[\Gamma]\forall i\in\Gamma;\varphi(i)\in A'(i)
$ \implies\forall\mathcal{A}\forall A':\mathcal{A}\rightarrow\mathcal{A}\exists\varphi:\mathcal{A}\rightarrow\bigcup A'[\mathcal{A}]\forall i\in\mathcal{A};\varphi(i)\in A'(i)
恒等写像$ A':A\mapsto Aを代入する
$ \implies \underline{\forall\mathcal{A}\exists\varphi:\mathcal{A}\rightarrow\bigcup\mathcal{A}\forall A\in\mathcal{A};\varphi(A)\in A}_{\quad\blacksquare}
$ \because A'[\mathcal{A}]=\{A_{out}\in \mathcal{A}|\exists A_{in}\in \mathcal{A}; A_{out}=A_{in}\}=\mathcal{A}