# Metamath Proof Explorer

## Theorem dispcmp

Description: Every discrete space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020)

Ref Expression
Assertion dispcmp ${⊢}{X}\in {V}\to 𝒫{X}\in \mathrm{Paracomp}$

### Proof

Step Hyp Ref Expression
1 distop ${⊢}{X}\in {V}\to 𝒫{X}\in \mathrm{Top}$
2 simpr ${⊢}\left({x}\in {X}\wedge {u}=\left\{{x}\right\}\right)\to {u}=\left\{{x}\right\}$
3 snelpwi ${⊢}{x}\in {X}\to \left\{{x}\right\}\in 𝒫{X}$
4 3 adantr ${⊢}\left({x}\in {X}\wedge {u}=\left\{{x}\right\}\right)\to \left\{{x}\right\}\in 𝒫{X}$
5 2 4 eqeltrd ${⊢}\left({x}\in {X}\wedge {u}=\left\{{x}\right\}\right)\to {u}\in 𝒫{X}$
6 5 rexlimiva ${⊢}\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\to {u}\in 𝒫{X}$
7 6 abssi ${⊢}\left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\subseteq 𝒫{X}$
8 simpl ${⊢}\left({u}={v}\wedge {x}={z}\right)\to {u}={v}$
9 simpr ${⊢}\left({u}={v}\wedge {x}={z}\right)\to {x}={z}$
10 9 sneqd ${⊢}\left({u}={v}\wedge {x}={z}\right)\to \left\{{x}\right\}=\left\{{z}\right\}$
11 8 10 eqeq12d ${⊢}\left({u}={v}\wedge {x}={z}\right)\to \left({u}=\left\{{x}\right\}↔{v}=\left\{{z}\right\}\right)$
12 11 cbvrexdva ${⊢}{u}={v}\to \left(\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}↔\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}{v}=\left\{{z}\right\}\right)$
13 12 cbvabv ${⊢}\left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}=\left\{{v}|\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}{v}=\left\{{z}\right\}\right\}$
14 13 dissnlocfin ${⊢}{X}\in {V}\to \left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\in \mathrm{LocFin}\left(𝒫{X}\right)$
15 elpwg ${⊢}\left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\in \mathrm{LocFin}\left(𝒫{X}\right)\to \left(\left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\in 𝒫𝒫{X}↔\left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\subseteq 𝒫{X}\right)$
16 14 15 syl ${⊢}{X}\in {V}\to \left(\left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\in 𝒫𝒫{X}↔\left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\subseteq 𝒫{X}\right)$
17 7 16 mpbiri ${⊢}{X}\in {V}\to \left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\in 𝒫𝒫{X}$
18 17 ad2antrr ${⊢}\left(\left({X}\in {V}\wedge {y}\in 𝒫𝒫{X}\right)\wedge {X}=\bigcup {y}\right)\to \left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\in 𝒫𝒫{X}$
19 14 ad2antrr ${⊢}\left(\left({X}\in {V}\wedge {y}\in 𝒫𝒫{X}\right)\wedge {X}=\bigcup {y}\right)\to \left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\in \mathrm{LocFin}\left(𝒫{X}\right)$
20 18 19 elind ${⊢}\left(\left({X}\in {V}\wedge {y}\in 𝒫𝒫{X}\right)\wedge {X}=\bigcup {y}\right)\to \left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\in \left(𝒫𝒫{X}\cap \mathrm{LocFin}\left(𝒫{X}\right)\right)$
21 simpll ${⊢}\left(\left({X}\in {V}\wedge {y}\in 𝒫𝒫{X}\right)\wedge {X}=\bigcup {y}\right)\to {X}\in {V}$
22 simpr ${⊢}\left(\left({X}\in {V}\wedge {y}\in 𝒫𝒫{X}\right)\wedge {X}=\bigcup {y}\right)\to {X}=\bigcup {y}$
23 22 eqcomd ${⊢}\left(\left({X}\in {V}\wedge {y}\in 𝒫𝒫{X}\right)\wedge {X}=\bigcup {y}\right)\to \bigcup {y}={X}$
24 13 dissnref ${⊢}\left({X}\in {V}\wedge \bigcup {y}={X}\right)\to \left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\mathrm{Ref}{y}$
25 21 23 24 syl2anc ${⊢}\left(\left({X}\in {V}\wedge {y}\in 𝒫𝒫{X}\right)\wedge {X}=\bigcup {y}\right)\to \left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\mathrm{Ref}{y}$
26 breq1 ${⊢}{z}=\left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\to \left({z}\mathrm{Ref}{y}↔\left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\mathrm{Ref}{y}\right)$
27 26 rspcev ${⊢}\left(\left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\in \left(𝒫𝒫{X}\cap \mathrm{LocFin}\left(𝒫{X}\right)\right)\wedge \left\{{u}|\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{u}=\left\{{x}\right\}\right\}\mathrm{Ref}{y}\right)\to \exists {z}\in \left(𝒫𝒫{X}\cap \mathrm{LocFin}\left(𝒫{X}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}$
28 20 25 27 syl2anc ${⊢}\left(\left({X}\in {V}\wedge {y}\in 𝒫𝒫{X}\right)\wedge {X}=\bigcup {y}\right)\to \exists {z}\in \left(𝒫𝒫{X}\cap \mathrm{LocFin}\left(𝒫{X}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}$
29 28 ex ${⊢}\left({X}\in {V}\wedge {y}\in 𝒫𝒫{X}\right)\to \left({X}=\bigcup {y}\to \exists {z}\in \left(𝒫𝒫{X}\cap \mathrm{LocFin}\left(𝒫{X}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)$
30 29 ralrimiva ${⊢}{X}\in {V}\to \forall {y}\in 𝒫𝒫{X}\phantom{\rule{.4em}{0ex}}\left({X}=\bigcup {y}\to \exists {z}\in \left(𝒫𝒫{X}\cap \mathrm{LocFin}\left(𝒫{X}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)$
31 unipw ${⊢}\bigcup 𝒫{X}={X}$
32 31 eqcomi ${⊢}{X}=\bigcup 𝒫{X}$
33 32 iscref ${⊢}𝒫{X}\in \mathrm{CovHasRef}\mathrm{LocFin}\left(𝒫{X}\right)↔\left(𝒫{X}\in \mathrm{Top}\wedge \forall {y}\in 𝒫𝒫{X}\phantom{\rule{.4em}{0ex}}\left({X}=\bigcup {y}\to \exists {z}\in \left(𝒫𝒫{X}\cap \mathrm{LocFin}\left(𝒫{X}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)\right)$
34 1 30 33 sylanbrc ${⊢}{X}\in {V}\to 𝒫{X}\in \mathrm{CovHasRef}\mathrm{LocFin}\left(𝒫{X}\right)$
35 ispcmp ${⊢}𝒫{X}\in \mathrm{Paracomp}↔𝒫{X}\in \mathrm{CovHasRef}\mathrm{LocFin}\left(𝒫{X}\right)$
36 34 35 sylibr ${⊢}{X}\in {V}\to 𝒫{X}\in \mathrm{Paracomp}$