Metamath Proof Explorer

Theorem cmppcmp

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

Ref Expression
Assertion cmppcmp 
|- ( J e. Comp -> J e. Paracomp )

Proof

Step Hyp Ref Expression
1 cmptop 
 |-  ( J e. Comp -> J e. Top )
2 cmpcref 
 |-  Comp = CovHasRef Fin
3 2 eleq2i 
 |-  ( J e. Comp <-> J e. CovHasRef Fin )
4 eqid 
 |-  U. J = U. J
5 4 iscref 
 |-  ( J e. CovHasRef Fin <-> ( J e. Top /\ A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P J i^i Fin ) z Ref y ) ) )
6 3 5 bitri 
 |-  ( J e. Comp <-> ( J e. Top /\ A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P J i^i Fin ) z Ref y ) ) )
7 6 simprbi 
 |-  ( J e. Comp -> A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P J i^i Fin ) z Ref y ) )
8 simprl 
 |-  ( ( ( ( J e. Comp /\ y e. ~P J ) /\ U. J = U. y ) /\ ( z e. ( ~P J i^i Fin ) /\ z Ref y ) ) -> z e. ( ~P J i^i Fin ) )
9 elin 
 |-  ( z e. ( ~P J i^i Fin ) <-> ( z e. ~P J /\ z e. Fin ) )
10 8 9 sylib 
 |-  ( ( ( ( J e. Comp /\ y e. ~P J ) /\ U. J = U. y ) /\ ( z e. ( ~P J i^i Fin ) /\ z Ref y ) ) -> ( z e. ~P J /\ z e. Fin ) )
11 10 simpld 
 |-  ( ( ( ( J e. Comp /\ y e. ~P J ) /\ U. J = U. y ) /\ ( z e. ( ~P J i^i Fin ) /\ z Ref y ) ) -> z e. ~P J )
12 1 ad3antrrr 
 |-  ( ( ( ( J e. Comp /\ y e. ~P J ) /\ U. J = U. y ) /\ ( z e. ( ~P J i^i Fin ) /\ z Ref y ) ) -> J e. Top )
13 10 simprd 
 |-  ( ( ( ( J e. Comp /\ y e. ~P J ) /\ U. J = U. y ) /\ ( z e. ( ~P J i^i Fin ) /\ z Ref y ) ) -> z e. Fin )
14 simplr 
 |-  ( ( ( ( J e. Comp /\ y e. ~P J ) /\ U. J = U. y ) /\ ( z e. ( ~P J i^i Fin ) /\ z Ref y ) ) -> U. J = U. y )
15 simprr 
 |-  ( ( ( ( J e. Comp /\ y e. ~P J ) /\ U. J = U. y ) /\ ( z e. ( ~P J i^i Fin ) /\ z Ref y ) ) -> z Ref y )
16 eqid 
 |-  U. z = U. z
17 eqid 
 |-  U. y = U. y
18 16 17 refbas 
 |-  ( z Ref y -> U. y = U. z )
19 15 18 syl 
 |-  ( ( ( ( J e. Comp /\ y e. ~P J ) /\ U. J = U. y ) /\ ( z e. ( ~P J i^i Fin ) /\ z Ref y ) ) -> U. y = U. z )
20 14 19 eqtrd 
 |-  ( ( ( ( J e. Comp /\ y e. ~P J ) /\ U. J = U. y ) /\ ( z e. ( ~P J i^i Fin ) /\ z Ref y ) ) -> U. J = U. z )
21 4 16 finlocfin 
 |-  ( ( J e. Top /\ z e. Fin /\ U. J = U. z ) -> z e. ( LocFin ` J ) )
22 12 13 20 21 syl3anc 
 |-  ( ( ( ( J e. Comp /\ y e. ~P J ) /\ U. J = U. y ) /\ ( z e. ( ~P J i^i Fin ) /\ z Ref y ) ) -> z e. ( LocFin ` J ) )
23 11 22 elind 
 |-  ( ( ( ( J e. Comp /\ y e. ~P J ) /\ U. J = U. y ) /\ ( z e. ( ~P J i^i Fin ) /\ z Ref y ) ) -> z e. ( ~P J i^i ( LocFin ` J ) ) )
24 23 15 jca 
 |-  ( ( ( ( J e. Comp /\ y e. ~P J ) /\ U. J = U. y ) /\ ( z e. ( ~P J i^i Fin ) /\ z Ref y ) ) -> ( z e. ( ~P J i^i ( LocFin ` J ) ) /\ z Ref y ) )
25 24 ex 
 |-  ( ( ( J e. Comp /\ y e. ~P J ) /\ U. J = U. y ) -> ( ( z e. ( ~P J i^i Fin ) /\ z Ref y ) -> ( z e. ( ~P J i^i ( LocFin ` J ) ) /\ z Ref y ) ) )
26 25 reximdv2 
 |-  ( ( ( J e. Comp /\ y e. ~P J ) /\ U. J = U. y ) -> ( E. z e. ( ~P J i^i Fin ) z Ref y -> E. z e. ( ~P J i^i ( LocFin ` J ) ) z Ref y ) )
27 26 ex 
 |-  ( ( J e. Comp /\ y e. ~P J ) -> ( U. J = U. y -> ( E. z e. ( ~P J i^i Fin ) z Ref y -> E. z e. ( ~P J i^i ( LocFin ` J ) ) z Ref y ) ) )
28 27 a2d 
 |-  ( ( J e. Comp /\ y e. ~P J ) -> ( ( U. J = U. y -> E. z e. ( ~P J i^i Fin ) z Ref y ) -> ( U. J = U. y -> E. z e. ( ~P J i^i ( LocFin ` J ) ) z Ref y ) ) )
29 28 ralimdva 
 |-  ( J e. Comp -> ( A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P J i^i Fin ) z Ref y ) -> A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P J i^i ( LocFin ` J ) ) z Ref y ) ) )
30 7 29 mpd 
 |-  ( J e. Comp -> A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P J i^i ( LocFin ` J ) ) z Ref y ) )
31 ispcmp 
 |-  ( J e. Paracomp <-> J e. CovHasRef ( LocFin ` J ) )
32 4 iscref 
 |-  ( J e. CovHasRef ( LocFin ` J ) <-> ( J e. Top /\ A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P J i^i ( LocFin ` J ) ) z Ref y ) ) )
33 31 32 bitri 
 |-  ( J e. Paracomp <-> ( J e. Top /\ A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P J i^i ( LocFin ` J ) ) z Ref y ) ) )
34 1 30 33 sylanbrc 
 |-  ( J e. Comp -> J e. Paracomp )