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 ∈ B z ∈ w ∧ w ⊆ x ∩ y
13 12 ralrimiva ⊢ x ∩ y ∈ topGen ⁡ B → ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
14 11 13 syl ⊢ topGen ⁡ B ∈ Top ∧ x ∈ B ∧ y ∈ B → ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
15 14 ralrimivva ⊢ topGen ⁡ B ∈ Top → ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
16 isbasis2g ⊢ B ∈ V → B ∈ TopBases ↔ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
17 3 16 syl ⊢ topGen ⁡ B ∈ Top → B ∈ TopBases ↔ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
18 15 17 mpbird ⊢ topGen ⁡ B ∈ Top → B ∈ TopBases
19 1 18 impbii ⊢ B ∈ TopBases ↔ topGen ⁡ B ∈ Top