Definition df-topgen 16717

Description: Define a function that converts a basis to its corresponding topology. Equivalent to the definition of a topology generated by a basis in [Munkres] p. 78 (see tgval2 21564). The first use of this definition is tgval 21563 but the token is used in df-pt 16718. See tgval3 21571 for an alternate expression for the value. (Contributed by NM, 16-Jul-2006.)

Assertion

Ref	Expression
df-topgen	⊢ topGen = (𝑥 ∈ V ↦ {𝑦 ∣ 𝑦 ⊆ ∪ (𝑥 ∩ 𝒫 𝑦)})

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-topgen

Step	Hyp	Ref	Expression
1		ctg 16711	. 2 class topGen
2		vx	. . 3 setvar 𝑥
3		cvv 3494	. . 3 class V
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1536	. . . . 5 class 𝑦
6	2	cv 1536	. . . . . . 7 class 𝑥
7	5	cpw 4539	. . . . . . 7 class 𝒫 𝑦
8	6, 7	cin 3935	. . . . . 6 class (𝑥 ∩ 𝒫 𝑦)
9	8	cuni 4838	. . . . 5 class ∪ (𝑥 ∩ 𝒫 𝑦)
10	5, 9	wss 3936	. . . 4 wff 𝑦 ⊆ ∪ (𝑥 ∩ 𝒫 𝑦)
11	10, 4	cab 2799	. . 3 class {𝑦 ∣ 𝑦 ⊆ ∪ (𝑥 ∩ 𝒫 𝑦)}
12	2, 3, 11	cmpt 5146	. 2 class (𝑥 ∈ V ↦ {𝑦 ∣ 𝑦 ⊆ ∪ (𝑥 ∩ 𝒫 𝑦)})
13	1, 12	wceq 1537	1 wff topGen = (𝑥 ∈ V ↦ {𝑦 ∣ 𝑦 ⊆ ∪ (𝑥 ∩ 𝒫 𝑦)})

This definition is referenced by:  tgval  21563