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 = ( 𝑏 ∈ V ↦ { 𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctopon	⊢ TopOn
1		vb	⊢ 𝑏
2		cvv	⊢ V
3		vj	⊢ 𝑗
4		ctop	⊢ Top
5	1	cv	⊢ 𝑏
6	3	cv	⊢ 𝑗
7	6	cuni	⊢ ∪ 𝑗
8	5 7	wceq	⊢ 𝑏 = ∪ 𝑗
9	8 3 4	crab	⊢ { 𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗 }
10	1 2 9	cmpt	⊢ ( 𝑏 ∈ V ↦ { 𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗 } )
11	0 10	wceq	⊢ TopOn = ( 𝑏 ∈ V ↦ { 𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗 } )