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	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctopon	|- TopOn
1		vb	|- b
2		cvv	|- _V
3		vj	|- j
4		ctop	|- Top
5	1	cv	|- b
6	3	cv	|- j
7	6	cuni	|- U. j
8	5 7	wceq	|- b = U. j
9	8 3 4	crab	|- { j e. Top | b = U. j }
10	1 2 9	cmpt	|- ( b e. _V |-> { j e. Top | b = U. j } )
11	0 10	wceq	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )