Definition df-topon 20523

Description: Define the set of topologies with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015.)

Assertion

Ref	Expression
df-topon	⊢ TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗})

Distinct variable group:   𝑗,𝑏

Detailed syntax breakdown of Definition df-topon

Step	Hyp	Ref	Expression
1		ctopon 20518	. 2 class TopOn
2		vb	. . 3 setvar 𝑏
3		cvv 3173	. . 3 class V
4	2	cv 1474	. . . . 5 class 𝑏
5		vj	. . . . . . 7 setvar 𝑗
6	5	cv 1474	. . . . . 6 class 𝑗
7	6	cuni 4372	. . . . 5 class ∪ 𝑗
8	4, 7	wceq 1475	. . . 4 wff 𝑏 = ∪ 𝑗
9		ctop 20517	. . . 4 class Top
10	8, 5, 9	crab 2900	. . 3 class {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗}
11	2, 3, 10	cmpt 4643	. 2 class (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗})
12	1, 11	wceq 1475	1 wff TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗})

This definition is referenced by:  istopon  20540  bj-funtopon  32236  bj-toponss  32241  bj-dmtopon  32242