Metamath Proof Explorer

Theorem tgval2

Description: Definition of a topology generated by a basis in Munkres p. 78. Later we show (in tgcl ) that ( topGenB ) is indeed a topology (on U. B , see unitg ). See also tgval and tgval3 . (Contributed by NM, 15-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

Ref Expression
Assertion tgval2 ⊢ B ∈ V → topGen ⁡ B = x | x ⊆ ⋃ B ∧ ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x

Proof

Step Hyp Ref Expression
1 tgval ⊢ B ∈ V → topGen ⁡ B = x | x ⊆ ⋃ B ∩ 𝒫 x
2 inss1 ⊢ B ∩ 𝒫 x ⊆ B
3 2 unissi ⊢ ⋃ B ∩ 𝒫 x ⊆ ⋃ B
4 3 sseli ⊢ y ∈ ⋃ B ∩ 𝒫 x → y ∈ ⋃ B
5 4 pm4.71ri ⊢ y ∈ ⋃ B ∩ 𝒫 x ↔ y ∈ ⋃ B ∧ y ∈ ⋃ B ∩ 𝒫 x
6 5 ralbii ⊢ ∀ y ∈ x y ∈ ⋃ B ∩ 𝒫 x ↔ ∀ y ∈ x y ∈ ⋃ B ∧ y ∈ ⋃ B ∩ 𝒫 x
7 r19.26 ⊢ ∀ y ∈ x y ∈ ⋃ B ∧ y ∈ ⋃ B ∩ 𝒫 x ↔ ∀ y ∈ x y ∈ ⋃ B ∧ ∀ y ∈ x y ∈ ⋃ B ∩ 𝒫 x
8 6 7 bitri ⊢ ∀ y ∈ x y ∈ ⋃ B ∩ 𝒫 x ↔ ∀ y ∈ x y ∈ ⋃ B ∧ ∀ y ∈ x y ∈ ⋃ B ∩ 𝒫 x
9 dfss3 ⊢ x ⊆ ⋃ B ∩ 𝒫 x ↔ ∀ y ∈ x y ∈ ⋃ B ∩ 𝒫 x
10 dfss3 ⊢ x ⊆ ⋃ B ↔ ∀ y ∈ x y ∈ ⋃ B
11 elin ⊢ z ∈ B ∩ 𝒫 x ↔ z ∈ B ∧ z ∈ 𝒫 x
12 11 anbi2i ⊢ y ∈ z ∧ z ∈ B ∩ 𝒫 x ↔ y ∈ z ∧ z ∈ B ∧ z ∈ 𝒫 x
13 an12 ⊢ y ∈ z ∧ z ∈ B ∧ z ∈ 𝒫 x ↔ z ∈ B ∧ y ∈ z ∧ z ∈ 𝒫 x
14 12 13 bitri ⊢ y ∈ z ∧ z ∈ B ∩ 𝒫 x ↔ z ∈ B ∧ y ∈ z ∧ z ∈ 𝒫 x
15 14 exbii ⊢ ∃ z y ∈ z ∧ z ∈ B ∩ 𝒫 x ↔ ∃ z z ∈ B ∧ y ∈ z ∧ z ∈ 𝒫 x
16 eluni ⊢ y ∈ ⋃ B ∩ 𝒫 x ↔ ∃ z y ∈ z ∧ z ∈ B ∩ 𝒫 x
17 df-rex ⊢ ∃ z ∈ B y ∈ z ∧ z ∈ 𝒫 x ↔ ∃ z z ∈ B ∧ y ∈ z ∧ z ∈ 𝒫 x
18 15 16 17 3bitr4i ⊢ y ∈ ⋃ B ∩ 𝒫 x ↔ ∃ z ∈ B y ∈ z ∧ z ∈ 𝒫 x
19 velpw ⊢ z ∈ 𝒫 x ↔ z ⊆ x
20 19 anbi2i ⊢ y ∈ z ∧ z ∈ 𝒫 x ↔ y ∈ z ∧ z ⊆ x
21 20 rexbii ⊢ ∃ z ∈ B y ∈ z ∧ z ∈ 𝒫 x ↔ ∃ z ∈ B y ∈ z ∧ z ⊆ x
22 18 21 bitr2i ⊢ ∃ z ∈ B y ∈ z ∧ z ⊆ x ↔ y ∈ ⋃ B ∩ 𝒫 x
23 22 ralbii ⊢ ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x ↔ ∀ y ∈ x y ∈ ⋃ B ∩ 𝒫 x
24 10 23 anbi12i ⊢ x ⊆ ⋃ B ∧ ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x ↔ ∀ y ∈ x y ∈ ⋃ B ∧ ∀ y ∈ x y ∈ ⋃ B ∩ 𝒫 x
25 8 9 24 3bitr4i ⊢ x ⊆ ⋃ B ∩ 𝒫 x ↔ x ⊆ ⋃ B ∧ ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x
26 25 abbii ⊢ x | x ⊆ ⋃ B ∩ 𝒫 x = x | x ⊆ ⋃ B ∧ ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x
27 1 26 eqtrdi ⊢ B ∈ V → topGen ⁡ B = x | x ⊆ ⋃ B ∧ ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x