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 ∉ V

Proof

Step	Hyp	Ref	Expression
1		pwnex	⊢ { 𝑦 ∣ ∃ 𝑥 𝑦 = 𝒫 𝑥 } ∉ V
2	1	neli	⊢ ¬ { 𝑦 ∣ ∃ 𝑥 𝑦 = 𝒫 𝑥 } ∈ V
3		distop	⊢ ( 𝑥 ∈ V → 𝒫 𝑥 ∈ Top )
4	3	elv	⊢ 𝒫 𝑥 ∈ Top
5		eleq1	⊢ ( 𝑦 = 𝒫 𝑥 → ( 𝑦 ∈ Top ↔ 𝒫 𝑥 ∈ Top ) )
6	4 5	mpbiri	⊢ ( 𝑦 = 𝒫 𝑥 → 𝑦 ∈ Top )
7	6	exlimiv	⊢ ( ∃ 𝑥 𝑦 = 𝒫 𝑥 → 𝑦 ∈ Top )
8	7	abssi	⊢ { 𝑦 ∣ ∃ 𝑥 𝑦 = 𝒫 𝑥 } ⊆ Top
9		ssexg	⊢ ( ( { 𝑦 ∣ ∃ 𝑥 𝑦 = 𝒫 𝑥 } ⊆ Top ∧ Top ∈ V ) → { 𝑦 ∣ ∃ 𝑥 𝑦 = 𝒫 𝑥 } ∈ V )
10	8 9	mpan	⊢ ( Top ∈ V → { 𝑦 ∣ ∃ 𝑥 𝑦 = 𝒫 𝑥 } ∈ V )
11	2 10	mto	⊢ ¬ Top ∈ V
12	11	nelir	⊢ Top ∉ V