Metamath Proof Explorer

Theorem isbasis2g

Description: Express the predicate "the set B is a basis for a topology". (Contributed by NM, 17-Jul-2006)

Ref Expression
Assertion isbasis2g ⊢ B ∈ C → B ∈ TopBases ↔ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y

Proof

Step Hyp Ref Expression
1 isbasisg ⊢ B ∈ C → B ∈ TopBases ↔ ∀ x ∈ B ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
2 dfss3 ⊢ x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y ↔ ∀ z ∈ x ∩ y z ∈ ⋃ B ∩ 𝒫 x ∩ y
3 elin ⊢ w ∈ B ∩ 𝒫 x ∩ y ↔ w ∈ B ∧ w ∈ 𝒫 x ∩ y
4 velpw ⊢ w ∈ 𝒫 x ∩ y ↔ w ⊆ x ∩ y
5 4 anbi2i ⊢ w ∈ B ∧ w ∈ 𝒫 x ∩ y ↔ w ∈ B ∧ w ⊆ x ∩ y
6 3 5 bitri ⊢ w ∈ B ∩ 𝒫 x ∩ y ↔ w ∈ B ∧ w ⊆ x ∩ y
7 6 anbi2i ⊢ z ∈ w ∧ w ∈ B ∩ 𝒫 x ∩ y ↔ z ∈ w ∧ w ∈ B ∧ w ⊆ x ∩ y
8 an12 ⊢ z ∈ w ∧ w ∈ B ∧ w ⊆ x ∩ y ↔ w ∈ B ∧ z ∈ w ∧ w ⊆ x ∩ y
9 7 8 bitri ⊢ z ∈ w ∧ w ∈ B ∩ 𝒫 x ∩ y ↔ w ∈ B ∧ z ∈ w ∧ w ⊆ x ∩ y
10 9 exbii ⊢ ∃ w z ∈ w ∧ w ∈ B ∩ 𝒫 x ∩ y ↔ ∃ w w ∈ B ∧ z ∈ w ∧ w ⊆ x ∩ y
11 eluni ⊢ z ∈ ⋃ B ∩ 𝒫 x ∩ y ↔ ∃ w z ∈ w ∧ w ∈ B ∩ 𝒫 x ∩ y
12 df-rex ⊢ ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y ↔ ∃ w w ∈ B ∧ z ∈ w ∧ w ⊆ x ∩ y
13 10 11 12 3bitr4i ⊢ z ∈ ⋃ B ∩ 𝒫 x ∩ y ↔ ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
14 13 ralbii ⊢ ∀ z ∈ x ∩ y z ∈ ⋃ B ∩ 𝒫 x ∩ y ↔ ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
15 2 14 bitri ⊢ x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y ↔ ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
16 15 2ralbii ⊢ ∀ x ∈ B ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y ↔ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
17 1 16 syl6bb ⊢ B ∈ C → B ∈ TopBases ↔ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y