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

Metamath Proof Explorer

Theorem toptopon

Description: Alternative definition of Top in terms of TopOn . (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Hypothesis toptopon.1 ⊢ X = ⋃ J
Assertion toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ X

Proof

Step Hyp Ref Expression
1 toptopon.1 ⊢ X = ⋃ J
2 istopon ⊢ J ∈ TopOn ⁡ X ↔ J ∈ Top ∧ X = ⋃ J
3 1 2 mpbiran2 ⊢ J ∈ TopOn ⁡ X ↔ J ∈ Top
4 3 bicomi ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ X