Metamath Proof Explorer

Theorem locfincmp

Description: For a compact space, the locally finite covers are precisely the finite covers. Sadly, this property does not properly characterize all compact spaces. (Contributed by Jeff Hankins, 22-Jan-2010) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses locfincmp.1 
|- X = U. J
locfincmp.2 
|- Y = U. C
Assertion locfincmp 
|- ( J e. Comp -> ( C e. ( LocFin ` J ) <-> ( C e. Fin /\ X = Y ) ) )

Proof

Step Hyp Ref Expression
1 locfincmp.1 
 |-  X = U. J
2 locfincmp.2 
 |-  Y = U. C
3 1 locfinnei 
 |-  ( ( C e. ( LocFin ` J ) /\ x e. X ) -> E. o e. J ( x e. o /\ { s e. C | ( s i^i o ) =/= (/) } e. Fin ) )
4 3 ralrimiva 
 |-  ( C e. ( LocFin ` J ) -> A. x e. X E. o e. J ( x e. o /\ { s e. C | ( s i^i o ) =/= (/) } e. Fin ) )
5 1 cmpcov2 
 |-  ( ( J e. Comp /\ A. x e. X E. o e. J ( x e. o /\ { s e. C | ( s i^i o ) =/= (/) } e. Fin ) ) -> E. c e. ( ~P J i^i Fin ) ( X = U. c /\ A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin ) )
6 4 5 sylan2 
 |-  ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> E. c e. ( ~P J i^i Fin ) ( X = U. c /\ A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin ) )
7 elfpw 
 |-  ( c e. ( ~P J i^i Fin ) <-> ( c C_ J /\ c e. Fin ) )
8 simplrr 
 |-  ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) -> c e. Fin )
9 eldifsn 
 |-  ( x e. ( C \ { (/) } ) <-> ( x e. C /\ x =/= (/) ) )
10 ineq1 
 |-  ( s = x -> ( s i^i o ) = ( x i^i o ) )
11 10 neeq1d 
 |-  ( s = x -> ( ( s i^i o ) =/= (/) <-> ( x i^i o ) =/= (/) ) )
12 simplrl 
 |-  ( ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) /\ ( o e. c /\ y e. o ) ) -> x e. C )
13 simplrr 
 |-  ( ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) /\ ( o e. c /\ y e. o ) ) -> y e. x )
14 simprr 
 |-  ( ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) /\ ( o e. c /\ y e. o ) ) -> y e. o )
15 inelcm 
 |-  ( ( y e. x /\ y e. o ) -> ( x i^i o ) =/= (/) )
16 13 14 15 syl2anc 
 |-  ( ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) /\ ( o e. c /\ y e. o ) ) -> ( x i^i o ) =/= (/) )
17 11 12 16 elrabd 
 |-  ( ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) /\ ( o e. c /\ y e. o ) ) -> x e. { s e. C | ( s i^i o ) =/= (/) } )
18 elunii 
 |-  ( ( y e. x /\ x e. C ) -> y e. U. C )
19 18 2 eleqtrrdi 
 |-  ( ( y e. x /\ x e. C ) -> y e. Y )
20 19 ancoms 
 |-  ( ( x e. C /\ y e. x ) -> y e. Y )
21 20 adantl 
 |-  ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) -> y e. Y )
22 1 2 locfinbas 
 |-  ( C e. ( LocFin ` J ) -> X = Y )
23 22 adantl 
 |-  ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> X = Y )
24 23 ad3antrrr 
 |-  ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) -> X = Y )
25 21 24 eleqtrrd 
 |-  ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) -> y e. X )
26 simplr 
 |-  ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) -> X = U. c )
27 25 26 eleqtrd 
 |-  ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) -> y e. U. c )
28 eluni2 
 |-  ( y e. U. c <-> E. o e. c y e. o )
29 27 28 sylib 
 |-  ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) -> E. o e. c y e. o )
30 17 29 reximddv 
 |-  ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ ( x e. C /\ y e. x ) ) -> E. o e. c x e. { s e. C | ( s i^i o ) =/= (/) } )
31 30 expr 
 |-  ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ x e. C ) -> ( y e. x -> E. o e. c x e. { s e. C | ( s i^i o ) =/= (/) } ) )
32 31 exlimdv 
 |-  ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ x e. C ) -> ( E. y y e. x -> E. o e. c x e. { s e. C | ( s i^i o ) =/= (/) } ) )
33 n0 
 |-  ( x =/= (/) <-> E. y y e. x )
34 eliun 
 |-  ( x e. U_ o e. c { s e. C | ( s i^i o ) =/= (/) } <-> E. o e. c x e. { s e. C | ( s i^i o ) =/= (/) } )
