This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐵 ∈ TopBases ↔ ( topGen ‘ 𝐵 ) ∈ Top )

Proof

Step Hyp Ref Expression
1 tgcl ⊢ ( 𝐵 ∈ TopBases → ( topGen ‘ 𝐵 ) ∈ Top )
2 0opn ⊢ ( ( topGen ‘ 𝐵 ) ∈ Top → ∅ ∈ ( topGen ‘ 𝐵 ) )
3 2 elfvexd ⊢ ( ( topGen ‘ 𝐵 ) ∈ Top → 𝐵 ∈ V )
4 bastg ⊢ ( 𝐵 ∈ V → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
5 3 4 syl ⊢ ( ( topGen ‘ 𝐵 ) ∈ Top → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
6 5 sselda ⊢ ( ( ( topGen ‘ 𝐵 ) ∈ Top ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( topGen ‘ 𝐵 ) )
7 5 sselda ⊢ ( ( ( topGen ‘ 𝐵 ) ∈ Top ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ( topGen ‘ 𝐵 ) )
8 6 7 anim12dan ⊢ ( ( ( topGen ‘ 𝐵 ) ∈ Top ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ∧ 𝑦 ∈ ( topGen ‘ 𝐵 ) ) )
9 inopn ⊢ ( ( ( topGen ‘ 𝐵 ) ∈ Top ∧ 𝑥 ∈ ( topGen ‘ 𝐵 ) ∧ 𝑦 ∈ ( topGen ‘ 𝐵 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( topGen ‘ 𝐵 ) )
10 9 3expb ⊢ ( ( ( topGen ‘ 𝐵 ) ∈ Top ∧ ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ∧ 𝑦 ∈ ( topGen ‘ 𝐵 ) ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( topGen ‘ 𝐵 ) )
11 8 10 syldan ⊢ ( ( ( topGen ‘ 𝐵 ) ∈ Top ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( topGen ‘ 𝐵 ) )
12 tg2 ⊢ ( ( ( 𝑥 ∩ 𝑦 ) ∈ ( topGen ‘ 𝐵 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
13 12 ralrimiva ⊢ ( ( 𝑥 ∩ 𝑦 ) ∈ ( topGen ‘ 𝐵 ) → ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
14 11 13 syl ⊢ ( ( ( topGen ‘ 𝐵 ) ∈ Top ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
15 14 ralrimivva ⊢ ( ( topGen ‘ 𝐵 ) ∈ Top → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
16 isbasis2g ⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
17 3 16 syl ⊢ ( ( topGen ‘ 𝐵 ) ∈ Top → ( 𝐵 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
18 15 17 mpbird ⊢ ( ( topGen ‘ 𝐵 ) ∈ Top → 𝐵 ∈ TopBases )
19 1 18 impbii ⊢ ( 𝐵 ∈ TopBases ↔ ( topGen ‘ 𝐵 ) ∈ Top )