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

Metamath Proof Explorer

Theorem topontopon

Description: A topology on a set is a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021)

Ref Expression
Assertion topontopon ⊢ J ∈ TopOn ⁡ X → J ∈ TopOn ⁡ ⋃ J

Proof

Step Hyp Ref Expression
1 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
2 toptopon2 ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ ⋃ J
3 1 2 sylib ⊢ J ∈ TopOn ⁡ X → J ∈ TopOn ⁡ ⋃ J