Metamath Proof Explorer


Theorem isbasis2g

Description: Express the predicate "the set B is a basis for a topology". (Contributed by NM, 17-Jul-2006)

Ref Expression
Assertion isbasis2g B C B TopBases x B y B z x y w B z w w x y

Proof

Step Hyp Ref Expression
1 isbasisg B C B TopBases x B y B x y B 𝒫 x y
2 dfss3 x y B 𝒫 x y z x y z B 𝒫 x y
3 elin w B 𝒫 x y w B w 𝒫 x y
4 velpw w 𝒫 x y w x y
5 4 anbi2i w B w 𝒫 x y w B w x y
6 3 5 bitri w B 𝒫 x y w B w x y
7 6 anbi2i z w w B 𝒫 x y z w w B w x y
8 an12 z w w B w x y w B z w w x y
9 7 8 bitri z w w B 𝒫 x y w B z w w x y
10 9 exbii w z w w B 𝒫 x y w w B z w w x y
11 eluni z B 𝒫 x y w z w w B 𝒫 x y
12 df-rex w B z w w x y w w B z w w x y
13 10 11 12 3bitr4i z B 𝒫 x y w B z w w x y
14 13 ralbii z x y z B 𝒫 x y z x y w B z w w x y
15 2 14 bitri x y B 𝒫 x y z x y w B z w w x y
16 15 2ralbii x B y B x y B 𝒫 x y x B y B z x y w B z w w x y
17 1 16 bitrdi B C B TopBases x B y B z x y w B z w w x y