MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  locfincmp Structured version   Visualization version   Unicode version

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

Proof of Theorem locfincmp
Dummy variables  o 
c  s  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 locfincmp.1 . . . . . . . . . 10  |-  X  = 
U. J
21locfinnei 20593 . . . . . . . . 9  |-  ( ( C  e.  ( LocFin `  J )  /\  x  e.  X )  ->  E. o  e.  J  ( x  e.  o  /\  { s  e.  C  |  ( s  i^i  o )  =/=  (/) }  e.  Fin ) )
32ralrimiva 2814 . . . . . . . 8  |-  ( C  e.  ( LocFin `  J
)  ->  A. x  e.  X  E. o  e.  J  ( x  e.  o  /\  { s  e.  C  |  ( s  i^i  o )  =/=  (/) }  e.  Fin ) )
41cmpcov2 20460 . . . . . . . 8  |-  ( ( 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 ) )
53, 4sylan2 481 . . . . . . 7  |-  ( ( 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 ) )
6 elfpw 7907 . . . . . . . . 9  |-  ( c  e.  ( ~P J  i^i  Fin )  <->  ( c  C_  J  /\  c  e. 
Fin ) )
7 simplrr 776 . . . . . . . . . . 11  |-  ( ( ( ( J  e. 
Comp  /\  C  e.  (
LocFin `  J ) )  /\  ( c  C_  J  /\  c  e.  Fin ) )  /\  X  =  U. c )  -> 
c  e.  Fin )
8 eldifsn 4110 . . . . . . . . . . . . 13  |-  ( x  e.  ( C  \  { (/) } )  <->  ( x  e.  C  /\  x  =/=  (/) ) )
9 simplrl 775 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( 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 )
10 simplrr 776 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( 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 )
11 simprr 771 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( 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 )
12 inelcm 3831 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  x  /\  y  e.  o )  ->  ( x  i^i  o
)  =/=  (/) )
1310, 11, 12syl2anc 671 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( 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 )  =/=  (/) )
14 ineq1 3639 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  x  ->  (
s  i^i  o )  =  ( x  i^i  o ) )
1514neeq1d 2695 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  x  ->  (
( s  i^i  o
)  =/=  (/)  <->  ( x  i^i  o )  =/=  (/) ) )
1615elrab 3208 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  { s  e.  C  |  ( s  i^i  o )  =/=  (/) }  <->  ( x  e.  C  /\  ( x  i^i  o )  =/=  (/) ) )
179, 13, 16sylanbrc 675 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( 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 4217 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( y  e.  x  /\  x  e.  C )  ->  y  e.  U. C
)
19 locfincmp.2 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  Y  = 
U. C
2018, 19syl6eleqr 2551 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  e.  x  /\  x  e.  C )  ->  y  e.  Y )
2120ancoms 459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  C  /\  y  e.  x )  ->  y  e.  Y )
2221adantl 472 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( 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 )
231, 19locfinbas 20592 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( C  e.  ( LocFin `  J
)  ->  X  =  Y )
2423adantl 472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( J  e.  Comp  /\  C  e.  ( LocFin `  J )
)  ->  X  =  Y )
2524ad3antrrr 741 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( J  e.  Comp  /\  C  e.  ( LocFin `  J )
)  /\  ( c  C_  J  /\  c  e. 
Fin ) )  /\  X  =  U. c
)  /\  ( x  e.  C  /\  y  e.  x ) )  ->  X  =  Y )
2622, 25eleqtrrd 2543 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( 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 )
27 simplr 767 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( 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
)
2826, 27eleqtrd 2542 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( 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
)
29 eluni2 4216 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  U. c  <->  E. o  e.  c  y  e.  o )
3028, 29sylib 201 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( 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 )
3117, 30reximddv 2875 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( 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 )  =/=  (/) } )
3231expr 624 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( 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 )  =/=  (/) } ) )
3332exlimdv 1790 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( 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 )  =/=  (/) } ) )
34 n0 3753 . . . . . . . . . . . . . . 15  |-  ( x  =/=  (/)  <->  E. y  y  e.  x )
35 eliun 4297 . . . . . . . . . . . . . . 15  |-  ( 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 )  =/=  (/) } )
3633, 34, 353imtr4g 278 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( 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 )  =/=  (/) } ) )
3736expimpd 612 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )  =/=  (/) } ) )
388, 37syl5bi 225 . . . . . . . . . . . 12  |-  ( ( ( ( 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
)  =/=  (/) } ) )
3938ssrdv 3450 . . . . . . . . . . 11  |-  ( ( ( ( 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 )  =/=  (/) } )
40 iunfi 7893 . . . . . . . . . . . . 13  |-  ( ( 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 )
4140ex 440 . . . . . . . . . . . 12  |-  ( 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 ) )
42 ssfi 7823 . . . . . . . . . . . . 13  |-  ( (
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 )
4342expcom 441 . . . . . . . . . . . 12  |-  ( ( 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 ) )
4441, 43sylan9 667 . . . . . . . . . . 11  |-  ( ( 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 ) )
457, 39, 44syl2anc 671 . . . . . . . . . 10  |-  ( ( ( ( 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 )
)
4645expimpd 612 . . . . . . . . 9  |-  ( ( ( 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 ) )
476, 46sylan2b 482 . . . . . . . 8  |-  ( ( ( 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 ) )
4847rexlimdva 2891 . . . . . . 7  |-  ( ( 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 ) )
495, 48mpd 15 . . . . . 6  |-  ( ( J  e.  Comp  /\  C  e.  ( LocFin `  J )
)  ->  ( C  \  { (/) } )  e. 
Fin )
50 snfi 7681 . . . . . 6  |-  { (/) }  e.  Fin
51 unfi 7869 . . . . . 6  |-  ( ( ( C  \  { (/)
} )  e.  Fin  /\ 
{ (/) }  e.  Fin )  ->  ( ( C 
\  { (/) } )  u.  { (/) } )  e.  Fin )
5249, 50, 51sylancl 673 . . . . 5  |-  ( ( J  e.  Comp  /\  C  e.  ( LocFin `  J )
)  ->  ( ( C  \  { (/) } )  u.  { (/) } )  e.  Fin )
53 ssun1 3609 . . . . . 6  |-  C  C_  ( C  u.  { (/) } )
54 undif1 3854 . . . . . 6  |-  ( ( C  \  { (/) } )  u.  { (/) } )  =  ( C  u.  { (/) } )
5553, 54sseqtr4i 3477 . . . . 5  |-  C  C_  ( ( C  \  { (/) } )  u. 
{ (/) } )
56 ssfi 7823 . . . . 5  |-  ( ( ( ( C  \  { (/) } )  u. 
{ (/) } )  e. 
Fin  /\  C  C_  (
( C  \  { (/)
} )  u.  { (/)
} ) )  ->  C  e.  Fin )
5752, 55, 56sylancl 673 . . . 4  |-  ( ( J  e.  Comp  /\  C  e.  ( LocFin `  J )
)  ->  C  e.  Fin )
5857, 24jca 539 . . 3  |-  ( ( J  e.  Comp  /\  C  e.  ( LocFin `  J )
)  ->  ( C  e.  Fin  /\  X  =  Y ) )
5958ex 440 . 2  |-  ( J  e.  Comp  ->  ( C  e.  ( LocFin `  J
)  ->  ( C  e.  Fin  /\  X  =  Y ) ) )
60 cmptop 20465 . . 3  |-  ( J  e.  Comp  ->  J  e. 
Top )
611, 19finlocfin 20590 . . . 4  |-  ( ( J  e.  Top  /\  C  e.  Fin  /\  X  =  Y )  ->  C  e.  ( LocFin `  J )
)
62613expib 1218 . . 3  |-  ( J  e.  Top  ->  (
( C  e.  Fin  /\  X  =  Y )  ->  C  e.  (
LocFin `  J ) ) )
6360, 62syl 17 . 2  |-  ( J  e.  Comp  ->  ( ( C  e.  Fin  /\  X  =  Y )  ->  C  e.  ( LocFin `  J ) ) )
6459, 63impbid 195 1  |-  ( J  e.  Comp  ->  ( C  e.  ( LocFin `  J
)  <->  ( C  e. 
Fin  /\  X  =  Y ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    = wceq 1455   E.wex 1674    e. wcel 1898    =/= wne 2633   A.wral 2749   E.wrex 2750   {crab 2753    \ cdif 3413    u. cun 3414    i^i cin 3415    C_ wss 3416   (/)c0 3743   ~Pcpw 3963   {csn 3980   U.cuni 4212   U_ciun 4292   ` cfv 5605   Fincfn 7600   Topctop 19972   Compccmp 20456   LocFinclocfin 20574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-1o 7213  df-oadd 7217  df-er 7394  df-en 7601  df-fin 7604  df-top 19976  df-cmp 20457  df-locfin 20577
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator