This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ TopBases = \{x \| \forall y \in x \forall z \in x y \cap z \subseteq ⋃ (x \cap 𝒫 (y \cap z))\}$

Detailed syntax breakdown

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