Metamath Proof Explorer

Theorem eltg

Description: Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

Ref Expression
Assertion eltg ⊢ B ∈ V → A ∈ topGen ⁡ B ↔ A ⊆ ⋃ B ∩ 𝒫 A

Proof

Step Hyp Ref Expression
1 tgval ⊢ B ∈ V → topGen ⁡ B = x | x ⊆ ⋃ B ∩ 𝒫 x
2 1 eleq2d ⊢ B ∈ V → A ∈ topGen ⁡ B ↔ A ∈ x | x ⊆ ⋃ B ∩ 𝒫 x
3 elex ⊢ A ∈ x | x ⊆ ⋃ B ∩ 𝒫 x → A ∈ V
4 3 adantl ⊢ B ∈ V ∧ A ∈ x | x ⊆ ⋃ B ∩ 𝒫 x → A ∈ V
5 inex1g ⊢ B ∈ V → B ∩ 𝒫 A ∈ V
6 5 uniexd ⊢ B ∈ V → ⋃ B ∩ 𝒫 A ∈ V
7 ssexg ⊢ A ⊆ ⋃ B ∩ 𝒫 A ∧ ⋃ B ∩ 𝒫 A ∈ V → A ∈ V
8 6 7 sylan2 ⊢ A ⊆ ⋃ B ∩ 𝒫 A ∧ B ∈ V → A ∈ V
9 8 ancoms ⊢ B ∈ V ∧ A ⊆ ⋃ B ∩ 𝒫 A → A ∈ V
10 id ⊢ x = A → x = A
11 pweq ⊢ x = A → 𝒫 x = 𝒫 A
12 11 ineq2d ⊢ x = A → B ∩ 𝒫 x = B ∩ 𝒫 A
13 12 unieqd ⊢ x = A → ⋃ B ∩ 𝒫 x = ⋃ B ∩ 𝒫 A
14 10 13 sseq12d ⊢ x = A → x ⊆ ⋃ B ∩ 𝒫 x ↔ A ⊆ ⋃ B ∩ 𝒫 A
15 14 elabg ⊢ A ∈ V → A ∈ x | x ⊆ ⋃ B ∩ 𝒫 x ↔ A ⊆ ⋃ B ∩ 𝒫 A
16 4 9 15 pm5.21nd ⊢ B ∈ V → A ∈ x | x ⊆ ⋃ B ∩ 𝒫 x ↔ A ⊆ ⋃ B ∩ 𝒫 A
17 2 16 bitrd ⊢ B ∈ V → A ∈ topGen ⁡ B ↔ A ⊆ ⋃ B ∩ 𝒫 A