Metamath Proof Explorer


Theorem isbasis3g

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

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

Proof

Step Hyp Ref Expression
1 isbasis2g B C B TopBases x B y B z x y w B z w w x y
2 elssuni x B x B
3 2 rgen x B x B
4 eluni2 x B y B x y
5 4 biimpi x B y B x y
6 5 rgen x B y B x y
7 3 6 pm3.2i x B x B x B y B x y
8 7 biantrur x B y B z x y w B z w w x y x B x B x B y B x y x B y B z x y w B z w w x y
9 df-3an x B x B x B y B x y x B y B z x y w B z w w x y x B x B x B y B x y x B y B z x y w B z w w x y
10 8 9 bitr4i x B y B z x y w B z w w x y x B x B x B y B x y x B y B z x y w B z w w x y
11 1 10 bitrdi B C B TopBases x B x B x B y B x y x B y B z x y w B z w w x y