Theorem onsucconni

Description: A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015)

	Ref	Expression
Hypothesis	onsucconni.1	$$⊢A\in \mathrm{On}$$
Assertion	onsucconni	$$⊢\mathrm{suc}A\in \mathrm{Conn}$$

Proof

Step	Hyp	Ref	Expression
1		onsucconni.1	$$⊢A\in \mathrm{On}$$
2		onsuctop	$$⊢A\in \mathrm{On}\to \mathrm{suc}A\in \mathrm{Top}$$
3	1 2	ax-mp	$$⊢\mathrm{suc}A\in \mathrm{Top}$$
4		elin	$$⊢x\in \left(\mathrm{suc}A\cap \mathrm{Clsd}\left(\mathrm{suc}A\right)\right)\leftrightarrow \left(x\in \mathrm{suc}A\wedge x\in \mathrm{Clsd}\left(\mathrm{suc}A\right)\right)$$
5		elsuci	$$⊢x\in \mathrm{suc}A\to \left(x\in A\vee x=A\right)$$
6	1	onunisuci	$$⊢\bigcup \mathrm{suc}A=A$$
7	6	eqcomi	$$⊢A=\bigcup \mathrm{suc}A$$
8	7	cldopn	$$⊢x\in \mathrm{Clsd}\left(\mathrm{suc}A\right)\to A\setminus x\in \mathrm{suc}A$$
9	1	onsuci	$$⊢\mathrm{suc}A\in \mathrm{On}$$
10	9	oneli	$$⊢A\setminus x\in \mathrm{suc}A\to A\setminus x\in \mathrm{On}$$
11		elndif	$$⊢\varnothing \in x\to \neg \varnothing \in \left(A\setminus x\right)$$
12		on0eln0	$$⊢A\setminus x\in \mathrm{On}\to \left(\varnothing \in \left(A\setminus x\right)\leftrightarrow A\setminus x\ne \varnothing \right)$$
13	12	biimprd	$$⊢A\setminus x\in \mathrm{On}\to \left(A\setminus x\ne \varnothing \to \varnothing \in \left(A\setminus x\right)\right)$$
14	13	necon1bd	$$⊢A\setminus x\in \mathrm{On}\to \left(\neg \varnothing \in \left(A\setminus x\right)\to A\setminus x=\varnothing \right)$$
15		ssdif0	$$⊢A\subseteq x\leftrightarrow A\setminus x=\varnothing$$
16	1	onssneli	$$⊢A\subseteq x\to \neg x\in A$$
17	15 16	sylbir	$$⊢A\setminus x=\varnothing \to \neg x\in A$$
18	11 14 17	syl56	$$⊢A\setminus x\in \mathrm{On}\to \left(\varnothing \in x\to \neg x\in A\right)$$
19	18	con2d	$$⊢A\setminus x\in \mathrm{On}\to \left(x\in A\to \neg \varnothing \in x\right)$$
20	1	oneli	$$⊢x\in A\to x\in \mathrm{On}$$
21		on0eln0	$$⊢x\in \mathrm{On}\to \left(\varnothing \in x\leftrightarrow x\ne \varnothing \right)$$
22	21	biimprd	$$⊢x\in \mathrm{On}\to \left(x\ne \varnothing \to \varnothing \in x\right)$$
23	20 22	syl	$$⊢x\in A\to \left(x\ne \varnothing \to \varnothing \in x\right)$$
24	23	necon1bd	$$⊢x\in A\to \left(\neg \varnothing \in x\to x=\varnothing \right)$$
25	19 24	sylcom	$$⊢A\setminus x\in \mathrm{On}\to \left(x\in A\to x=\varnothing \right)$$
26	10 25	syl	$$⊢A\setminus x\in \mathrm{suc}A\to \left(x\in A\to x=\varnothing \right)$$
27	26	orim1d	$$⊢A\setminus x\in \mathrm{suc}A\to \left(\left(x\in A\vee x=A\right)\to \left(x=\varnothing \vee x=A\right)\right)$$
28	27	impcom	$$⊢\left(\left(x\in A\vee x=A\right)\wedge A\setminus x\in \mathrm{suc}A\right)\to \left(x=\varnothing \vee x=A\right)$$
29		vex	$$⊢x\in \mathrm{V}$$
30	29	elpr	$$⊢x\in \left\{\varnothing ,A\right\}\leftrightarrow \left(x=\varnothing \vee x=A\right)$$
31	28 30	sylibr	$$⊢\left(\left(x\in A\vee x=A\right)\wedge A\setminus x\in \mathrm{suc}A\right)\to x\in \left\{\varnothing ,A\right\}$$
32	5 8 31	syl2an	$$⊢\left(x\in \mathrm{suc}A\wedge x\in \mathrm{Clsd}\left(\mathrm{suc}A\right)\right)\to x\in \left\{\varnothing ,A\right\}$$
33	4 32	sylbi	$$⊢x\in \left(\mathrm{suc}A\cap \mathrm{Clsd}\left(\mathrm{suc}A\right)\right)\to x\in \left\{\varnothing ,A\right\}$$
34	33	ssriv	$$⊢\mathrm{suc}A\cap \mathrm{Clsd}\left(\mathrm{suc}A\right)\subseteq \left\{\varnothing ,A\right\}$$
35	7	isconn2	$$⊢\mathrm{suc}A\in \mathrm{Conn}\leftrightarrow \left(\mathrm{suc}A\in \mathrm{Top}\wedge \mathrm{suc}A\cap \mathrm{Clsd}\left(\mathrm{suc}A\right)\subseteq \left\{\varnothing ,A\right\}\right)$$
36	3 34 35	mpbir2an	$$⊢\mathrm{suc}A\in \mathrm{Conn}$$