Metamath Proof Explorer

Theorem discmp

Description: A discrete topology is compact iff the base set is finite. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion discmp ${⊢}{A}\in \mathrm{Fin}↔𝒫{A}\in \mathrm{Comp}$

Proof

Step Hyp Ref Expression
1 distop ${⊢}{A}\in \mathrm{Fin}\to 𝒫{A}\in \mathrm{Top}$
2 pwfi ${⊢}{A}\in \mathrm{Fin}↔𝒫{A}\in \mathrm{Fin}$
3 2 biimpi ${⊢}{A}\in \mathrm{Fin}\to 𝒫{A}\in \mathrm{Fin}$
4 1 3 elind ${⊢}{A}\in \mathrm{Fin}\to 𝒫{A}\in \left(\mathrm{Top}\cap \mathrm{Fin}\right)$
5 fincmp ${⊢}𝒫{A}\in \left(\mathrm{Top}\cap \mathrm{Fin}\right)\to 𝒫{A}\in \mathrm{Comp}$
6 4 5 syl ${⊢}{A}\in \mathrm{Fin}\to 𝒫{A}\in \mathrm{Comp}$
7 simpr ${⊢}\left(𝒫{A}\in \mathrm{Comp}\wedge {x}\in {A}\right)\to {x}\in {A}$
8 7 snssd ${⊢}\left(𝒫{A}\in \mathrm{Comp}\wedge {x}\in {A}\right)\to \left\{{x}\right\}\subseteq {A}$
9 snex ${⊢}\left\{{x}\right\}\in \mathrm{V}$
10 9 elpw ${⊢}\left\{{x}\right\}\in 𝒫{A}↔\left\{{x}\right\}\subseteq {A}$
11 8 10 sylibr ${⊢}\left(𝒫{A}\in \mathrm{Comp}\wedge {x}\in {A}\right)\to \left\{{x}\right\}\in 𝒫{A}$
12 11 fmpttd ${⊢}𝒫{A}\in \mathrm{Comp}\to \left({x}\in {A}⟼\left\{{x}\right\}\right):{A}⟶𝒫{A}$
13 12 frnd ${⊢}𝒫{A}\in \mathrm{Comp}\to \mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)\subseteq 𝒫{A}$
14 eqid ${⊢}\left({x}\in {A}⟼\left\{{x}\right\}\right)=\left({x}\in {A}⟼\left\{{x}\right\}\right)$
15 14 rnmpt ${⊢}\mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}=\left\{{x}\right\}\right\}$
16 15 unieqi ${⊢}\bigcup \mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)=\bigcup \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}=\left\{{x}\right\}\right\}$
17 9 dfiun2 ${⊢}\bigcup _{{x}\in {A}}\left\{{x}\right\}=\bigcup \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}=\left\{{x}\right\}\right\}$
18 iunid ${⊢}\bigcup _{{x}\in {A}}\left\{{x}\right\}={A}$
19 16 17 18 3eqtr2ri ${⊢}{A}=\bigcup \mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)$
20 19 a1i ${⊢}𝒫{A}\in \mathrm{Comp}\to {A}=\bigcup \mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)$
21 unipw ${⊢}\bigcup 𝒫{A}={A}$
22 21 eqcomi ${⊢}{A}=\bigcup 𝒫{A}$
23 22 cmpcov ${⊢}\left(𝒫{A}\in \mathrm{Comp}\wedge \mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)\subseteq 𝒫{A}\wedge {A}=\bigcup \mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)\right)\to \exists {y}\in \left(𝒫\mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{A}=\bigcup {y}$
24 13 20 23 mpd3an23 ${⊢}𝒫{A}\in \mathrm{Comp}\to \exists {y}\in \left(𝒫\mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{A}=\bigcup {y}$
25 elinel2 ${⊢}{y}\in \left(𝒫\mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)\cap \mathrm{Fin}\right)\to {y}\in \mathrm{Fin}$
26 elinel1 ${⊢}{y}\in \left(𝒫\mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)\cap \mathrm{Fin}\right)\to {y}\in 𝒫\mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)$
27 26 elpwid ${⊢}{y}\in \left(𝒫\mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)\cap \mathrm{Fin}\right)\to {y}\subseteq \mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)$
28 snfi ${⊢}\left\{{x}\right\}\in \mathrm{Fin}$
29 28 rgenw ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{x}\right\}\in \mathrm{Fin}$
30 14 fmpt ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{x}\right\}\in \mathrm{Fin}↔\left({x}\in {A}⟼\left\{{x}\right\}\right):{A}⟶\mathrm{Fin}$
31 29 30 mpbi ${⊢}\left({x}\in {A}⟼\left\{{x}\right\}\right):{A}⟶\mathrm{Fin}$
32 frn ${⊢}\left({x}\in {A}⟼\left\{{x}\right\}\right):{A}⟶\mathrm{Fin}\to \mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)\subseteq \mathrm{Fin}$
33 31 32 mp1i ${⊢}{y}\in \left(𝒫\mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)\cap \mathrm{Fin}\right)\to \mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)\subseteq \mathrm{Fin}$
34 27 33 sstrd ${⊢}{y}\in \left(𝒫\mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)\cap \mathrm{Fin}\right)\to {y}\subseteq \mathrm{Fin}$
35 unifi ${⊢}\left({y}\in \mathrm{Fin}\wedge {y}\subseteq \mathrm{Fin}\right)\to \bigcup {y}\in \mathrm{Fin}$
36 25 34 35 syl2anc ${⊢}{y}\in \left(𝒫\mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)\cap \mathrm{Fin}\right)\to \bigcup {y}\in \mathrm{Fin}$
37 eleq1 ${⊢}{A}=\bigcup {y}\to \left({A}\in \mathrm{Fin}↔\bigcup {y}\in \mathrm{Fin}\right)$
38 36 37 syl5ibrcom ${⊢}{y}\in \left(𝒫\mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)\cap \mathrm{Fin}\right)\to \left({A}=\bigcup {y}\to {A}\in \mathrm{Fin}\right)$
39 38 rexlimiv ${⊢}\exists {y}\in \left(𝒫\mathrm{ran}\left({x}\in {A}⟼\left\{{x}\right\}\right)\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{A}=\bigcup {y}\to {A}\in \mathrm{Fin}$
40 24 39 syl ${⊢}𝒫{A}\in \mathrm{Comp}\to {A}\in \mathrm{Fin}$
41 6 40 impbii ${⊢}{A}\in \mathrm{Fin}↔𝒫{A}\in \mathrm{Comp}$