Definition df-bases 12835

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

Assertion

Ref	Expression
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 ) ) }

Distinct variable group:   x, y, z

Detailed syntax breakdown of Definition df-bases

Step	Hyp	Ref	Expression
1		ctb 12834	. 2 class TopBases
2		vy	. . . . . . . 8 setvar y
3	2	cv 1347	. . . . . . 7 class y
4		vz	. . . . . . . 8 setvar z
5	4	cv 1347	. . . . . . 7 class z
6	3, 5	cin 3120	. . . . . 6 class ( y i^i z )
7		vx	. . . . . . . . 9 setvar x
8	7	cv 1347	. . . . . . . 8 class x
9	6	cpw 3566	. . . . . . . 8 class ~P ( y i^i z )
10	8, 9	cin 3120	. . . . . . 7 class ( x i^i ~P ( y i^i z ) )
11	10	cuni 3796	. . . . . 6 class U. ( x i^i ~P ( y i^i z ) )
12	6, 11	wss 3121	. . . . 5 wff ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) )
13	12, 4, 8	wral 2448	. . . 4 wff A. z e. x ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) )
14	13, 2, 8	wral 2448	. . 3 wff A. y e. x A. z e. x ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) )
15	14, 7	cab 2156	. 2 class { x | A. y e. x A. z e. x ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) ) }
16	1, 15	wceq 1348	1 wff TopBases = { x | A. y e. x A. z e. x ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) ) }

This definition is referenced by:  isbasisg  12836