Metamath Proof Explorer

Theorem topdifinf

Description: Part of Exercise 3 of Munkres p. 83. The topology of all subsets x of A such that the complement of x in A is infinite, or x is the empty set, or x is all of A , is a topology if and only if A is finite, in which case it is the trivial topology. (Contributed by ML, 17-Jul-2020)

Ref Expression
Hypothesis topdifinf.t ⊢ T = x ∈ 𝒫 A | ¬ A ∖ x ∈ Fin ∨ x = ∅ ∨ x = A
Assertion topdifinf ⊢ T ∈ TopOn ⁡ A ↔ A ∈ Fin ∧ T ∈ TopOn ⁡ A → T = ∅ A

Proof

Step Hyp Ref Expression
1 topdifinf.t ⊢ T = x ∈ 𝒫 A | ¬ A ∖ x ∈ Fin ∨ x = ∅ ∨ x = A
2 1 topdifinffin ⊢ T ∈ TopOn ⁡ A → A ∈ Fin
3 1 topdifinfindis ⊢ A ∈ Fin → T = ∅ A
4 indistopon ⊢ A ∈ Fin → ∅ A ∈ TopOn ⁡ A
5 3 4 eqeltrd ⊢ A ∈ Fin → T ∈ TopOn ⁡ A
6 2 5 impbii ⊢ T ∈ TopOn ⁡ A ↔ A ∈ Fin
7 2 3 syl ⊢ T ∈ TopOn ⁡ A → T = ∅ A
8 6 7 pm3.2i ⊢ T ∈ TopOn ⁡ A ↔ A ∈ Fin ∧ T ∈ TopOn ⁡ A → T = ∅ A