>>250
>metric spaces として completion（完備）までやっているが、どの選択公理を使うかの記述がない
>”axiom of dependent choice”だと思うのだが・・ （＾＾

分かってないけど、分かりましたｗ　；ｐ）
下記”ソロヴェイモデル”で
『ZF + DC を満たし、実数集合が全てルベーグ可測で perfect set property を持ち、ベールの性質を持つものになっている。この証明には、M[G] の実数は全て順序数の可算列を用いて定義可能であり、N と M[G] が同じ実数を持っていることを使う。』
とあるので、”ZF + DC”でよさそう
”到達不能基数”の要否は、いまいちわかりません！ｗ ；ｐ）

(参考)
ja.wikipedia.org/wiki/%E3%82%BD%E3%83%AD%E3%83%B4%E3%82%A7%E3%82%A4%E3%83%A2%E3%83%87%E3%83%AB
ソロヴェイモデルはロバート M. ソロヴェイ (1970)によって構成されたモデルでツェルメロ＝フレンケル集合論 (ZF) の全ての公理が成り立ち、選択公理を除去し、実数の集合が全てルベーグ可測であるようにしたものである。この構成は到達不能基数の存在に依拠している。

これによってソロヴェイはルベーグ不可測集合の存在をZFC (ZF+選択公理) から証明するには、少なくとも到達不能基数の存在がZFCと矛盾しない限り、選択公理が本質的に必要であることを示した。

構成
ソロヴェイはそのモデルを二つのステップによって構成した。まず初めに、到達不能基数 κ を含む ZFC のモデル M から始める。
略す
二つ目のステップではソロヴェイのモデル N として、M[G] の中で順序数の可算列で遺伝的に定義可能な集合全てからなるクラスを考える。このモデル N は M[G] の内部モデルであって ZF + DC を満たし、実数集合が全てルベーグ可測で perfect set property を持ち、ベールの性質を持つものになっている。この証明には、M[G] の実数は全て順序数の可算列を用いて定義可能であり、N と M[G] が同じ実数を持っていることを使う。
略す

補足
ソロヴェイは自身の論文で、到達不能基数の使用は必要ないかもしれないと示唆した。何人かの研究者はソロヴェイの結果の弱いバージョンを到達不能基数の存在を仮定せずに証明した。特に、Krivine (1969) は順序数定義可能な実数集合は全てルベーグ可測である ZFC のモデルの存在を示したし、ソロヴェイは ZF + DC のモデルであって、ルベーグ測度の拡張で平行移動不変性を持ちつつ全ての集合に定義可能であるような測度が存在するモデルの存在を示したし、そして Shelah (1984) は実数集合が全てベールの性質を持つモデルの存在を示した (つまり、実はベールの性質には到達不能基数は不要であった).

最終的に、Shelah (1984) では到達不能基数の無矛盾性が、実数集合が全てルベーグ可測であるモデルの構成に必要であることが示された。もっと正確には、彼は全ての Σ1
3 な実数集合が可測であれば、最小の不可算基数 ℵ1 が構成可能宇宙で到達不能になっていることを示した。つまり、ソロヴェイの定理から、到達不能基数の条件は外すことはできない。

en.wikipedia.org/wiki/Solovay_model
Solovay model

en.wikipedia.org/wiki/Vitali_set
Vitali set

ja.wikipedia.org/wiki/%E3%83%B4%E3%82%A3%E3%82%BF%E3%83%AA%E9%9B%86%E5%90%88
ヴィタリ集合