| 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 |