Definition df-bases 8863

Description: Define the class of all topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 8881). Note that "bases" is the plural of "basis."

Assertion

Ref	Expression
df-bases	|- Bases = {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 8859	. 2 class Bases
2		vy	. . . . . . . 8 set y
3	2	cv 1297	. . . . . . 7 class y
4		vz	. . . . . . . 8 set z
5	4	cv 1297	. . . . . . 7 class z
6	3, 5	cin 2592	. . . . . 6 class (y i^i z)
7		vx	. . . . . . . . 9 set x
8	7	cv 1297	. . . . . . . 8 class x
9	6	cpw 3032	. . . . . . . 8 class ~P(y i^i z)
10	8, 9	cin 2592	. . . . . . 7 class (x i^i ~P(y i^i z))
11	10	cuni 3177	. . . . . 6 class U.(x i^i ~P(y i^i z))
12	6, 11	wss 2593	. . . . 5 wff (y i^i z) C_ U.(x i^i ~P(y i^i z))
13	12, 4, 8	wral 2105	. . . 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 2105	. . 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 1871	. 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 1298	1 wff Bases = {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 8880

Copyright terms: Public domain