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 e. Top <-> J e. ( TopOn ` U. J ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )