Metamath Proof Explorer

Theorem basgen2

Description: Given a topology J , show that a subset B satisfying the third antecedent is a basis for it. Lemma 2.3 of Munkres p. 81. (Contributed by NM, 20-Jul-2006) (Proof shortened by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion basgen2 ⊢ J ∈ Top ∧ B ⊆ J ∧ ∀ x ∈ J ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x → topGen ⁡ B = J

Proof

Step Hyp Ref Expression
1 dfss3 ⊢ J ⊆ topGen ⁡ B ↔ ∀ x ∈ J x ∈ topGen ⁡ B
2 ssexg ⊢ B ⊆ J ∧ J ∈ Top → B ∈ V
3 2 ancoms ⊢ J ∈ Top ∧ B ⊆ J → B ∈ V
4 eltg2b ⊢ B ∈ V → x ∈ topGen ⁡ B ↔ ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x
5 3 4 syl ⊢ J ∈ Top ∧ B ⊆ J → x ∈ topGen ⁡ B ↔ ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x
6 5 ralbidv ⊢ J ∈ Top ∧ B ⊆ J → ∀ x ∈ J x ∈ topGen ⁡ B ↔ ∀ x ∈ J ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x
7 1 6 bitrid ⊢ J ∈ Top ∧ B ⊆ J → J ⊆ topGen ⁡ B ↔ ∀ x ∈ J ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x
8 7 biimp3ar ⊢ J ∈ Top ∧ B ⊆ J ∧ ∀ x ∈ J ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x → J ⊆ topGen ⁡ B
9 basgen ⊢ J ∈ Top ∧ B ⊆ J ∧ J ⊆ topGen ⁡ B → topGen ⁡ B = J
10 8 9 syld3an3 ⊢ J ∈ Top ∧ B ⊆ J ∧ ∀ x ∈ J ∀ y ∈ x ∃ z ∈ B y ∈ z ∧ z ⊆ x → topGen ⁡ B = J