# Metamath Proof Explorer

## 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 ${⊢}¬{A}\in {A}$
6 1 1 onsucssi ${⊢}{A}\in {A}↔\mathrm{suc}{A}\subseteq {A}$
7 5 6 mtbi ${⊢}¬\mathrm{suc}{A}\subseteq {A}$
8 sseq1 ${⊢}\mathrm{suc}{A}=\bigcup {y}\to \left(\mathrm{suc}{A}\subseteq {A}↔\bigcup {y}\subseteq {A}\right)$
9 7 8 mtbii ${⊢}\mathrm{suc}{A}=\bigcup {y}\to ¬\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 ¬{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)↔\left({y}\in 𝒫\left(\mathrm{suc}{A}\cup \left\{\mathrm{suc}{A}\right\}\right)\wedge ¬{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 ¬{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(¬{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(¬{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)↔\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)\phantom{\rule{.4em}{0ex}}\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)\phantom{\rule{.4em}{0ex}}\mathrm{suc}{A}=\bigcup {z}$
33 22 32 syl ${⊢}\mathrm{suc}{A}\in {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\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)\phantom{\rule{.4em}{0ex}}\mathrm{suc}{A}=\bigcup {z}\right)$
35 34 rgen ${⊢}\forall {y}\in 𝒫\mathrm{suc}\mathrm{suc}{A}\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{A}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\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}↔\left(\mathrm{suc}\mathrm{suc}{A}\in \mathrm{Top}\wedge \forall {y}\in 𝒫\mathrm{suc}\mathrm{suc}{A}\phantom{\rule{.4em}{0ex}}\left(\mathrm{suc}{A}=\bigcup {y}\to \exists {z}\in \left(𝒫{y}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{suc}{A}=\bigcup {z}\right)\right)$
39 4 35 38 mpbir2an ${⊢}\mathrm{suc}\mathrm{suc}{A}\in \mathrm{Comp}$