Theorem dmtopon

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

	Ref	Expression
Assertion	dmtopon	$$⊢\mathrm{dom}\mathrm{TopOn}=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		vpwex	$$⊢𝒫x\in \mathrm{V}$$
2	1	pwex	$$⊢𝒫𝒫x\in \mathrm{V}$$
3		eqcom	$$⊢x=\bigcup y\leftrightarrow \bigcup y=x$$
4	3	rabbii	$$⊢\left\{y\in \mathrm{Top}|x=\bigcup y\right\}=\left\{y\in \mathrm{Top}|\bigcup y=x\right\}$$
5		rabssab	$$⊢\left\{y\in \mathrm{Top}|\bigcup y=x\right\}\subseteq \left\{y|\bigcup y=x\right\}$$
6		pwpwssunieq	$$⊢\left\{y|\bigcup y=x\right\}\subseteq 𝒫𝒫x$$
7	5 6	sstri	$$⊢\left\{y\in \mathrm{Top}|\bigcup y=x\right\}\subseteq 𝒫𝒫x$$
8	4 7	eqsstri	$$⊢\left\{y\in \mathrm{Top}|x=\bigcup y\right\}\subseteq 𝒫𝒫x$$
9	2 8	ssexi	$$⊢\left\{y\in \mathrm{Top}|x=\bigcup y\right\}\in \mathrm{V}$$
10		df-topon	$$⊢\mathrm{TopOn}=\left(x\in \mathrm{V}⟼\left\{y\in \mathrm{Top}|x=\bigcup y\right\}\right)$$
11	9 10	dmmpti	$$⊢\mathrm{dom}\mathrm{TopOn}=\mathrm{V}$$