This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) → ( topGen ‘ 𝐵 ) = 𝐽 )

Proof

Step Hyp Ref Expression
1 dfss3 ⊢ ( 𝐽 ⊆ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐽 𝑥 ∈ ( topGen ‘ 𝐵 ) )
2 ssexg ⊢ ( ( 𝐵 ⊆ 𝐽 ∧ 𝐽 ∈ Top ) → 𝐵 ∈ V )
3 2 ancoms ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ) → 𝐵 ∈ V )
4 eltg2b ⊢ ( 𝐵 ∈ V → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) )
5 3 4 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ) → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) )
6 5 ralbidv ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ) → ( ∀ 𝑥 ∈ 𝐽 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) )
7 1 6 bitrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ) → ( 𝐽 ⊆ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) )
8 7 biimp3ar ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) → 𝐽 ⊆ ( topGen ‘ 𝐵 ) )
9 basgen ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ 𝐽 ⊆ ( topGen ‘ 𝐵 ) ) → ( topGen ‘ 𝐵 ) = 𝐽 )
10 8 9 syld3an3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) → ( topGen ‘ 𝐵 ) = 𝐽 )