Metamath Proof Explorer

Theorem fiinbas

Description: If a set is closed under finite intersection, then it is a basis for a topology. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion fiinbas ⊢ B ∈ C ∧ ∀ x ∈ B ∀ y ∈ B x ∩ y ∈ B → B ∈ TopBases

Proof

Step Hyp Ref Expression
1 ssid ⊢ x ∩ y ⊆ x ∩ y
2 eleq2 ⊢ w = x ∩ y → z ∈ w ↔ z ∈ x ∩ y
3 sseq1 ⊢ w = x ∩ y → w ⊆ x ∩ y ↔ x ∩ y ⊆ x ∩ y
4 2 3 anbi12d ⊢ w = x ∩ y → z ∈ w ∧ w ⊆ x ∩ y ↔ z ∈ x ∩ y ∧ x ∩ y ⊆ x ∩ y
5 4 rspcev ⊢ x ∩ y ∈ B ∧ z ∈ x ∩ y ∧ x ∩ y ⊆ x ∩ y → ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
6 1 5 mpanr2 ⊢ x ∩ y ∈ B ∧ z ∈ x ∩ y → ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
7 6 ralrimiva ⊢ x ∩ y ∈ B → ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
8 7 a1i ⊢ B ∈ C → x ∩ y ∈ B → ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
9 8 ralimdv ⊢ B ∈ C → ∀ y ∈ B x ∩ y ∈ B → ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
10 9 ralimdv ⊢ B ∈ C → ∀ x ∈ B ∀ y ∈ B x ∩ y ∈ B → ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
11 isbasis2g ⊢ B ∈ C → B ∈ TopBases ↔ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
12 10 11 sylibrd ⊢ B ∈ C → ∀ x ∈ B ∀ y ∈ B x ∩ y ∈ B → B ∈ TopBases
13 12 imp ⊢ B ∈ C ∧ ∀ x ∈ B ∀ y ∈ B x ∩ y ∈ B → B ∈ TopBases