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