Metamath Proof Explorer


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 | y x z x y z x 𝒫 y z

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctb class TopBases
1 vx setvar x
2 vy setvar y
3 1 cv setvar x
4 vz setvar z
5 2 cv setvar y
6 4 cv setvar z
7 5 6 cin class y z
8 7 cpw class 𝒫 y z
9 3 8 cin class x 𝒫 y z
10 9 cuni class x 𝒫 y z
11 7 10 wss wff y z x 𝒫 y z
12 11 4 3 wral wff z x y z x 𝒫 y z
13 12 2 3 wral wff y x z x y z x 𝒫 y z
14 13 1 cab class x | y x z x y z x 𝒫 y z
15 0 14 wceq wff TopBases = x | y x z x y z x 𝒫 y z