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

Metamath Proof Explorer

Theorem eltg4i

Description: An open set in a topology generated by a basis is the union of all basic open sets contained in it. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion eltg4i ⊢ A ∈ topGen ⁡ B → A = ⋃ B ∩ 𝒫 A

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ A ∈ topGen ⁡ B → B ∈ dom ⁡ topGen
2 eltg ⊢ B ∈ dom ⁡ topGen → A ∈ topGen ⁡ B ↔ A ⊆ ⋃ B ∩ 𝒫 A
3 1 2 syl ⊢ A ∈ topGen ⁡ B → A ∈ topGen ⁡ B ↔ A ⊆ ⋃ B ∩ 𝒫 A
4 3 ibi ⊢ A ∈ topGen ⁡ B → A ⊆ ⋃ B ∩ 𝒫 A
5 inss2 ⊢ B ∩ 𝒫 A ⊆ 𝒫 A
6 5 unissi ⊢ ⋃ B ∩ 𝒫 A ⊆ ⋃ 𝒫 A
7 unipw ⊢ ⋃ 𝒫 A = A
8 6 7 sseqtri ⊢ ⋃ B ∩ 𝒫 A ⊆ A
9 8 a1i ⊢ A ∈ topGen ⁡ B → ⋃ B ∩ 𝒫 A ⊆ A
10 4 9 eqssd ⊢ A ∈ topGen ⁡ B → A = ⋃ B ∩ 𝒫 A