Metamath Proof Explorer


Theorem dmtopon

Description: The domain of TopOn is the universal class _V . (Contributed by BJ, 29-Apr-2021)

Ref Expression
Assertion dmtopon domTopOn=V

Proof

Step Hyp Ref Expression
1 vpwex 𝒫xV
2 1 pwex 𝒫𝒫xV
3 eqcom x=yy=x
4 3 rabbii yTop|x=y=yTop|y=x
5 rabssab yTop|y=xy|y=x
6 pwpwssunieq y|y=x𝒫𝒫x
7 5 6 sstri yTop|y=x𝒫𝒫x
8 4 7 eqsstri yTop|x=y𝒫𝒫x
9 2 8 ssexi yTop|x=yV
10 df-topon TopOn=xVyTop|x=y
11 9 10 dmmpti domTopOn=V