Metamath Proof Explorer

Theorem tgclb

Description: The property tgcl can be reversed: if the topology generated by B is actually a topology, then B must be a topological basis. This yields an alternative definition of TopBases . (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion tgclb ⊢B∈TopBases↔topGen⁡B∈Top

Proof

Step Hyp Ref Expression
1 tgcl ⊢B∈TopBases→topGen⁡B∈Top
2 0opn ⊢topGen⁡B∈Top→∅∈topGen⁡B
3 2 elfvexd ⊢topGen⁡B∈Top→B∈V
4 bastg ⊢B∈V→B⊆topGen⁡B
5 3 4 syl ⊢topGen⁡B∈Top→B⊆topGen⁡B
6 5 sselda ⊢topGen⁡B∈Top∧x∈B→x∈topGen⁡B
7 5 sselda ⊢topGen⁡B∈Top∧y∈B→y∈topGen⁡B
8 6 7 anim12dan ⊢topGen⁡B∈Top∧x∈B∧y∈B→x∈topGen⁡B∧y∈topGen⁡B
9 inopn ⊢topGen⁡B∈Top∧x∈topGen⁡B∧y∈topGen⁡B→x∩y∈topGen⁡B
10 9 3expb ⊢topGen⁡B∈Top∧x∈topGen⁡B∧y∈topGen⁡B→x∩y∈topGen⁡B
11 8 10 syldan ⊢topGen⁡B∈Top∧x∈B∧y∈B→x∩y∈topGen⁡B
12 tg2 ⊢x∩y∈topGen⁡B∧z∈x∩y→∃w∈Bz∈w∧w⊆x∩y
13 12 ralrimiva ⊢x∩y∈topGen⁡B→∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y
14 11 13 syl ⊢topGen⁡B∈Top∧x∈B∧y∈B→∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y
15 14 ralrimivva ⊢topGen⁡B∈Top→∀x∈B∀y∈B∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y
16 isbasis2g ⊢B∈V→B∈TopBases↔∀x∈B∀y∈B∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y
17 3 16 syl ⊢topGen⁡B∈Top→B∈TopBases↔∀x∈B∀y∈B∀z∈x∩y∃w∈Bz∈w∧w⊆x∩y
18 15 17 mpbird ⊢topGen⁡B∈Top→B∈TopBases
19 1 18 impbii ⊢B∈TopBases↔topGen⁡B∈Top