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 \notin V$

Proof

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

Metamath Proof Explorer

Theorem topnex

Proof