# 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}=\left\{{x}\in 𝒫{A}|\left(¬{A}\setminus {x}\in \mathrm{Fin}\vee \left({x}=\varnothing \vee {x}={A}\right)\right)\right\}$
Assertion topdifinf ${⊢}\left(\left({T}\in \mathrm{TopOn}\left({A}\right)↔{A}\in \mathrm{Fin}\right)\wedge \left({T}\in \mathrm{TopOn}\left({A}\right)\to {T}=\left\{\varnothing ,{A}\right\}\right)\right)$

### Proof

Step Hyp Ref Expression
1 topdifinf.t ${⊢}{T}=\left\{{x}\in 𝒫{A}|\left(¬{A}\setminus {x}\in \mathrm{Fin}\vee \left({x}=\varnothing \vee {x}={A}\right)\right)\right\}$
2 1 topdifinffin ${⊢}{T}\in \mathrm{TopOn}\left({A}\right)\to {A}\in \mathrm{Fin}$
3 1 topdifinfindis ${⊢}{A}\in \mathrm{Fin}\to {T}=\left\{\varnothing ,{A}\right\}$
4 indistopon ${⊢}{A}\in \mathrm{Fin}\to \left\{\varnothing ,{A}\right\}\in \mathrm{TopOn}\left({A}\right)$
5 3 4 eqeltrd ${⊢}{A}\in \mathrm{Fin}\to {T}\in \mathrm{TopOn}\left({A}\right)$
6 2 5 impbii ${⊢}{T}\in \mathrm{TopOn}\left({A}\right)↔{A}\in \mathrm{Fin}$
7 2 3 syl ${⊢}{T}\in \mathrm{TopOn}\left({A}\right)\to {T}=\left\{\varnothing ,{A}\right\}$
8 6 7 pm3.2i ${⊢}\left(\left({T}\in \mathrm{TopOn}\left({A}\right)↔{A}\in \mathrm{Fin}\right)\wedge \left({T}\in \mathrm{TopOn}\left({A}\right)\to {T}=\left\{\varnothing ,{A}\right\}\right)\right)$