Definition df-topon

Description: Define the function that associates with a set the set of topologies on it. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Assertion	df-topon	$$⊢\mathrm{TopOn}=\left(b\in \mathrm{V}⟼\left\{j\in \mathrm{Top}|b=\bigcup j\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctopon	$$class\mathrm{TopOn}$$
1		vb	$$setvarb$$
2		cvv	$$class\mathrm{V}$$
3		vj	$$setvarj$$
4		ctop	$$class\mathrm{Top}$$
5	1	cv	$$setvarb$$
6	3	cv	$$setvarj$$
7	6	cuni	$$class\bigcup j$$
8	5 7	wceq	$$wffb=\bigcup j$$
9	8 3 4	crab	$$class\left\{j\in \mathrm{Top}|b=\bigcup j\right\}$$
10	1 2 9	cmpt	$$class\left(b\in \mathrm{V}⟼\left\{j\in \mathrm{Top}|b=\bigcup j\right\}\right)$$
11	0 10	wceq	$$wff\mathrm{TopOn}=\left(b\in \mathrm{V}⟼\left\{j\in \mathrm{Top}|b=\bigcup j\right\}\right)$$