Theorem indiscld

Description: The closed sets of an indiscrete topology. (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	indiscld	$$⊢\mathrm{Clsd}\left(\left\{\varnothing ,A\right\}\right)=\left\{\varnothing ,A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		indistop	$$⊢\left\{\varnothing ,A\right\}\in \mathrm{Top}$$
2		indisuni	$$⊢\mathrm{I}\left(A\right)=\bigcup \left\{\varnothing ,A\right\}$$
3	2	iscld	$$⊢\left\{\varnothing ,A\right\}\in \mathrm{Top}\to \left(x\in \mathrm{Clsd}\left(\left\{\varnothing ,A\right\}\right)\leftrightarrow \left(x\subseteq \mathrm{I}\left(A\right)\wedge \mathrm{I}\left(A\right)\setminus x\in \left\{\varnothing ,A\right\}\right)\right)$$
4	1 3	ax-mp	$$⊢x\in \mathrm{Clsd}\left(\left\{\varnothing ,A\right\}\right)\leftrightarrow \left(x\subseteq \mathrm{I}\left(A\right)\wedge \mathrm{I}\left(A\right)\setminus x\in \left\{\varnothing ,A\right\}\right)$$
5		simpl	$$⊢\left(x\subseteq \mathrm{I}\left(A\right)\wedge \mathrm{I}\left(A\right)\setminus x\in \left\{\varnothing ,A\right\}\right)\to x\subseteq \mathrm{I}\left(A\right)$$
6		dfss4	$$⊢x\subseteq \mathrm{I}\left(A\right)\leftrightarrow \mathrm{I}\left(A\right)\setminus \left(\mathrm{I}\left(A\right)\setminus x\right)=x$$
7	5 6	sylib	$$⊢\left(x\subseteq \mathrm{I}\left(A\right)\wedge \mathrm{I}\left(A\right)\setminus x\in \left\{\varnothing ,A\right\}\right)\to \mathrm{I}\left(A\right)\setminus \left(\mathrm{I}\left(A\right)\setminus x\right)=x$$
8		simpr	$$⊢\left(x\subseteq \mathrm{I}\left(A\right)\wedge \mathrm{I}\left(A\right)\setminus x\in \left\{\varnothing ,A\right\}\right)\to \mathrm{I}\left(A\right)\setminus x\in \left\{\varnothing ,A\right\}$$
9		indislem	$$⊢\left\{\varnothing ,\mathrm{I}\left(A\right)\right\}=\left\{\varnothing ,A\right\}$$
10	8 9	eleqtrrdi	$$⊢\left(x\subseteq \mathrm{I}\left(A\right)\wedge \mathrm{I}\left(A\right)\setminus x\in \left\{\varnothing ,A\right\}\right)\to \mathrm{I}\left(A\right)\setminus x\in \left\{\varnothing ,\mathrm{I}\left(A\right)\right\}$$
11		elpri	$$⊢\mathrm{I}\left(A\right)\setminus x\in \left\{\varnothing ,\mathrm{I}\left(A\right)\right\}\to \left(\mathrm{I}\left(A\right)\setminus x=\varnothing \vee \mathrm{I}\left(A\right)\setminus x=\mathrm{I}\left(A\right)\right)$$
12		difeq2	$$⊢\mathrm{I}\left(A\right)\setminus x=\varnothing \to \mathrm{I}\left(A\right)\setminus \left(\mathrm{I}\left(A\right)\setminus x\right)=\mathrm{I}\left(A\right)\setminus \varnothing$$
13		dif0	$$⊢\mathrm{I}\left(A\right)\setminus \varnothing =\mathrm{I}\left(A\right)$$
14	12 13	eqtrdi	$$⊢\mathrm{I}\left(A\right)\setminus x=\varnothing \to \mathrm{I}\left(A\right)\setminus \left(\mathrm{I}\left(A\right)\setminus x\right)=\mathrm{I}\left(A\right)$$
15		fvex	$$⊢\mathrm{I}\left(A\right)\in \mathrm{V}$$
16	15	prid2	$$⊢\mathrm{I}\left(A\right)\in \left\{\varnothing ,\mathrm{I}\left(A\right)\right\}$$
17	16 9	eleqtri	$$⊢\mathrm{I}\left(A\right)\in \left\{\varnothing ,A\right\}$$
18	14 17	eqeltrdi	$$⊢\mathrm{I}\left(A\right)\setminus x=\varnothing \to \mathrm{I}\left(A\right)\setminus \left(\mathrm{I}\left(A\right)\setminus x\right)\in \left\{\varnothing ,A\right\}$$
19		difeq2	$$⊢\mathrm{I}\left(A\right)\setminus x=\mathrm{I}\left(A\right)\to \mathrm{I}\left(A\right)\setminus \left(\mathrm{I}\left(A\right)\setminus x\right)=\mathrm{I}\left(A\right)\setminus \mathrm{I}\left(A\right)$$
20		difid	$$⊢\mathrm{I}\left(A\right)\setminus \mathrm{I}\left(A\right)=\varnothing$$
21	19 20	eqtrdi	$$⊢\mathrm{I}\left(A\right)\setminus x=\mathrm{I}\left(A\right)\to \mathrm{I}\left(A\right)\setminus \left(\mathrm{I}\left(A\right)\setminus x\right)=\varnothing$$
22		0ex	$$⊢\varnothing \in \mathrm{V}$$
23	22	prid1	$$⊢\varnothing \in \left\{\varnothing ,A\right\}$$
24	21 23	eqeltrdi	$$⊢\mathrm{I}\left(A\right)\setminus x=\mathrm{I}\left(A\right)\to \mathrm{I}\left(A\right)\setminus \left(\mathrm{I}\left(A\right)\setminus x\right)\in \left\{\varnothing ,A\right\}$$
25	18 24	jaoi	$$⊢\left(\mathrm{I}\left(A\right)\setminus x=\varnothing \vee \mathrm{I}\left(A\right)\setminus x=\mathrm{I}\left(A\right)\right)\to \mathrm{I}\left(A\right)\setminus \left(\mathrm{I}\left(A\right)\setminus x\right)\in \left\{\varnothing ,A\right\}$$
26	10 11 25	3syl	$$⊢\left(x\subseteq \mathrm{I}\left(A\right)\wedge \mathrm{I}\left(A\right)\setminus x\in \left\{\varnothing ,A\right\}\right)\to \mathrm{I}\left(A\right)\setminus \left(\mathrm{I}\left(A\right)\setminus x\right)\in \left\{\varnothing ,A\right\}$$
27	7 26	eqeltrrd	$$⊢\left(x\subseteq \mathrm{I}\left(A\right)\wedge \mathrm{I}\left(A\right)\setminus x\in \left\{\varnothing ,A\right\}\right)\to x\in \left\{\varnothing ,A\right\}$$
28	4 27	sylbi	$$⊢x\in \mathrm{Clsd}\left(\left\{\varnothing ,A\right\}\right)\to x\in \left\{\varnothing ,A\right\}$$
29	28	ssriv	$$⊢\mathrm{Clsd}\left(\left\{\varnothing ,A\right\}\right)\subseteq \left\{\varnothing ,A\right\}$$
30		0cld	$$⊢\left\{\varnothing ,A\right\}\in \mathrm{Top}\to \varnothing \in \mathrm{Clsd}\left(\left\{\varnothing ,A\right\}\right)$$
31	1 30	ax-mp	$$⊢\varnothing \in \mathrm{Clsd}\left(\left\{\varnothing ,A\right\}\right)$$
32	2	topcld	$$⊢\left\{\varnothing ,A\right\}\in \mathrm{Top}\to \mathrm{I}\left(A\right)\in \mathrm{Clsd}\left(\left\{\varnothing ,A\right\}\right)$$
33	1 32	ax-mp	$$⊢\mathrm{I}\left(A\right)\in \mathrm{Clsd}\left(\left\{\varnothing ,A\right\}\right)$$
34		prssi	$$⊢\left(\varnothing \in \mathrm{Clsd}\left(\left\{\varnothing ,A\right\}\right)\wedge \mathrm{I}\left(A\right)\in \mathrm{Clsd}\left(\left\{\varnothing ,A\right\}\right)\right)\to \left\{\varnothing ,\mathrm{I}\left(A\right)\right\}\subseteq \mathrm{Clsd}\left(\left\{\varnothing ,A\right\}\right)$$
35	31 33 34	mp2an	$$⊢\left\{\varnothing ,\mathrm{I}\left(A\right)\right\}\subseteq \mathrm{Clsd}\left(\left\{\varnothing ,A\right\}\right)$$
36	9 35	eqsstrri	$$⊢\left\{\varnothing ,A\right\}\subseteq \mathrm{Clsd}\left(\left\{\varnothing ,A\right\}\right)$$
37	29 36	eqssi	$$⊢\mathrm{Clsd}\left(\left\{\varnothing ,A\right\}\right)=\left\{\varnothing ,A\right\}$$