Metamath Proof Explorer

Theorem topgele

Description: The topologies over the same set have the greatest element (the discrete topology) and the least element (the indiscrete topology). (Contributed by FL, 18-Apr-2010) (Revised by Mario Carneiro, 16-Sep-2015)

Ref Expression
Assertion topgele 
|- ( J e. ( TopOn ` X ) -> ( { (/) , X } C_ J /\ J C_ ~P X ) )

Proof

Step Hyp Ref Expression
1 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
2 0opn 
 |-  ( J e. Top -> (/) e. J )
3 1 2 syl 
 |-  ( J e. ( TopOn ` X ) -> (/) e. J )
4 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
5 3 4 prssd 
 |-  ( J e. ( TopOn ` X ) -> { (/) , X } C_ J )
6 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
7 eqimss2 
 |-  ( X = U. J -> U. J C_ X )
8 6 7 syl 
 |-  ( J e. ( TopOn ` X ) -> U. J C_ X )
9 sspwuni 
 |-  ( J C_ ~P X <-> U. J C_ X )
10 8 9 sylibr 
 |-  ( J e. ( TopOn ` X ) -> J C_ ~P X )
11 5 10 jca 
 |-  ( J e. ( TopOn ` X ) -> ( { (/) , X } C_ J /\ J C_ ~P X ) )