Definition df-topgen

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 ). The first use of this definition is tgval but the token is used in df-pt . See tgval3 for an alternate expression for the value. (Contributed by NM, 16-Jul-2006)

	Ref	Expression
Assertion	df-topgen	$$⊢\mathrm{topGen}=\left(x\in \mathrm{V}⟼\left\{y|y\subseteq \bigcup \left(x\cap 𝒫y\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctg	$$class\mathrm{topGen}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vy	$$setvary$$
4	3	cv	$$setvary$$
5	1	cv	$$setvarx$$
6	4	cpw	$$class𝒫y$$
7	5 6	cin	$$class\left(x\cap 𝒫y\right)$$
8	7	cuni	$$class\bigcup \left(x\cap 𝒫y\right)$$
9	4 8	wss	$$wffy\subseteq \bigcup \left(x\cap 𝒫y\right)$$
10	9 3	cab	$$class\left\{y|y\subseteq \bigcup \left(x\cap 𝒫y\right)\right\}$$
11	1 2 10	cmpt	$$class\left(x\in \mathrm{V}⟼\left\{y|y\subseteq \bigcup \left(x\cap 𝒫y\right)\right\}\right)$$
12	0 11	wceq	$$wff\mathrm{topGen}=\left(x\in \mathrm{V}⟼\left\{y|y\subseteq \bigcup \left(x\cap 𝒫y\right)\right\}\right)$$