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