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

Metamath Proof Explorer

Theorem toponcom

Description: If K is a topology on the base set of topology J , then J is a topology on the base of K . (Contributed by Mario Carneiro, 22-Aug-2015)

Ref Expression
Assertion toponcom ⊢ J ∈ Top ∧ K ∈ TopOn ⁡ ⋃ J → J ∈ TopOn ⁡ ⋃ K

Proof

Step Hyp Ref Expression
1 toponuni ⊢ K ∈ TopOn ⁡ ⋃ J → ⋃ J = ⋃ K
2 1 eqcomd ⊢ K ∈ TopOn ⁡ ⋃ J → ⋃ K = ⋃ J
3 2 anim2i ⊢ J ∈ Top ∧ K ∈ TopOn ⁡ ⋃ J → J ∈ Top ∧ ⋃ K = ⋃ J
4 istopon ⊢ J ∈ TopOn ⁡ ⋃ K ↔ J ∈ Top ∧ ⋃ K = ⋃ J
5 3 4 sylibr ⊢ J ∈ Top ∧ K ∈ TopOn ⁡ ⋃ J → J ∈ TopOn ⁡ ⋃ K