Metamath Proof Explorer

Theorem cmppcmp

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

Ref Expression
Assertion cmppcmp ${⊢}{J}\in \mathrm{Comp}\to {J}\in \mathrm{Paracomp}$

Proof

Step Hyp Ref Expression
1 cmptop ${⊢}{J}\in \mathrm{Comp}\to {J}\in \mathrm{Top}$
2 cmpcref ${⊢}\mathrm{Comp}=\mathrm{CovHasRef}\mathrm{Fin}$
3 2 eleq2i ${⊢}{J}\in \mathrm{Comp}↔{J}\in \mathrm{CovHasRef}\mathrm{Fin}$
4 eqid ${⊢}\bigcup {J}=\bigcup {J}$
5 4 iscref ${⊢}{J}\in \mathrm{CovHasRef}\mathrm{Fin}↔\left({J}\in \mathrm{Top}\wedge \forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)\right)$
6 3 5 bitri ${⊢}{J}\in \mathrm{Comp}↔\left({J}\in \mathrm{Top}\wedge \forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)\right)$
7 6 simprbi ${⊢}{J}\in \mathrm{Comp}\to \forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)$
8 simprl ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {y}\in 𝒫{J}\right)\wedge \bigcup {J}=\bigcup {y}\right)\wedge \left({z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\wedge {z}\mathrm{Ref}{y}\right)\right)\to {z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)$
9 elin ${⊢}{z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)↔\left({z}\in 𝒫{J}\wedge {z}\in \mathrm{Fin}\right)$
10 8 9 sylib ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {y}\in 𝒫{J}\right)\wedge \bigcup {J}=\bigcup {y}\right)\wedge \left({z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\wedge {z}\mathrm{Ref}{y}\right)\right)\to \left({z}\in 𝒫{J}\wedge {z}\in \mathrm{Fin}\right)$
11 10 simpld ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {y}\in 𝒫{J}\right)\wedge \bigcup {J}=\bigcup {y}\right)\wedge \left({z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\wedge {z}\mathrm{Ref}{y}\right)\right)\to {z}\in 𝒫{J}$
12 1 ad3antrrr ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {y}\in 𝒫{J}\right)\wedge \bigcup {J}=\bigcup {y}\right)\wedge \left({z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\wedge {z}\mathrm{Ref}{y}\right)\right)\to {J}\in \mathrm{Top}$
13 10 simprd ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {y}\in 𝒫{J}\right)\wedge \bigcup {J}=\bigcup {y}\right)\wedge \left({z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\wedge {z}\mathrm{Ref}{y}\right)\right)\to {z}\in \mathrm{Fin}$
14 simplr ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {y}\in 𝒫{J}\right)\wedge \bigcup {J}=\bigcup {y}\right)\wedge \left({z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\wedge {z}\mathrm{Ref}{y}\right)\right)\to \bigcup {J}=\bigcup {y}$
15 simprr ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {y}\in 𝒫{J}\right)\wedge \bigcup {J}=\bigcup {y}\right)\wedge \left({z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\wedge {z}\mathrm{Ref}{y}\right)\right)\to {z}\mathrm{Ref}{y}$
16 eqid ${⊢}\bigcup {z}=\bigcup {z}$
17 eqid ${⊢}\bigcup {y}=\bigcup {y}$
18 16 17 refbas ${⊢}{z}\mathrm{Ref}{y}\to \bigcup {y}=\bigcup {z}$
19 15 18 syl ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {y}\in 𝒫{J}\right)\wedge \bigcup {J}=\bigcup {y}\right)\wedge \left({z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\wedge {z}\mathrm{Ref}{y}\right)\right)\to \bigcup {y}=\bigcup {z}$
20 14 19 eqtrd ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {y}\in 𝒫{J}\right)\wedge \bigcup {J}=\bigcup {y}\right)\wedge \left({z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\wedge {z}\mathrm{Ref}{y}\right)\right)\to \bigcup {J}=\bigcup {z}$
21 4 16 finlocfin ${⊢}\left({J}\in \mathrm{Top}\wedge {z}\in \mathrm{Fin}\wedge \bigcup {J}=\bigcup {z}\right)\to {z}\in \mathrm{LocFin}\left({J}\right)$
22 12 13 20 21 syl3anc ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {y}\in 𝒫{J}\right)\wedge \bigcup {J}=\bigcup {y}\right)\wedge \left({z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\wedge {z}\mathrm{Ref}{y}\right)\right)\to {z}\in \mathrm{LocFin}\left({J}\right)$
23 11 22 elind ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {y}\in 𝒫{J}\right)\wedge \bigcup {J}=\bigcup {y}\right)\wedge \left({z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\wedge {z}\mathrm{Ref}{y}\right)\right)\to {z}\in \left(𝒫{J}\cap \mathrm{LocFin}\left({J}\right)\right)$
24 23 15 jca ${⊢}\left(\left(\left({J}\in \mathrm{Comp}\wedge {y}\in 𝒫{J}\right)\wedge \bigcup {J}=\bigcup {y}\right)\wedge \left({z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\wedge {z}\mathrm{Ref}{y}\right)\right)\to \left({z}\in \left(𝒫{J}\cap \mathrm{LocFin}\left({J}\right)\right)\wedge {z}\mathrm{Ref}{y}\right)$
25 24 ex ${⊢}\left(\left({J}\in \mathrm{Comp}\wedge {y}\in 𝒫{J}\right)\wedge \bigcup {J}=\bigcup {y}\right)\to \left(\left({z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\wedge {z}\mathrm{Ref}{y}\right)\to \left({z}\in \left(𝒫{J}\cap \mathrm{LocFin}\left({J}\right)\right)\wedge {z}\mathrm{Ref}{y}\right)\right)$
26 25 reximdv2 ${⊢}\left(\left({J}\in \mathrm{Comp}\wedge {y}\in 𝒫{J}\right)\wedge \bigcup {J}=\bigcup {y}\right)\to \left(\exists {z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\to \exists {z}\in \left(𝒫{J}\cap \mathrm{LocFin}\left({J}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)$
27 26 ex ${⊢}\left({J}\in \mathrm{Comp}\wedge {y}\in 𝒫{J}\right)\to \left(\bigcup {J}=\bigcup {y}\to \left(\exists {z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\to \exists {z}\in \left(𝒫{J}\cap \mathrm{LocFin}\left({J}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)\right)$
28 27 a2d ${⊢}\left({J}\in \mathrm{Comp}\wedge {y}\in 𝒫{J}\right)\to \left(\left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)\to \left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{J}\cap \mathrm{LocFin}\left({J}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)\right)$
29 28 ralimdva ${⊢}{J}\in \mathrm{Comp}\to \left(\forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{J}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)\to \forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{J}\cap \mathrm{LocFin}\left({J}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)\right)$
30 7 29 mpd ${⊢}{J}\in \mathrm{Comp}\to \forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{J}\cap \mathrm{LocFin}\left({J}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)$
31 ispcmp ${⊢}{J}\in \mathrm{Paracomp}↔{J}\in \mathrm{CovHasRef}\mathrm{LocFin}\left({J}\right)$
32 4 iscref ${⊢}{J}\in \mathrm{CovHasRef}\mathrm{LocFin}\left({J}\right)↔\left({J}\in \mathrm{Top}\wedge \forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{J}\cap \mathrm{LocFin}\left({J}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)\right)$
33 31 32 bitri ${⊢}{J}\in \mathrm{Paracomp}↔\left({J}\in \mathrm{Top}\wedge \forall {y}\in 𝒫{J}\phantom{\rule{.4em}{0ex}}\left(\bigcup {J}=\bigcup {y}\to \exists {z}\in \left(𝒫{J}\cap \mathrm{LocFin}\left({J}\right)\right)\phantom{\rule{.4em}{0ex}}{z}\mathrm{Ref}{y}\right)\right)$
34 1 30 33 sylanbrc ${⊢}{J}\in \mathrm{Comp}\to {J}\in \mathrm{Paracomp}$