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

Metamath Proof Explorer

Theorem toponuni

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

Ref Expression
Assertion toponuni 
|- ( J e. ( TopOn ` B ) -> B = U. J )

Proof

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