Metamath Proof Explorer

Theorem pcmplfin

Description: Given a paracompact topology J and an open cover U , there exists an open refinement v that is locally finite. (Contributed by Thierry Arnoux, 31-Jan-2020)

Ref Expression
Hypothesis pcmplfin.x 
|- X = U. J
Assertion pcmplfin 
|- ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) -> E. v e. ~P J ( v e. ( LocFin ` J ) /\ v Ref U ) )

Proof

Step Hyp Ref Expression
1 pcmplfin.x 
 |-  X = U. J
2 ssexg 
 |-  ( ( U C_ J /\ J e. Paracomp ) -> U e. _V )
3 2 ancoms 
 |-  ( ( J e. Paracomp /\ U C_ J ) -> U e. _V )
4 3 3adant3 
 |-  ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) -> U e. _V )
5 simp2 
 |-  ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) -> U C_ J )
6 4 5 elpwd 
 |-  ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) -> U e. ~P J )
7 ispcmp 
 |-  ( J e. Paracomp <-> J e. CovHasRef ( LocFin ` J ) )
8 1 iscref 
 |-  ( J e. CovHasRef ( LocFin ` J ) <-> ( J e. Top /\ A. u e. ~P J ( X = U. u -> E. v e. ( ~P J i^i ( LocFin ` J ) ) v Ref u ) ) )
9 7 8 bitri 
 |-  ( J e. Paracomp <-> ( J e. Top /\ A. u e. ~P J ( X = U. u -> E. v e. ( ~P J i^i ( LocFin ` J ) ) v Ref u ) ) )
10 9 simprbi 
 |-  ( J e. Paracomp -> A. u e. ~P J ( X = U. u -> E. v e. ( ~P J i^i ( LocFin ` J ) ) v Ref u ) )
11 10 3ad2ant1 
 |-  ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) -> A. u e. ~P J ( X = U. u -> E. v e. ( ~P J i^i ( LocFin ` J ) ) v Ref u ) )
12 simp3 
 |-  ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) -> X = U. U )
13 unieq 
 |-  ( u = U -> U. u = U. U )
14 13 eqeq2d 
 |-  ( u = U -> ( X = U. u <-> X = U. U ) )
15 breq2 
 |-  ( u = U -> ( v Ref u <-> v Ref U ) )
16 15 rexbidv 
 |-  ( u = U -> ( E. v e. ( ~P J i^i ( LocFin ` J ) ) v Ref u <-> E. v e. ( ~P J i^i ( LocFin ` J ) ) v Ref U ) )
17 14 16 imbi12d 
 |-  ( u = U -> ( ( X = U. u -> E. v e. ( ~P J i^i ( LocFin ` J ) ) v Ref u ) <-> ( X = U. U -> E. v e. ( ~P J i^i ( LocFin ` J ) ) v Ref U ) ) )
18 17 rspcv 
 |-  ( U e. ~P J -> ( A. u e. ~P J ( X = U. u -> E. v e. ( ~P J i^i ( LocFin ` J ) ) v Ref u ) -> ( X = U. U -> E. v e. ( ~P J i^i ( LocFin ` J ) ) v Ref U ) ) )
19 6 11 12 18 syl3c 
 |-  ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) -> E. v e. ( ~P J i^i ( LocFin ` J ) ) v Ref U )
20 rexin 
 |-  ( E. v e. ( ~P J i^i ( LocFin ` J ) ) v Ref U <-> E. v e. ~P J ( v e. ( LocFin ` J ) /\ v Ref U ) )
21 19 20 sylib 
 |-  ( ( J e. Paracomp /\ U C_ J /\ X = U. U ) -> E. v e. ~P J ( v e. ( LocFin ` J ) /\ v Ref U ) )