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

Proof

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