Metamath Proof Explorer


Theorem isbasisg

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

Ref Expression
Assertion isbasisg B C B TopBases x B y B x y B 𝒫 x y

Proof

Step Hyp Ref Expression
1 ineq1 z = B z 𝒫 x y = B 𝒫 x y
2 1 unieqd z = B z 𝒫 x y = B 𝒫 x y
3 2 sseq2d z = B x y z 𝒫 x y x y B 𝒫 x y
4 3 raleqbi1dv z = B y z x y z 𝒫 x y y B x y B 𝒫 x y
5 4 raleqbi1dv z = B x z y z x y z 𝒫 x y x B y B x y B 𝒫 x y
6 df-bases TopBases = z | x z y z x y z 𝒫 x y
7 5 6 elab2g B C B TopBases x B y B x y B 𝒫 x y