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 
|- dom TopOn = _V

Proof

Step Hyp Ref Expression
1 vpwex 
 |-  ~P x e. _V
2 1 pwex 
 |-  ~P ~P x e. _V
3 eqcom 
 |-  ( x = U. y <-> U. y = x )
4 3 rabbii 
 |-  { y e. Top | x = U. y } = { y e. Top | U. y = x }
5 rabssab 
 |-  { y e. Top | U. y = x } C_ { y | U. y = x }
6 pwpwssunieq 
 |-  { y | U. y = x } C_ ~P ~P x
7 5 6 sstri 
 |-  { y e. Top | U. y = x } C_ ~P ~P x
8 4 7 eqsstri 
 |-  { y e. Top | x = U. y } C_ ~P ~P x
9 2 8 ssexi 
 |-  { y e. Top | x = U. y } e. _V
10 df-topon 
 |-  TopOn = ( x e. _V |-> { y e. Top | x = U. y } )
11 9 10 dmmpti 
 |-  dom TopOn = _V