Definition df-bases 13479

Description: Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 13481). 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 13478	. 2 class TopBases
2		vy	. . . . . . . 8 setvar y
3	2	cv 1352	. . . . . . 7 class y
4		vz	. . . . . . . 8 setvar z
5	4	cv 1352	. . . . . . 7 class z
6	3, 5	cin 3128	. . . . . 6 class ( y i^i z )
7		vx	. . . . . . . . 9 setvar x
8	7	cv 1352	. . . . . . . 8 class x
9	6	cpw 3575	. . . . . . . 8 class ~P ( y i^i z )
10	8, 9	cin 3128	. . . . . . 7 class ( x i^i ~P ( y i^i z ) )
11	10	cuni 3809	. . . . . 6 class U. ( x i^i ~P ( y i^i z ) )
12	6, 11	wss 3129	. . . . 5 wff ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) )
13	12, 4, 8	wral 2455	. . . 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 2455	. . 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 2163	. 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 1353	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  13480