Metamath Proof Explorer

Theorem toponmax

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

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

Proof

Step Hyp Ref Expression
1 toponuni 
 |-  ( J e. ( TopOn ` B ) -> B = U. J )
2 topontop 
 |-  ( J e. ( TopOn ` B ) -> J e. Top )
3 eqid 
 |-  U. J = U. J
4 3 topopn 
 |-  ( J e. Top -> U. J e. J )
5 2 4 syl 
 |-  ( J e. ( TopOn ` B ) -> U. J e. J )
6 1 5 eqeltrd 
 |-  ( J e. ( TopOn ` B ) -> B e. J )