Metamath Proof Explorer

Theorem isbasis3g

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

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

Proof

Step Hyp Ref Expression
1 isbasis2g ⊢ B ∈ C → B ∈ TopBases ↔ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
2 elssuni ⊢ x ∈ B → x ⊆ ⋃ B
3 2 rgen ⊢ ∀ x ∈ B x ⊆ ⋃ B
4 eluni2 ⊢ x ∈ ⋃ B ↔ ∃ y ∈ B x ∈ y
5 4 biimpi ⊢ x ∈ ⋃ B → ∃ y ∈ B x ∈ y
6 5 rgen ⊢ ∀ x ∈ ⋃ B ∃ y ∈ B x ∈ y
7 3 6 pm3.2i ⊢ ∀ x ∈ B x ⊆ ⋃ B ∧ ∀ x ∈ ⋃ B ∃ y ∈ B x ∈ y
8 7 biantrur ⊢ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y ↔ ∀ x ∈ B x ⊆ ⋃ B ∧ ∀ x ∈ ⋃ B ∃ y ∈ B x ∈ y ∧ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
9 df-3an ⊢ ∀ x ∈ B x ⊆ ⋃ B ∧ ∀ x ∈ ⋃ B ∃ y ∈ B x ∈ y ∧ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y ↔ ∀ x ∈ B x ⊆ ⋃ B ∧ ∀ x ∈ ⋃ B ∃ y ∈ B x ∈ y ∧ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
10 8 9 bitr4i ⊢ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y ↔ ∀ x ∈ B x ⊆ ⋃ B ∧ ∀ x ∈ ⋃ B ∃ y ∈ B x ∈ y ∧ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y
11 1 10 syl6bb ⊢ B ∈ C → B ∈ TopBases ↔ ∀ x ∈ B x ⊆ ⋃ B ∧ ∀ x ∈ ⋃ B ∃ y ∈ B x ∈ y ∧ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x ∩ y ∃ w ∈ B z ∈ w ∧ w ⊆ x ∩ y