This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∣ 𝑏 = ∪ 𝑗 } )