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

Proof

Step Hyp Ref Expression
1 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
2 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
3 1 2 sylib 
 |-  ( J e. ( TopOn ` X ) -> J e. ( TopOn ` U. J ) )