Metamath Proof Explorer

Theorem dispcmp

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

Ref Expression
Assertion dispcmp 
|- ( X e. V -> ~P X e. Paracomp )

Proof

Step Hyp Ref Expression
1 distop 
 |-  ( X e. V -> ~P X e. Top )
2 simpr 
 |-  ( ( x e. X /\ u = { x } ) -> u = { x } )
3 snelpwi 
 |-  ( x e. X -> { x } e. ~P X )
4 3 adantr 
 |-  ( ( x e. X /\ u = { x } ) -> { x } e. ~P X )
5 2 4 eqeltrd 
 |-  ( ( x e. X /\ u = { x } ) -> u e. ~P X )
6 5 rexlimiva 
 |-  ( E. x e. X u = { x } -> u e. ~P X )
7 6 abssi 
 |-  { u | E. x e. X u = { x } } C_ ~P X
8 simpl 
 |-  ( ( u = v /\ x = z ) -> u = v )
9 simpr 
 |-  ( ( u = v /\ x = z ) -> x = z )
10 9 sneqd 
 |-  ( ( u = v /\ x = z ) -> { x } = { z } )
11 8 10 eqeq12d 
 |-  ( ( u = v /\ x = z ) -> ( u = { x } <-> v = { z } ) )
12 11 cbvrexdva 
 |-  ( u = v -> ( E. x e. X u = { x } <-> E. z e. X v = { z } ) )
13 12 cbvabv 
 |-  { u | E. x e. X u = { x } } = { v | E. z e. X v = { z } }
14 13 dissnlocfin 
 |-  ( X e. V -> { u | E. x e. X u = { x } } e. ( LocFin ` ~P X ) )
15 elpwg 
 |-  ( { u | E. x e. X u = { x } } e. ( LocFin ` ~P X ) -> ( { u | E. x e. X u = { x } } e. ~P ~P X <-> { u | E. x e. X u = { x } } C_ ~P X ) )
16 14 15 syl 
 |-  ( X e. V -> ( { u | E. x e. X u = { x } } e. ~P ~P X <-> { u | E. x e. X u = { x } } C_ ~P X ) )
17 7 16 mpbiri 
 |-  ( X e. V -> { u | E. x e. X u = { x } } e. ~P ~P X )
18 17 ad2antrr 
 |-  ( ( ( X e. V /\ y e. ~P ~P X ) /\ X = U. y ) -> { u | E. x e. X u = { x } } e. ~P ~P X )
19 14 ad2antrr 
 |-  ( ( ( X e. V /\ y e. ~P ~P X ) /\ X = U. y ) -> { u | E. x e. X u = { x } } e. ( LocFin ` ~P X ) )
20 18 19 elind 
 |-  ( ( ( X e. V /\ y e. ~P ~P X ) /\ X = U. y ) -> { u | E. x e. X u = { x } } e. ( ~P ~P X i^i ( LocFin ` ~P X ) ) )
21 simpll 
 |-  ( ( ( X e. V /\ y e. ~P ~P X ) /\ X = U. y ) -> X e. V )
22 simpr 
 |-  ( ( ( X e. V /\ y e. ~P ~P X ) /\ X = U. y ) -> X = U. y )
23 22 eqcomd 
 |-  ( ( ( X e. V /\ y e. ~P ~P X ) /\ X = U. y ) -> U. y = X )
24 13 dissnref 
 |-  ( ( X e. V /\ U. y = X ) -> { u | E. x e. X u = { x } } Ref y )
25 21 23 24 syl2anc 
 |-  ( ( ( X e. V /\ y e. ~P ~P X ) /\ X = U. y ) -> { u | E. x e. X u = { x } } Ref y )
26 breq1 
 |-  ( z = { u | E. x e. X u = { x } } -> ( z Ref y <-> { u | E. x e. X u = { x } } Ref y ) )
27 26 rspcev 
 |-  ( ( { u | E. x e. X u = { x } } e. ( ~P ~P X i^i ( LocFin ` ~P X ) ) /\ { u | E. x e. X u = { x } } Ref y ) -> E. z e. ( ~P ~P X i^i ( LocFin ` ~P X ) ) z Ref y )
28 20 25 27 syl2anc 
 |-  ( ( ( X e. V /\ y e. ~P ~P X ) /\ X = U. y ) -> E. z e. ( ~P ~P X i^i ( LocFin ` ~P X ) ) z Ref y )
29 28 ex 
 |-  ( ( X e. V /\ y e. ~P ~P X ) -> ( X = U. y -> E. z e. ( ~P ~P X i^i ( LocFin ` ~P X ) ) z Ref y ) )
30 29 ralrimiva 
 |-  ( X e. V -> A. y e. ~P ~P X ( X = U. y -> E. z e. ( ~P ~P X i^i ( LocFin ` ~P X ) ) z Ref y ) )
31 unipw 
 |-  U. ~P X = X
32 31 eqcomi 
 |-  X = U. ~P X
33 32 iscref 
 |-  ( ~P X e. CovHasRef ( LocFin ` ~P X ) <-> ( ~P X e. Top /\ A. y e. ~P ~P X ( X = U. y -> E. z e. ( ~P ~P X i^i ( LocFin ` ~P X ) ) z Ref y ) ) )
34 1 30 33 sylanbrc 
 |-  ( X e. V -> ~P X e. CovHasRef ( LocFin ` ~P X ) )
35 ispcmp 
 |-  ( ~P X e. Paracomp <-> ~P X e. CovHasRef ( LocFin ` ~P X ) )
36 34 35 sylibr 
 |-  ( X e. V -> ~P X e. Paracomp )