集合の宇宙の定義

集合の宇宙の定義を試みます。
※最後尾に追記をしました。

その前に記号の定義
Powはベキ集合演算子
Pow := { (x,y) | x,yは集合 ∧ { u | ∀v(v∈u ⇒ v∈x) }=y }

練習 : Pow({1,2,3}) = {∅,{1},{2},{3},{1,2},{2,3},{1,3},{1,2,3}}

Unionは和集合演算子
Union := { (x,y) | x,yは集合 ∧ { u | ∃v(u∈v ∧ v∈x) }=y }

練習 : Union({{1,2,3},{3,4},{1,3,5}}) = {1,2,3,4,5}
練習 : Union(∅) = ∅
練習 : Union({∅}) = ∅
練習 : ∀x(Union(Pow(x))=x)
練習 : ∀x(Union({ {y} | y∈x })=x)
練習 : ∀x(Union({x})=x)

Intersectは共通集合演算子
Intersect := { (x,y) | x,yは集合 ∧ { u | u∈Union(x) ∧ ∀v(v∈x ⇒ u∈v) }=y }

練習 : Intersect({{1,2,3},{3,4},{1,3,5}}) = {3}
練習 : ∀x(Intersect(x)⊂Union(x))

Domは定義域演算子
Dom := { (f,x) | f,xは集合 ∧ { u | ∃v((u,v)∈f) }=x }

練習 : Dom({0,(1,a),(2,{b}),((3,4),c)}) = {1,2,(3,4)}

Ranは値域演算子
Ran := { (f,y) | f,yは集合 ∧ { v | ∃u((u,v)∈f) }=y }

練習 : Ran({0,(1,a),(2,{b}),((3,4),c)}) = {a,{b},c}

Prodは直積集合演算子
Prod := { ((x,y),z) | x,y,zは集合 ∧ { (u,v) | u∈x ∧ v∈y }=z }

練習 : Prod({1,2},{a,b,c}) = {(1,a),(1,b),(1,c),(2,a),(2,b),(2,c)}

MapClassは写像のクラス
MapClass := ({∅}∪{ f | f≠∅ ∧ f⊂Prod(Dom(f),Ran(f)) ∧ ∀u(u∈Dom(f) ⇒ ∃!v(v∈Ran(f) ∧ (u,v)∈f))})

Onは順序数のクラス
On := { x | xは順序数 ∧ ￢(x∈x) }

ωは最小の極限順序数
ω := Intersect({ x | ∅∈x ∧ ∀y(y∈x ⇒ Suc(y)∈x) })

{x,y}はxとyの非順序対
{x,y} := { u | u=x ∨ u=y }

備考 : {x} := {x,x}
説明 : 最初に2引数をとる形式{x,y}があり、それを基に1引数をとる形式{x}が与えられます。

(x,y)はxとyの順序対
(x,y) := {{x,x},{x,y}}

Uを集合の宇宙としておきます。
Uが満たすべき条件を挙げると、
・まずUはωを要素として含んでいること。つまり、ω∈U。
・x∈Uならば、Pow(x)∈U、Union(x)∈Uという連鎖があること。
・x,y∈Uならば、{x,y}∈U、(x,y)∈Uという連鎖があること。
　(x,y)という形式も積極的に集合として認めていこうという立場となります。
・そしてUは推移的であること。
　つまり、x∈y∈Uならば、x∈U。
・置換公理を備えていること
という感じになるでしょう。

置換公理は次のような形で与えることにします。
fは写像として、その定義域Dom(f)がUに要素として含まれていて、x∈Dom(f)に対してf(x)の行く先がまたUに要素として含まれていれば、それらを束ねたfの値域をUの要素として含めましょう。
つまり、
∀f((f∈MapClass ∧ Dom(f)∈U ∧ Ran(f)⊂U) ⇒ Ran(f)∈U)
という表記になります。
集合関数も写像として積極的に認めようという立場になります。

全部をまとめると、
{ U | ω∈U
∧ ∀x(x∈U ⇒ Pow(x)∈U)
∧ ∀x(x∈U ⇒ Union(x)∈U)
∧ ∀x∀y(x,y∈U ⇒ {x,y}∈U)
∧ ∀x∀y(x,y∈U ⇒ (x,y)∈U)
∧ ∀x∀y((x∈U ∧ y∈x) ⇒ y∈U)
∧ ∀f((f∈MapClass ∧ Dom(f)∈U ∧ Ran(f)⊂U) ⇒ Ran(f)∈U) }
となります。
このクラスはただ一つの要素を持つ単集合にはなりません。
Uがωを種に生成されるもの以外を含んでいてもまったくかまわないからです。
つまり、余分なものから生成される系を含むUも存在しています。
ならば、それらすべての共通集合をとれば、求めるただ一つのUが得られるでしょうか？
その確証はまだ得られていません。
ここから先の理論展開が分からず、集合の宇宙に関する私の考察はここで行き詰まっています。

