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

Metamath Proof Explorer

Theorem eltg3

Description: Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006) (Proof shortened by Mario Carneiro, 30-Aug-2015)

Ref Expression
Assertion eltg3 ⊢ B ∈ V → A ∈ topGen ⁡ B ↔ ∃ x x ⊆ B ∧ A = ⋃ x

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ A ∈ topGen ⁡ B → B ∈ dom ⁡ topGen
2 inex1g ⊢ B ∈ dom ⁡ topGen → B ∩ 𝒫 A ∈ V
3 1 2 syl ⊢ A ∈ topGen ⁡ B → B ∩ 𝒫 A ∈ V
4 eltg4i ⊢ A ∈ topGen ⁡ B → A = ⋃ B ∩ 𝒫 A
5 inss1 ⊢ B ∩ 𝒫 A ⊆ B
6 sseq1 ⊢ x = B ∩ 𝒫 A → x ⊆ B ↔ B ∩ 𝒫 A ⊆ B
7 5 6 mpbiri ⊢ x = B ∩ 𝒫 A → x ⊆ B
8 7 biantrurd ⊢ x = B ∩ 𝒫 A → A = ⋃ x ↔ x ⊆ B ∧ A = ⋃ x
9 unieq ⊢ x = B ∩ 𝒫 A → ⋃ x = ⋃ B ∩ 𝒫 A
10 9 eqeq2d ⊢ x = B ∩ 𝒫 A → A = ⋃ x ↔ A = ⋃ B ∩ 𝒫 A
11 8 10 bitr3d ⊢ x = B ∩ 𝒫 A → x ⊆ B ∧ A = ⋃ x ↔ A = ⋃ B ∩ 𝒫 A
12 3 4 11 spcedv ⊢ A ∈ topGen ⁡ B → ∃ x x ⊆ B ∧ A = ⋃ x
13 eltg3i ⊢ B ∈ V ∧ x ⊆ B → ⋃ x ∈ topGen ⁡ B
14 eleq1 ⊢ A = ⋃ x → A ∈ topGen ⁡ B ↔ ⋃ x ∈ topGen ⁡ B
15 13 14 syl5ibrcom ⊢ B ∈ V ∧ x ⊆ B → A = ⋃ x → A ∈ topGen ⁡ B
16 15 expimpd ⊢ B ∈ V → x ⊆ B ∧ A = ⋃ x → A ∈ topGen ⁡ B
17 16 exlimdv ⊢ B ∈ V → ∃ x x ⊆ B ∧ A = ⋃ x → A ∈ topGen ⁡ B
18 12 17 impbid2 ⊢ B ∈ V → A ∈ topGen ⁡ B ↔ ∃ x x ⊆ B ∧ A = ⋃ x