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

Metamath Proof Explorer

Theorem topnex

Description: The class of all topologies is a proper class. The proof uses discrete topologies and pwnex ; an alternate proof uses indiscrete topologies (see indistop ) and the analogue of pwnex with pairs { (/) , x } instead of power sets ~P x (that analogue is also a consequence of abnex ). (Contributed by BJ, 2-May-2021)

Ref Expression
Assertion topnex 
|- Top e/ _V

Proof

Step Hyp Ref Expression
1 pwnex 
 |-  { y | E. x y = ~P x } e/ _V
2 1 neli 
 |-  -. { y | E. x y = ~P x } e. _V
3 distop 
 |-  ( x e. _V -> ~P x e. Top )
4 3 elv 
 |-  ~P x e. Top
5 eleq1 
 |-  ( y = ~P x -> ( y e. Top <-> ~P x e. Top ) )
6 4 5 mpbiri 
 |-  ( y = ~P x -> y e. Top )
7 6 exlimiv 
 |-  ( E. x y = ~P x -> y e. Top )
8 7 abssi 
 |-  { y | E. x y = ~P x } C_ Top
9 ssexg 
 |-  ( ( { y | E. x y = ~P x } C_ Top /\ Top e. _V ) -> { y | E. x y = ~P x } e. _V )
10 8 9 mpan 
 |-  ( Top e. _V -> { y | E. x y = ~P x } e. _V )
11 2 10 mto 
 |-  -. Top e. _V
12 11 nelir 
 |-  Top e/ _V