Definition df-top 22878

Description: Define the class of topologies. It is a proper class (see topnex 22980). See istopg 22879 and istop2g 22880 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.)

Assertion

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

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-top

Step	Hyp	Ref	Expression
1		ctop 22877	. 2 class Top
2		vy	. . . . . . . 8 setvar 𝑦
3	2	cv 1546	. . . . . . 7 class 𝑦
4	3	cuni 4839	. . . . . 6 class ∪ 𝑦
5		vx	. . . . . . 7 setvar 𝑥
6	5	cv 1546	. . . . . 6 class 𝑥
7	4, 6	wcel 2119	. . . . 5 wff ∪ 𝑦 ∈ 𝑥
8	6	cpw 4530	. . . . 5 class 𝒫 𝑥
9	7, 2, 8	wral 3053	. . . 4 wff ∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥
10		vz	. . . . . . . . 9 setvar 𝑧
11	10	cv 1546	. . . . . . . 8 class 𝑧
12	3, 11	cin 3882	. . . . . . 7 class (𝑦 ∩ 𝑧)
13	12, 6	wcel 2119	. . . . . 6 wff (𝑦 ∩ 𝑧) ∈ 𝑥
14	13, 10, 6	wral 3053	. . . . 5 wff ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥
15	14, 2, 6	wral 3053	. . . 4 wff ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥
16	9, 15	wa 396	. . 3 wff (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)
17	16, 5	cab 2717	. 2 class {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)}
18	1, 17	wceq 1547	1 wff Top = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)}

This definition is referenced by:  istopg  22879