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

Metamath Proof Explorer

Theorem tg1

Description: Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006)

Ref Expression
Assertion tg1 ⊢ A ∈ topGen ⁡ B → A ⊆ ⋃ B

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ A ∈ topGen ⁡ B → B ∈ dom ⁡ topGen
2 eltg2 ⊢ B ∈ dom ⁡ topGen → A ∈ topGen ⁡ B ↔ A ⊆ ⋃ B ∧ ∀ x ∈ A ∃ y ∈ B x ∈ y ∧ y ⊆ A
3 2 simprbda ⊢ B ∈ dom ⁡ topGen ∧ A ∈ topGen ⁡ B → A ⊆ ⋃ B
4 1 3 mpancom ⊢ A ∈ topGen ⁡ B → A ⊆ ⋃ B