Definition df-bases

Description: Define the class of topological bases. Equivalent to definition of basis in Munkres p. 78 (see isbasis2g ). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006)

	Ref	Expression
Assertion	df-bases	$$⊢\mathrm{TopBases}=\left\{x|\forall y\in x\forall z\in xy\cap z\subseteq \bigcup \left(x\cap 𝒫\left(y\cap z\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctb	$$class\mathrm{TopBases}$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3	1	cv	$$setvarx$$
4		vz	$$setvarz$$
5	2	cv	$$setvary$$
6	4	cv	$$setvarz$$
7	5 6	cin	$$class\left(y\cap z\right)$$
8	7	cpw	$$class𝒫\left(y\cap z\right)$$
9	3 8	cin	$$class\left(x\cap 𝒫\left(y\cap z\right)\right)$$
10	9	cuni	$$class\bigcup \left(x\cap 𝒫\left(y\cap z\right)\right)$$
11	7 10	wss	$$wffy\cap z\subseteq \bigcup \left(x\cap 𝒫\left(y\cap z\right)\right)$$
12	11 4 3	wral	$$wff\forall z\in xy\cap z\subseteq \bigcup \left(x\cap 𝒫\left(y\cap z\right)\right)$$
13	12 2 3	wral	$$wff\forall y\in x\forall z\in xy\cap z\subseteq \bigcup \left(x\cap 𝒫\left(y\cap z\right)\right)$$
14	13 1	cab	$$class\left\{x|\forall y\in x\forall z\in xy\cap z\subseteq \bigcup \left(x\cap 𝒫\left(y\cap z\right)\right)\right\}$$
15	0 14	wceq	$$wff\mathrm{TopBases}=\left\{x|\forall y\in x\forall z\in xy\cap z\subseteq \bigcup \left(x\cap 𝒫\left(y\cap z\right)\right)\right\}$$