35 32 33 34 3imtr4g 
 |-  ( ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) /\ x e. C ) -> ( x =/= (/) -> x e. U_ o e. c { s e. C | ( s i^i o ) =/= (/) } ) )
36 35 expimpd 
 |-  ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) -> ( ( x e. C /\ x =/= (/) ) -> x e. U_ o e. c { s e. C | ( s i^i o ) =/= (/) } ) )
37 9 36 syl5bi 
 |-  ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) -> ( x e. ( C \ { (/) } ) -> x e. U_ o e. c { s e. C | ( s i^i o ) =/= (/) } ) )
38 37 ssrdv 
 |-  ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) -> ( C \ { (/) } ) C_ U_ o e. c { s e. C | ( s i^i o ) =/= (/) } )
39 iunfi 
 |-  ( ( c e. Fin /\ A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin ) -> U_ o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin )
40 39 ex 
 |-  ( c e. Fin -> ( A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin -> U_ o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin ) )
41 ssfi 
 |-  ( ( U_ o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin /\ ( C \ { (/) } ) C_ U_ o e. c { s e. C | ( s i^i o ) =/= (/) } ) -> ( C \ { (/) } ) e. Fin )
42 41 expcom 
 |-  ( ( C \ { (/) } ) C_ U_ o e. c { s e. C | ( s i^i o ) =/= (/) } -> ( U_ o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin -> ( C \ { (/) } ) e. Fin ) )
43 40 42 sylan9 
 |-  ( ( c e. Fin /\ ( C \ { (/) } ) C_ U_ o e. c { s e. C | ( s i^i o ) =/= (/) } ) -> ( A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin -> ( C \ { (/) } ) e. Fin ) )
44 8 38 43 syl2anc 
 |-  ( ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) /\ X = U. c ) -> ( A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin -> ( C \ { (/) } ) e. Fin ) )
45 44 expimpd 
 |-  ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ ( c C_ J /\ c e. Fin ) ) -> ( ( X = U. c /\ A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin ) -> ( C \ { (/) } ) e. Fin ) )
46 7 45 sylan2b 
 |-  ( ( ( J e. Comp /\ C e. ( LocFin ` J ) ) /\ c e. ( ~P J i^i Fin ) ) -> ( ( X = U. c /\ A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin ) -> ( C \ { (/) } ) e. Fin ) )
47 46 rexlimdva 
 |-  ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> ( E. c e. ( ~P J i^i Fin ) ( X = U. c /\ A. o e. c { s e. C | ( s i^i o ) =/= (/) } e. Fin ) -> ( C \ { (/) } ) e. Fin ) )
48 6 47 mpd 
 |-  ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> ( C \ { (/) } ) e. Fin )
49 snfi 
 |-  { (/) } e. Fin
50 unfi 
 |-  ( ( ( C \ { (/) } ) e. Fin /\ { (/) } e. Fin ) -> ( ( C \ { (/) } ) u. { (/) } ) e. Fin )
51 48 49 50 sylancl 
 |-  ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> ( ( C \ { (/) } ) u. { (/) } ) e. Fin )
52 ssun1 
 |-  C C_ ( C u. { (/) } )
53 undif1 
 |-  ( ( C \ { (/) } ) u. { (/) } ) = ( C u. { (/) } )
54 52 53 sseqtrri 
 |-  C C_ ( ( C \ { (/) } ) u. { (/) } )
55 ssfi 
 |-  ( ( ( ( C \ { (/) } ) u. { (/) } ) e. Fin /\ C C_ ( ( C \ { (/) } ) u. { (/) } ) ) -> C e. Fin )
56 51 54 55 sylancl 
 |-  ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> C e. Fin )
57 56 23 jca 
 |-  ( ( J e. Comp /\ C e. ( LocFin ` J ) ) -> ( C e. Fin /\ X = Y ) )
58 57 ex 
 |-  ( J e. Comp -> ( C e. ( LocFin ` J ) -> ( C e. Fin /\ X = Y ) ) )
59 cmptop 
 |-  ( J e. Comp -> J e. Top )
60 1 2 finlocfin 
 |-  ( ( J e. Top /\ C e. Fin /\ X = Y ) -> C e. ( LocFin ` J ) )
61 60 3expib 
 |-  ( J e. Top -> ( ( C e. Fin /\ X = Y ) -> C e. ( LocFin ` J ) ) )
62 59 61 syl 
 |-  ( J e. Comp -> ( ( C e. Fin /\ X = Y ) -> C e. ( LocFin ` J ) ) )
63 58 62 impbid 
 |-  ( J e. Comp -> ( C e. ( LocFin ` J ) <-> ( C e. Fin /\ X = Y ) ) )