Theorem onsucsuccmpi

Description: The successor of a successor ordinal number is a compact topology, proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 18-Oct-2015)

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

Proof

Step	Hyp	Ref	Expression
1		onsucsuccmpi.1	$$⊢A\in \mathrm{On}$$
2	1	onsuci	$$⊢\mathrm{suc}A\in \mathrm{On}$$
3		onsuctop	$$⊢\mathrm{suc}A\in \mathrm{On}\to \mathrm{suc}\mathrm{suc}A\in \mathrm{Top}$$
4	2 3	ax-mp	$$⊢\mathrm{suc}\mathrm{suc}A\in \mathrm{Top}$$
5	1	onirri	$$⊢\neg A\in A$$
6	1 1	onsucssi	$$⊢A\in A\leftrightarrow \mathrm{suc}A\subseteq A$$
7	5 6	mtbi	$$⊢\neg \mathrm{suc}A\subseteq A$$
8		sseq1	$$⊢\mathrm{suc}A=\bigcup y\to \left(\mathrm{suc}A\subseteq A\leftrightarrow \bigcup y\subseteq A\right)$$
9	7 8	mtbii	$$⊢\mathrm{suc}A=\bigcup y\to \neg \bigcup y\subseteq A$$
10		elpwi	$$⊢y\in 𝒫\mathrm{suc}A\to y\subseteq \mathrm{suc}A$$
11	10	unissd	$$⊢y\in 𝒫\mathrm{suc}A\to \bigcup y\subseteq \bigcup \mathrm{suc}A$$
12	1	onunisuci	$$⊢\bigcup \mathrm{suc}A=A$$
13	11 12	sseqtrdi	$$⊢y\in 𝒫\mathrm{suc}A\to \bigcup y\subseteq A$$
14	9 13	nsyl	$$⊢\mathrm{suc}A=\bigcup y\to \neg y\in 𝒫\mathrm{suc}A$$
15		eldif	$$⊢y\in \left(𝒫\left(\mathrm{suc}A\cup \left\{\mathrm{suc}A\right\}\right)\setminus 𝒫\mathrm{suc}A\right)\leftrightarrow \left(y\in 𝒫\left(\mathrm{suc}A\cup \left\{\mathrm{suc}A\right\}\right)\wedge \neg y\in 𝒫\mathrm{suc}A\right)$$
16		elpwunsn	$$⊢y\in \left(𝒫\left(\mathrm{suc}A\cup \left\{\mathrm{suc}A\right\}\right)\setminus 𝒫\mathrm{suc}A\right)\to \mathrm{suc}A\in y$$
17	15 16	sylbir	$$⊢\left(y\in 𝒫\left(\mathrm{suc}A\cup \left\{\mathrm{suc}A\right\}\right)\wedge \neg y\in 𝒫\mathrm{suc}A\right)\to \mathrm{suc}A\in y$$
18	17	ex	$$⊢y\in 𝒫\left(\mathrm{suc}A\cup \left\{\mathrm{suc}A\right\}\right)\to \left(\neg y\in 𝒫\mathrm{suc}A\to \mathrm{suc}A\in y\right)$$
19		df-suc	$$⊢\mathrm{suc}\mathrm{suc}A=\mathrm{suc}A\cup \left\{\mathrm{suc}A\right\}$$
20	19	pweqi	$$⊢𝒫\mathrm{suc}\mathrm{suc}A=𝒫\left(\mathrm{suc}A\cup \left\{\mathrm{suc}A\right\}\right)$$
21	18 20	eleq2s	$$⊢y\in 𝒫\mathrm{suc}\mathrm{suc}A\to \left(\neg y\in 𝒫\mathrm{suc}A\to \mathrm{suc}A\in y\right)$$
22		snelpwi	$$⊢\mathrm{suc}A\in y\to \left\{\mathrm{suc}A\right\}\in 𝒫y$$
23		snfi	$$⊢\left\{\mathrm{suc}A\right\}\in \mathrm{Fin}$$
24	23	jctr	$$⊢\left\{\mathrm{suc}A\right\}\in 𝒫y\to \left(\left\{\mathrm{suc}A\right\}\in 𝒫y\wedge \left\{\mathrm{suc}A\right\}\in \mathrm{Fin}\right)$$
25		elin	$$⊢\left\{\mathrm{suc}A\right\}\in \left(𝒫y\cap \mathrm{Fin}\right)\leftrightarrow \left(\left\{\mathrm{suc}A\right\}\in 𝒫y\wedge \left\{\mathrm{suc}A\right\}\in \mathrm{Fin}\right)$$
26	24 25	sylibr	$$⊢\left\{\mathrm{suc}A\right\}\in 𝒫y\to \left\{\mathrm{suc}A\right\}\in \left(𝒫y\cap \mathrm{Fin}\right)$$
27	2	elexi	$$⊢\mathrm{suc}A\in \mathrm{V}$$
28	27	unisn	$$⊢\bigcup \left\{\mathrm{suc}A\right\}=\mathrm{suc}A$$
29	28	eqcomi	$$⊢\mathrm{suc}A=\bigcup \left\{\mathrm{suc}A\right\}$$
30		unieq	$$⊢z=\left\{\mathrm{suc}A\right\}\to \bigcup z=\bigcup \left\{\mathrm{suc}A\right\}$$
31	30	rspceeqv	$$⊢\left(\left\{\mathrm{suc}A\right\}\in \left(𝒫y\cap \mathrm{Fin}\right)\wedge \mathrm{suc}A=\bigcup \left\{\mathrm{suc}A\right\}\right)\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)\mathrm{suc}A=\bigcup z$$
32	26 29 31	sylancl	$$⊢\left\{\mathrm{suc}A\right\}\in 𝒫y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)\mathrm{suc}A=\bigcup z$$
33	22 32	syl	$$⊢\mathrm{suc}A\in y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)\mathrm{suc}A=\bigcup z$$
34	14 21 33	syl56	$$⊢y\in 𝒫\mathrm{suc}\mathrm{suc}A\to \left(\mathrm{suc}A=\bigcup y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)\mathrm{suc}A=\bigcup z\right)$$
35	34	rgen	$$⊢\forall y\in 𝒫\mathrm{suc}\mathrm{suc}A\left(\mathrm{suc}A=\bigcup y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)\mathrm{suc}A=\bigcup z\right)$$
36	2	onunisuci	$$⊢\bigcup \mathrm{suc}\mathrm{suc}A=\mathrm{suc}A$$
37	36	eqcomi	$$⊢\mathrm{suc}A=\bigcup \mathrm{suc}\mathrm{suc}A$$
38	37	iscmp	$$⊢\mathrm{suc}\mathrm{suc}A\in \mathrm{Comp}\leftrightarrow \left(\mathrm{suc}\mathrm{suc}A\in \mathrm{Top}\wedge \forall y\in 𝒫\mathrm{suc}\mathrm{suc}A\left(\mathrm{suc}A=\bigcup y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)\mathrm{suc}A=\bigcup z\right)\right)$$
39	4 35 38	mpbir2an	$$⊢\mathrm{suc}\mathrm{suc}A\in \mathrm{Comp}$$