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 )