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

Metamath Proof Explorer

Theorem toponmax

Description: The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion toponmax ⊢ J ∈ TopOn ⁡ B → B ∈ J

Proof

Step Hyp Ref Expression
1 toponuni ⊢ J ∈ TopOn ⁡ B → B = ⋃ J
2 topontop ⊢ J ∈ TopOn ⁡ B → J ∈ Top
3 eqid ⊢ ⋃ J = ⋃ J
4 3 topopn ⊢ J ∈ Top → ⋃ J ∈ J
5 2 4 syl ⊢ J ∈ TopOn ⁡ B → ⋃ J ∈ J
6 1 5 eqeltrd ⊢ J ∈ TopOn ⁡ B → B ∈ J