Metamath Proof Explorer


Theorem topontop

Description: A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion topontop
|- ( J e. ( TopOn ` B ) -> J e. Top )

Proof

Step Hyp Ref Expression
1 istopon
 |-  ( J e. ( TopOn ` B ) <-> ( J e. Top /\ B = U. J ) )
2 1 simplbi
 |-  ( J e. ( TopOn ` B ) -> J e. Top )