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

Metamath Proof Explorer

Theorem topontop

Description: A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion topontop ⊢ J ∈ TopOn ⁡ B → J ∈ Top

Proof

Step Hyp Ref Expression
1 istopon ⊢ J ∈ TopOn ⁡ B ↔ J ∈ Top ∧ B = ⋃ J
2 1 simplbi ⊢ J ∈ TopOn ⁡ B → J ∈ Top