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

Metamath Proof Explorer

Theorem toptopon2

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

		Ref	Expression
	Assertion	toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$