Theorem topdifinfindis

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 the trivial topology when A is finite. (Contributed by ML, 14-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	topdifinfindis	$$⊢A\in \mathrm{Fin}\to T=\left\{\varnothing ,A\right\}$$

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		nfv	$$⊢ℲxA\in \mathrm{Fin}$$
3		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in 𝒫A|\left(\neg A\setminus x\in \mathrm{Fin}\vee \left(x=\varnothing \vee x=A\right)\right)\right\}$$
4	1 3	nfcxfr	$$⊢\underset{\_}{Ⅎ}xT$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}x\left\{\varnothing ,A\right\}$$
6		0elpw	$$⊢\varnothing \in 𝒫A$$
7		eleq1a	$$⊢\varnothing \in 𝒫A\to \left(x=\varnothing \to x\in 𝒫A\right)$$
8	6 7	mp1i	$$⊢A\in \mathrm{Fin}\to \left(x=\varnothing \to x\in 𝒫A\right)$$
9		pwidg	$$⊢A\in \mathrm{Fin}\to A\in 𝒫A$$
10		eleq1a	$$⊢A\in 𝒫A\to \left(x=A\to x\in 𝒫A\right)$$
11	9 10	syl	$$⊢A\in \mathrm{Fin}\to \left(x=A\to x\in 𝒫A\right)$$
12	8 11	jaod	$$⊢A\in \mathrm{Fin}\to \left(\left(x=\varnothing \vee x=A\right)\to x\in 𝒫A\right)$$
13	12	pm4.71rd	$$⊢A\in \mathrm{Fin}\to \left(\left(x=\varnothing \vee x=A\right)\leftrightarrow \left(x\in 𝒫A\wedge \left(x=\varnothing \vee x=A\right)\right)\right)$$
14		vex	$$⊢x\in \mathrm{V}$$
15	14	elpr	$$⊢x\in \left\{\varnothing ,A\right\}\leftrightarrow \left(x=\varnothing \vee x=A\right)$$
16	15	a1i	$$⊢A\in \mathrm{Fin}\to \left(x\in \left\{\varnothing ,A\right\}\leftrightarrow \left(x=\varnothing \vee x=A\right)\right)$$
17	1	reqabi	$$⊢x\in T\leftrightarrow \left(x\in 𝒫A\wedge \left(\neg A\setminus x\in \mathrm{Fin}\vee \left(x=\varnothing \vee x=A\right)\right)\right)$$
18		diffi	$$⊢A\in \mathrm{Fin}\to A\setminus x\in \mathrm{Fin}$$
19		biortn	$$⊢A\setminus x\in \mathrm{Fin}\to \left(\left(x=\varnothing \vee x=A\right)\leftrightarrow \left(\neg A\setminus x\in \mathrm{Fin}\vee \left(x=\varnothing \vee x=A\right)\right)\right)$$
20	18 19	syl	$$⊢A\in \mathrm{Fin}\to \left(\left(x=\varnothing \vee x=A\right)\leftrightarrow \left(\neg A\setminus x\in \mathrm{Fin}\vee \left(x=\varnothing \vee x=A\right)\right)\right)$$
21	20	anbi2d	$$⊢A\in \mathrm{Fin}\to \left(\left(x\in 𝒫A\wedge \left(x=\varnothing \vee x=A\right)\right)\leftrightarrow \left(x\in 𝒫A\wedge \left(\neg A\setminus x\in \mathrm{Fin}\vee \left(x=\varnothing \vee x=A\right)\right)\right)\right)$$
22	17 21	bitr4id	$$⊢A\in \mathrm{Fin}\to \left(x\in T\leftrightarrow \left(x\in 𝒫A\wedge \left(x=\varnothing \vee x=A\right)\right)\right)$$
23	13 16 22	3bitr4rd	$$⊢A\in \mathrm{Fin}\to \left(x\in T\leftrightarrow x\in \left\{\varnothing ,A\right\}\right)$$
24	2 4 5 23	eqrd	$$⊢A\in \mathrm{Fin}\to T=\left\{\varnothing ,A\right\}$$