Definition df-topon 14483

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

Assertion

Ref	Expression
df-topon	|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )

Distinct variable group:   j, b

Detailed syntax breakdown of Definition df-topon

Step	Hyp	Ref	Expression
1		ctopon 14482	. 2 class TopOn
2		vb	. . 3 setvar b
3		cvv 2772	. . 3 class _V
4	2	cv 1372	. . . . 5 class b
5		vj	. . . . . . 7 setvar j
6	5	cv 1372	. . . . . 6 class j
7	6	cuni 3850	. . . . 5 class U. j
8	4, 7	wceq 1373	. . . 4 wff b = U. j
9		ctop 14469	. . . 4 class Top
10	8, 5, 9	crab 2488	. . 3 class { j e. Top | b = U. j }
11	2, 3, 10	cmpt 4105	. 2 class ( b e. _V |-> { j e. Top | b = U. j } )
12	1, 11	wceq 1373	1 wff TopOn = ( b e. _V |-> { j e. Top | b = U. j } )

This definition is referenced by:  funtopon  14484  istopon  14485  toponsspwpwg  14494  dmtopon  14495