Theorem topdifinffin

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 only if A is finite. (Contributed by ML, 17-Jul-2020)

	Ref	Expression
Hypothesis	topdifinf.t	$$⊢T=\left\{x\in 𝒫A|\left(\neg A\setminus x\in \mathrm{Fin}\vee \left(x=\varnothing \vee x=A\right)\right)\right\}$$
Assertion	topdifinffin	$$⊢T\in \mathrm{TopOn}\left(A\right)\to A\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		topdifinf.t	$$⊢T=\left\{x\in 𝒫A|\left(\neg A\setminus x\in \mathrm{Fin}\vee \left(x=\varnothing \vee x=A\right)\right)\right\}$$
2		difeq2	$$⊢x=y\to A\setminus x=A\setminus y$$
3	2	eleq1d	$$⊢x=y\to \left(A\setminus x\in \mathrm{Fin}\leftrightarrow A\setminus y\in \mathrm{Fin}\right)$$
4	3	notbid	$$⊢x=y\to \left(\neg A\setminus x\in \mathrm{Fin}\leftrightarrow \neg A\setminus y\in \mathrm{Fin}\right)$$
5		eqeq1	$$⊢x=y\to \left(x=\varnothing \leftrightarrow y=\varnothing \right)$$
6		eqeq1	$$⊢x=y\to \left(x=A\leftrightarrow y=A\right)$$
7	5 6	orbi12d	$$⊢x=y\to \left(\left(x=\varnothing \vee x=A\right)\leftrightarrow \left(y=\varnothing \vee y=A\right)\right)$$
8	4 7	orbi12d	$$⊢x=y\to \left(\left(\neg A\setminus x\in \mathrm{Fin}\vee \left(x=\varnothing \vee x=A\right)\right)\leftrightarrow \left(\neg A\setminus y\in \mathrm{Fin}\vee \left(y=\varnothing \vee y=A\right)\right)\right)$$
9	8	cbvrabv	$$⊢\left\{x\in 𝒫A|\left(\neg A\setminus x\in \mathrm{Fin}\vee \left(x=\varnothing \vee x=A\right)\right)\right\}=\left\{y\in 𝒫A|\left(\neg A\setminus y\in \mathrm{Fin}\vee \left(y=\varnothing \vee y=A\right)\right)\right\}$$
10	1 9	eqtri	$$⊢T=\left\{y\in 𝒫A|\left(\neg A\setminus y\in \mathrm{Fin}\vee \left(y=\varnothing \vee y=A\right)\right)\right\}$$
11	10	topdifinffinlem	$$⊢T\in \mathrm{TopOn}\left(A\right)\to A\in \mathrm{Fin}$$