Definition df-bases 7579

Description: Define the class of all topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 7597). 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) (_ 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 7575	. 2 class Bases
2		vy	. . . . . . . 8 set y
3	2	cv 955	. . . . . . 7 class y
4		vz	. . . . . . . 8 set z
5	4	cv 955	. . . . . . 7 class z
6	3, 5	cin 2046	. . . . . 6 class (y i^i z)
7		vx	. . . . . . . . 9 set x
8	7	cv 955	. . . . . . . 8 class x
9	6	cpw 2401	. . . . . . . 8 class P~(y i^i z)
10	8, 9	cin 2046	. . . . . . 7 class (x i^i P~(y i^i z))
11	10	cuni 2503	. . . . . 6 class U.(x i^i P~(y i^i z))
12	6, 11	wss 2047	. . . . 5 wff (y i^i z) (_ U.(x i^i P~(y i^i z))
13	12, 4, 8	wral 1645	. . . 4 wff A.z e. x (y i^i z) (_ U.(x i^i P~(y i^i z))
14	13, 2, 8	wral 1645	. . 3 wff A.y e. x A.z e. x (y i^i z) (_ U.(x i^i P~(y i^i z))
15	14, 7	cab 1463	. 2 class {x | A.y e. x A.z e. x (y i^i z) (_ U.(x i^i P~(y i^i z))}
16	1, 15	wceq 956	1 wff Bases = {x | A.y e. x A.z e. x (y i^i z) (_ U.(x i^i P~(y i^i z))}

This definition is referenced by:  isbasisg 7596

Copyright terms: Public domain