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	$$⊢\mathrm{Top}\notin \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		pwnex	$$⊢\left\{y|\exists xy=𝒫x\right\}\notin \mathrm{V}$$
2	1	neli	$$⊢\neg \left\{y|\exists xy=𝒫x\right\}\in \mathrm{V}$$
3		distop	$$⊢x\in \mathrm{V}\to 𝒫x\in \mathrm{Top}$$
4	3	elv	$$⊢𝒫x\in \mathrm{Top}$$
5		eleq1	$$⊢y=𝒫x\to \left(y\in \mathrm{Top}\leftrightarrow 𝒫x\in \mathrm{Top}\right)$$
6	4 5	mpbiri	$$⊢y=𝒫x\to y\in \mathrm{Top}$$
7	6	exlimiv	$$⊢\exists xy=𝒫x\to y\in \mathrm{Top}$$
8	7	abssi	$$⊢\left\{y|\exists xy=𝒫x\right\}\subseteq \mathrm{Top}$$
9		ssexg	$$⊢\left(\left\{y|\exists xy=𝒫x\right\}\subseteq \mathrm{Top}\wedge \mathrm{Top}\in \mathrm{V}\right)\to \left\{y|\exists xy=𝒫x\right\}\in \mathrm{V}$$
10	8 9	mpan	$$⊢\mathrm{Top}\in \mathrm{V}\to \left\{y|\exists xy=𝒫x\right\}\in \mathrm{V}$$
11	2 10	mto	$$⊢\neg \mathrm{Top}\in \mathrm{V}$$
12	11	nelir	$$⊢\mathrm{Top}\notin \mathrm{V}$$