以上のことを念頭に形式だけ追い求めます。
ωにこだわらないで、もっと一般的な順序数で考えます。
集合の宇宙は次のような形式になると考えたくなります。
Universe := { (α,A) | α∈On ∧ Aはクラス ∧
Intersect({ U | α∈U
∧ ∀x(x∈U ⇒ Pow(x)∈U)
∧ ∀x(x∈U ⇒ Union(x)∈U)
∧ ∀x∀y(x,y∈U ⇒ {x,y}∈U)
∧ ∀x∀y(x,y∈U ⇒ (x,y)∈U)
∧ ∀x∀y((x∈U ∧ y∈x) ⇒ y∈U)
∧ ∀f((f∈MapClass ∧ Dom(f)∈U ∧ Ran(f)⊂U) ⇒ Ran(f)∈U) })=A
}
このように写像の形式で与えます。
直感的に
∀α∀β((α,β∈On ∧ α∈β) ⇒ Universe(α)⊂Universe(β))
が分かるでしょうか。
α∈βの意味は順序数α、βの順序関係を表わしています。
順序数は所属関係で順序関係を与えると整列順序になること、整列順序は全順序であることを注意しておきます。
このように順序数のクラスOnの順序性を利用して、集合の宇宙を広げて行きます。
そして、
Union({ Universe(α) | α∈On })
と言うように集合の宇宙を目一杯広げ、集合論で語りうる全体を示すことになります。
しかし、一般的な数学は
Universe(ω)
の中で展開されるようです。

直積集合はどうなると思いますか。
直積集合は自然にUに含まれています。それを示します。
A,B∈Uとします。
Prod(A,B) = Union({ { (x,y) | x∈A } | y∈B })
が成立しているので、右辺がUに属していることを示します。
Uの推移性より
x∈A ⇒ x∈U
y∈B ⇒ y∈U
順序対にして、(x,y)∈U
{ (x,(x,y)) | x∈A }はAからUへの写像と見ることができるので、
Ran({ (x,(x,y)) | x∈A })⊂U
置換公理より、
Ran({ (x,(x,y)) | x∈A })∈U
Ran({ (x,(x,y)) | x∈A }) = { (x,y) | x∈A }なので、
{ (x,y) | x∈A }∈U
{ (y,{ (x,y) | x∈A }) | y∈B }はBからUへの写像と見ることができるので、
Ran({ (y,{ (x,y) | x∈A }) | y∈B })⊂U
置換公理より、
Ran({ (y,{ (x,y) | x∈A }) | y∈B })∈U
Ran({ (y,{ (x,y) | x∈A }) | y∈B }) = { { (x,y) | x∈A } | y∈B }なので、
{ { (x,y) | x∈A } | y∈B }∈U
和集合演算子を適用して、
Union({ { (x,y) | x∈A } | y∈B })∈U
よって、Prod(A,B)∈U
まとめると、∀A∀B(A,B∈U ⇒ Prod(A,B)∈U)

順序対の定義に怪しさを感じます。
具体的な定義を与えてしまって、後から矛盾が発生したりしないのでしょうか。

また、順序対を公理的に考えると、
順序対はU×UからUへの写像で、
その写像をφとすると、
∀x∀y∀u∀v((x,y,u,v∈U ∧ φ(x,y)=φ(u,v)) ⇒ (x=u ∧ y=v))
を満たしていなければなりません。
同時に
∃x∃y(x,y∈U ∧ φ(x,y)≠φ(y,x))
を満たしていなければいけないでしょう。
もっと冴えたやり方で順序対の対応物をUの中に与える方法はないものでしょうか。

あるいは、順序対にはUの中に対応物を求めてはいけないのかも知れません。
つまり、Uには順序対は(x,y)の形のままで存在しているのかも知れません。

位相空間を指定するとき、集合Xとその位相Tを対にして、「(X,T)は位相空間とする」という具合に使われます。
群を指定するときも、集合Gとその演算ρを対にして、「(G,ρ)は群とする」などのように使われます。
このとき、(X,T)や(G,ρ)にUの中に対応物を求めるというのも、妙な感じがします。
これらを順序対として扱っていいのかどうかという問題もありそうですが。

順序対の形式は簡単に取り扱わないで、ちゃんと考察しなければいけないと思います。

※追記部分です。
次に示す変形を思いつきました。
ω∈U ⇔ {ω}⊂U
∀x(x∈U ⇒ Pow(x)∈U) ⇔ { Pow(x) | x∈U }⊂U
∀x(x∈U ⇒ Union(x)∈U) ⇔ { Union(x) | x∈U }⊂U
∀x∀y(x,y∈U ⇒ {x,y}∈U) ⇔ { {x,y} | x,y∈U }⊂U
∀x∀y(x,y∈U ⇒ (x,y)∈U) ⇔ { (x,y) | x,y∈U }⊂U
∀x∀y((x∈U ∧ y∈x) ⇒ y∈U) ⇔ { y | ∃x(y∈x ∧ x∈U) }=Union(U)⊂U
∀f((f∈MapClass ∧ Dom(f)∈U ∧ Ran(f)⊂U) ⇒ Ran(f)∈U) ⇔ { Ran(f) | f∈MapClass ∧ Dom(f)∈U ∧ Ran(f)⊂U }⊂U

これらを一つにまとめて、
Union({ {ω}, {Pow(x)|x∈U}, {Union(x)|x∈U}, {{x,y}|x,y∈U}, {(x,y)|x,y∈U}, Union(U), {Ran(f)|f∈MapClass∧Dom(f)∈U∧Ran(f)⊂U} })⊂U

これをUのクラスの条件パートと入れ替えて、
{ U | Union({ {ω}, {Pow(x)|x∈U}, {Union(x)|x∈U}, {{x,y}|x,y∈U}, {(x,y)|x,y∈U}, Union(U), {Ran(f)|f∈MapClass∧Dom(f)∈U∧Ran(f)⊂U} })⊂U }
これはUに関する集合論的方程式になっています。
代数方程式のように見えて面白く思えたので追記しました。