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 ‘ 𝐵 ) = 𝐽 )