Metamath Proof Explorer

Theorem locfindis

Description: The locally finite covers of a discrete space are precisely the point-finite covers. (Contributed by Jeff Hankins, 22-Jan-2010) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypothesis locfindis.1 
|- Y = U. C
Assertion locfindis 
|- ( C e. ( LocFin ` ~P X ) <-> ( C e. PtFin /\ X = Y ) )

Proof

Step Hyp Ref Expression
1 locfindis.1 
 |-  Y = U. C
2 lfinpfin 
 |-  ( C e. ( LocFin ` ~P X ) -> C e. PtFin )
3 unipw 
 |-  U. ~P X = X
4 3 eqcomi 
 |-  X = U. ~P X
5 4 1 locfinbas 
 |-  ( C e. ( LocFin ` ~P X ) -> X = Y )
6 2 5 jca 
 |-  ( C e. ( LocFin ` ~P X ) -> ( C e. PtFin /\ X = Y ) )
7 simpr 
 |-  ( ( C e. PtFin /\ X = Y ) -> X = Y )
8 uniexg 
 |-  ( C e. PtFin -> U. C e. _V )
9 1 8 eqeltrid 
 |-  ( C e. PtFin -> Y e. _V )
10 9 adantr 
 |-  ( ( C e. PtFin /\ X = Y ) -> Y e. _V )
11 7 10 eqeltrd 
 |-  ( ( C e. PtFin /\ X = Y ) -> X e. _V )
12 distop 
 |-  ( X e. _V -> ~P X e. Top )
13 11 12 syl 
 |-  ( ( C e. PtFin /\ X = Y ) -> ~P X e. Top )
14 snelpwi 
 |-  ( x e. X -> { x } e. ~P X )
15 14 adantl 
 |-  ( ( ( C e. PtFin /\ X = Y ) /\ x e. X ) -> { x } e. ~P X )
16 snidg 
 |-  ( x e. X -> x e. { x } )
17 16 adantl 
 |-  ( ( ( C e. PtFin /\ X = Y ) /\ x e. X ) -> x e. { x } )
18 simpll 
 |-  ( ( ( C e. PtFin /\ X = Y ) /\ x e. X ) -> C e. PtFin )
19 7 eleq2d 
 |-  ( ( C e. PtFin /\ X = Y ) -> ( x e. X <-> x e. Y ) )
20 19 biimpa 
 |-  ( ( ( C e. PtFin /\ X = Y ) /\ x e. X ) -> x e. Y )
21 1 ptfinfin 
 |-  ( ( C e. PtFin /\ x e. Y ) -> { s e. C | x e. s } e. Fin )
22 18 20 21 syl2anc 
 |-  ( ( ( C e. PtFin /\ X = Y ) /\ x e. X ) -> { s e. C | x e. s } e. Fin )
23 eleq2 
 |-  ( y = { x } -> ( x e. y <-> x e. { x } ) )
24 ineq2 
 |-  ( y = { x } -> ( s i^i y ) = ( s i^i { x } ) )
25 24 neeq1d 
 |-  ( y = { x } -> ( ( s i^i y ) =/= (/) <-> ( s i^i { x } ) =/= (/) ) )
26 disjsn 
 |-  ( ( s i^i { x } ) = (/) <-> -. x e. s )
27 26 necon2abii 
 |-  ( x e. s <-> ( s i^i { x } ) =/= (/) )
28 25 27 bitr4di 
 |-  ( y = { x } -> ( ( s i^i y ) =/= (/) <-> x e. s ) )
29 28 rabbidv 
 |-  ( y = { x } -> { s e. C | ( s i^i y ) =/= (/) } = { s e. C | x e. s } )
30 29 eleq1d 
 |-  ( y = { x } -> ( { s e. C | ( s i^i y ) =/= (/) } e. Fin <-> { s e. C | x e. s } e. Fin ) )
31 23 30 anbi12d 
 |-  ( y = { x } -> ( ( x e. y /\ { s e. C | ( s i^i y ) =/= (/) } e. Fin ) <-> ( x e. { x } /\ { s e. C | x e. s } e. Fin ) ) )
32 31 rspcev 
 |-  ( ( { x } e. ~P X /\ ( x e. { x } /\ { s e. C | x e. s } e. Fin ) ) -> E. y e. ~P X ( x e. y /\ { s e. C | ( s i^i y ) =/= (/) } e. Fin ) )
33 15 17 22 32 syl12anc 
 |-  ( ( ( C e. PtFin /\ X = Y ) /\ x e. X ) -> E. y e. ~P X ( x e. y /\ { s e. C | ( s i^i y ) =/= (/) } e. Fin ) )
34 33 ralrimiva 
 |-  ( ( C e. PtFin /\ X = Y ) -> A. x e. X E. y e. ~P X ( x e. y /\ { s e. C | ( s i^i y ) =/= (/) } e. Fin ) )
35 4 1 islocfin 
 |-  ( C e. ( LocFin ` ~P X ) <-> ( ~P X e. Top /\ X = Y /\ A. x e. X E. y e. ~P X ( x e. y /\ { s e. C | ( s i^i y ) =/= (/) } e. Fin ) ) )
36 13 7 34 35 syl3anbrc 
 |-  ( ( C e. PtFin /\ X = Y ) -> C e. ( LocFin ` ~P X ) )
37 6 36 impbii 
 |-  ( C e. ( LocFin ` ~P X ) <-> ( C e. PtFin /\ X = Y ) )