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 | A. y e. x A. z e. x ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctb	|- TopBases
1		vx	|- x
2		vy	|- y
3	1	cv	|- x
4		vz	|- z
5	2	cv	|- y
6	4	cv	|- z
7	5 6	cin	|- ( y i^i z )
8	7	cpw	|- ~P ( y i^i z )
9	3 8	cin	|- ( x i^i ~P ( y i^i z ) )
10	9	cuni	|- U. ( x i^i ~P ( y i^i z ) )
11	7 10	wss	|- ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) )
12	11 4 3	wral	|- A. z e. x ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) )
13	12 2 3	wral	|- A. y e. x A. z e. x ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) )
14	13 1	cab	|- { x | A. y e. x A. z e. x ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) ) }
15	0 14	wceq	|- TopBases = { x | A. y e. x A. z e. x ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) ) }