Metamath Proof Explorer


Theorem eltg2b

Description: Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014) (Revised by Mario Carneiro, 10-Jan-2015)

Ref Expression
Assertion eltg2b B V A topGen B x A y B x y y A

Proof

Step Hyp Ref Expression
1 eltg2 B V A topGen B A B x A y B x y y A
2 simpl x y y A x y
3 2 reximi y B x y y A y B x y
4 eluni2 x B y B x y
5 3 4 sylibr y B x y y A x B
6 5 ralimi x A y B x y y A x A x B
7 dfss3 A B x A x B
8 6 7 sylibr x A y B x y y A A B
9 8 pm4.71ri x A y B x y y A A B x A y B x y y A
10 1 9 bitr4di B V A topGen B x A y B x y y A