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

Metamath Proof Explorer

Theorem basgen

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 using abbreviations. (Contributed by NM, 22-Jul-2006) (Revised by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion basgen ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ 𝐽 ⊆ ( topGen ‘ 𝐵 ) ) → ( topGen ‘ 𝐵 ) = 𝐽 )

Proof

Step Hyp Ref Expression
1 tgss ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ) → ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐽 ) )
2 1 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ 𝐽 ⊆ ( topGen ‘ 𝐵 ) ) → ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐽 ) )
3 tgtop ⊢ ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) = 𝐽 )
4 3 3ad2ant1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ 𝐽 ⊆ ( topGen ‘ 𝐵 ) ) → ( topGen ‘ 𝐽 ) = 𝐽 )
5 2 4 sseqtrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ 𝐽 ⊆ ( topGen ‘ 𝐵 ) ) → ( topGen ‘ 𝐵 ) ⊆ 𝐽 )
6 simp3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ 𝐽 ⊆ ( topGen ‘ 𝐵 ) ) → 𝐽 ⊆ ( topGen ‘ 𝐵 ) )
7 5 6 eqssd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ 𝐽 ⊆ ( topGen ‘ 𝐵 ) ) → ( topGen ‘ 𝐵 ) = 𝐽 )