Definition df-top

Description: Define the class of topologies. It is a proper class (see topnex ). See istopg and istop2g for the corresponding characterizations, using respectively binary intersections like in this definition and nonempty finite intersections.

The final form of the definition is due to Bourbaki (Def. 1 of BourbakiTop1 p. I.1), while the idea of defining a topology in terms of its open sets is due to Aleksandrov. For the convoluted history of the definitions of these notions, see

Gregory H. Moore,The emergence of open sets, closed sets, and limit points in analysis and topology, Historia Mathematica 35 (2008) 220--241.

(Contributed by NM, 3-Mar-2006) (Revised by BJ, 20-Oct-2018)

	Ref	Expression
Assertion	df-top	⊢ Top = { 𝑥 ∣ ( ∀ 𝑦 ∈ 𝒫 𝑥 ∪ 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ∩ 𝑧 ) ∈ 𝑥 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctop	⊢ Top
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4	3	cpw	⊢ 𝒫 𝑥
5	2	cv	⊢ 𝑦
6	5	cuni	⊢ ∪ 𝑦
7	6 3	wcel	⊢ ∪ 𝑦 ∈ 𝑥
8	7 2 4	wral	⊢ ∀ 𝑦 ∈ 𝒫 𝑥 ∪ 𝑦 ∈ 𝑥
9		vz	⊢ 𝑧
10	9	cv	⊢ 𝑧
11	5 10	cin	⊢ ( 𝑦 ∩ 𝑧 )
12	11 3	wcel	⊢ ( 𝑦 ∩ 𝑧 ) ∈ 𝑥
13	12 9 3	wral	⊢ ∀ 𝑧 ∈ 𝑥 ( 𝑦 ∩ 𝑧 ) ∈ 𝑥
14	13 2 3	wral	⊢ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ∩ 𝑧 ) ∈ 𝑥
15	8 14	wa	⊢ ( ∀ 𝑦 ∈ 𝒫 𝑥 ∪ 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ∩ 𝑧 ) ∈ 𝑥 )
16	15 1	cab	⊢ { 𝑥 ∣ ( ∀ 𝑦 ∈ 𝒫 𝑥 ∪ 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ∩ 𝑧 ) ∈ 𝑥 ) }
17	0 16	wceq	⊢ Top = { 𝑥 ∣ ( ∀ 𝑦 ∈ 𝒫 𝑥 ∪ 𝑦 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ∩ 𝑧 ) ∈ 𝑥 ) }