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

Theorem hausllycmp 20521
Description: A compact Hausdorff space is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.)
Assertion
Ref Expression
hausllycmp  |-  ( ( J  e.  Haus  /\  J  e.  Comp )  ->  J  e. 𝑛Locally  Comp )

Proof of Theorem hausllycmp
Dummy variables  u  v  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 haustop 20359 . . 3  |-  ( J  e.  Haus  ->  J  e. 
Top )
21adantr 467 . 2  |-  ( ( J  e.  Haus  /\  J  e.  Comp )  ->  J  e.  Top )
3 eqid 2453 . . . . . 6  |-  U. J  =  U. J
4 eqid 2453 . . . . . 6  |-  { z  e.  J  |  E. v  e.  J  (
y  e.  v  /\  ( ( cls `  J
) `  v )  C_  ( U. J  \ 
z ) ) }  =  { z  e.  J  |  E. v  e.  J  ( y  e.  v  /\  (
( cls `  J
) `  v )  C_  ( U. J  \ 
z ) ) }
5 simpll 761 . . . . . 6  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  J  e.  Haus )
6 difssd 3563 . . . . . 6  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  ( U. J  \  x
)  C_  U. J )
7 simplr 763 . . . . . . 7  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  J  e.  Comp )
81ad2antrr 733 . . . . . . . 8  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  J  e.  Top )
9 simprl 765 . . . . . . . 8  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  x  e.  J )
103opncld 20060 . . . . . . . 8  |-  ( ( J  e.  Top  /\  x  e.  J )  ->  ( U. J  \  x )  e.  (
Clsd `  J )
)
118, 9, 10syl2anc 667 . . . . . . 7  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  ( U. J  \  x
)  e.  ( Clsd `  J ) )
12 cmpcld 20429 . . . . . . 7  |-  ( ( J  e.  Comp  /\  ( U. J  \  x
)  e.  ( Clsd `  J ) )  -> 
( Jt  ( U. J  \  x ) )  e. 
Comp )
137, 11, 12syl2anc 667 . . . . . 6  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  ( Jt  ( U. J  \  x
) )  e.  Comp )
14 simprr 767 . . . . . . 7  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  y  e.  x )
15 elssuni 4230 . . . . . . . . 9  |-  ( x  e.  J  ->  x  C_ 
U. J )
1615ad2antrl 735 . . . . . . . 8  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  x  C_ 
U. J )
17 dfss4 3679 . . . . . . . 8  |-  ( x 
C_  U. J  <->  ( U. J  \  ( U. J  \  x ) )  =  x )
1816, 17sylib 200 . . . . . . 7  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  ( U. J  \  ( U. J  \  x
) )  =  x )
1914, 18eleqtrrd 2534 . . . . . 6  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  y  e.  ( U. J  \ 
( U. J  \  x ) ) )
203, 4, 5, 6, 13, 19hauscmplem 20433 . . . . 5  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  E. u  e.  J  ( y  e.  u  /\  (
( cls `  J
) `  u )  C_  ( U. J  \ 
( U. J  \  x ) ) ) )
2118sseq2d 3462 . . . . . . 7  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  (
( ( cls `  J
) `  u )  C_  ( U. J  \ 
( U. J  \  x ) )  <->  ( ( cls `  J ) `  u )  C_  x
) )
2221anbi2d 711 . . . . . 6  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  (
( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  ( U. J  \ 
( U. J  \  x ) ) )  <-> 
( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )
2322rexbidv 2903 . . . . 5  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  ( E. u  e.  J  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  ( U. J  \ 
( U. J  \  x ) ) )  <->  E. u  e.  J  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )
2420, 23mpbid 214 . . . 4  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  E. u  e.  J  ( y  e.  u  /\  (
( cls `  J
) `  u )  C_  x ) )
258adantr 467 . . . . . . 7  |-  ( ( ( ( J  e. 
Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x ) )  /\  ( u  e.  J  /\  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )  ->  J  e.  Top )
26 simprl 765 . . . . . . . 8  |-  ( ( ( ( J  e. 
Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x ) )  /\  ( u  e.  J  /\  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )  ->  u  e.  J
)
27 simprrl 775 . . . . . . . 8  |-  ( ( ( ( J  e. 
Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x ) )  /\  ( u  e.  J  /\  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )  ->  y  e.  u
)
28 opnneip 20147 . . . . . . . 8  |-  ( ( J  e.  Top  /\  u  e.  J  /\  y  e.  u )  ->  u  e.  ( ( nei `  J ) `
 { y } ) )
2925, 26, 27, 28syl3anc 1269 . . . . . . 7  |-  ( ( ( ( J  e. 
Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x ) )  /\  ( u  e.  J  /\  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )  ->  u  e.  ( ( nei `  J
) `  { y } ) )
30 elssuni 4230 . . . . . . . . 9  |-  ( u  e.  J  ->  u  C_ 
U. J )
3130ad2antrl 735 . . . . . . . 8  |-  ( ( ( ( J  e. 
Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x ) )  /\  ( u  e.  J  /\  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )  ->  u  C_  U. J
)
323sscls 20083 . . . . . . . 8  |-  ( ( J  e.  Top  /\  u  C_  U. J )  ->  u  C_  (
( cls `  J
) `  u )
)
3325, 31, 32syl2anc 667 . . . . . . 7  |-  ( ( ( ( J  e. 
Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x ) )  /\  ( u  e.  J  /\  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )  ->  u  C_  (
( cls `  J
) `  u )
)
343clsss3 20086 . . . . . . . 8  |-  ( ( J  e.  Top  /\  u  C_  U. J )  ->  ( ( cls `  J ) `  u
)  C_  U. J )
3525, 31, 34syl2anc 667 . . . . . . 7  |-  ( ( ( ( J  e. 
Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x ) )  /\  ( u  e.  J  /\  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )  ->  ( ( cls `  J ) `  u
)  C_  U. J )
363ssnei2 20144 . . . . . . 7  |-  ( ( ( J  e.  Top  /\  u  e.  ( ( nei `  J ) `
 { y } ) )  /\  (
u  C_  ( ( cls `  J ) `  u )  /\  (
( cls `  J
) `  u )  C_ 
U. J ) )  ->  ( ( cls `  J ) `  u
)  e.  ( ( nei `  J ) `
 { y } ) )
3725, 29, 33, 35, 36syl22anc 1270 . . . . . 6  |-  ( ( ( ( J  e. 
Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x ) )  /\  ( u  e.  J  /\  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )  ->  ( ( cls `  J ) `  u
)  e.  ( ( nei `  J ) `
 { y } ) )
38 simprrr 776 . . . . . . 7  |-  ( ( ( ( J  e. 
Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x ) )  /\  ( u  e.  J  /\  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )  ->  ( ( cls `  J ) `  u
)  C_  x )
39 vex 3050 . . . . . . . 8  |-  x  e. 
_V
4039elpw2 4570 . . . . . . 7  |-  ( ( ( cls `  J
) `  u )  e.  ~P x  <->  ( ( cls `  J ) `  u )  C_  x
)
4138, 40sylibr 216 . . . . . 6  |-  ( ( ( ( J  e. 
Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x ) )  /\  ( u  e.  J  /\  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )  ->  ( ( cls `  J ) `  u
)  e.  ~P x
)
4237, 41elind 3620 . . . . 5  |-  ( ( ( ( J  e. 
Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x ) )  /\  ( u  e.  J  /\  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )  ->  ( ( cls `  J ) `  u
)  e.  ( ( ( nei `  J
) `  { y } )  i^i  ~P x ) )
437adantr 467 . . . . . 6  |-  ( ( ( ( J  e. 
Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x ) )  /\  ( u  e.  J  /\  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )  ->  J  e.  Comp )
443clscld 20074 . . . . . . 7  |-  ( ( J  e.  Top  /\  u  C_  U. J )  ->  ( ( cls `  J ) `  u
)  e.  ( Clsd `  J ) )
4525, 31, 44syl2anc 667 . . . . . 6  |-  ( ( ( ( J  e. 
Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x ) )  /\  ( u  e.  J  /\  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )  ->  ( ( cls `  J ) `  u
)  e.  ( Clsd `  J ) )
46 cmpcld 20429 . . . . . 6  |-  ( ( J  e.  Comp  /\  (
( cls `  J
) `  u )  e.  ( Clsd `  J
) )  ->  ( Jt  ( ( cls `  J
) `  u )
)  e.  Comp )
4743, 45, 46syl2anc 667 . . . . 5  |-  ( ( ( ( J  e. 
Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x ) )  /\  ( u  e.  J  /\  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )  ->  ( Jt  ( ( cls `  J ) `
 u ) )  e.  Comp )
48 oveq2 6303 . . . . . . 7  |-  ( v  =  ( ( cls `  J ) `  u
)  ->  ( Jt  v
)  =  ( Jt  ( ( cls `  J
) `  u )
) )
4948eleq1d 2515 . . . . . 6  |-  ( v  =  ( ( cls `  J ) `  u
)  ->  ( ( Jt  v )  e.  Comp  <->  ( Jt  ( ( cls `  J
) `  u )
)  e.  Comp )
)
5049rspcev 3152 . . . . 5  |-  ( ( ( ( cls `  J
) `  u )  e.  ( ( ( nei `  J ) `  {
y } )  i^i 
~P x )  /\  ( Jt  ( ( cls `  J ) `  u
) )  e.  Comp )  ->  E. v  e.  ( ( ( nei `  J
) `  { y } )  i^i  ~P x ) ( Jt  v )  e.  Comp )
5142, 47, 50syl2anc 667 . . . 4  |-  ( ( ( ( J  e. 
Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x ) )  /\  ( u  e.  J  /\  ( y  e.  u  /\  ( ( cls `  J
) `  u )  C_  x ) ) )  ->  E. v  e.  ( ( ( nei `  J
) `  { y } )  i^i  ~P x ) ( Jt  v )  e.  Comp )
5224, 51rexlimddv 2885 . . 3  |-  ( ( ( J  e.  Haus  /\  J  e.  Comp )  /\  ( x  e.  J  /\  y  e.  x
) )  ->  E. v  e.  ( ( ( nei `  J ) `  {
y } )  i^i 
~P x ) ( Jt  v )  e.  Comp )
5352ralrimivva 2811 . 2  |-  ( ( J  e.  Haus  /\  J  e.  Comp )  ->  A. x  e.  J  A. y  e.  x  E. v  e.  ( ( ( nei `  J ) `  {
y } )  i^i 
~P x ) ( Jt  v )  e.  Comp )
54 isnlly 20496 . 2  |-  ( J  e. 𝑛Locally 
Comp 
<->  ( J  e.  Top  /\ 
A. x  e.  J  A. y  e.  x  E. v  e.  (
( ( nei `  J
) `  { y } )  i^i  ~P x ) ( Jt  v )  e.  Comp )
)
552, 53, 54sylanbrc 671 1  |-  ( ( J  e.  Haus  /\  J  e.  Comp )  ->  J  e. 𝑛Locally  Comp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1446    e. wcel 1889   A.wral 2739   E.wrex 2740   {crab 2743    \ cdif 3403    i^i cin 3405    C_ wss 3406   ~Pcpw 3953   {csn 3970   U.cuni 4201   ` cfv 5585  (class class class)co 6295   ↾t crest 15331   Topctop 19929   Clsdccld 20043   clsccl 20045   neicnei 20125   Hauscha 20336   Compccmp 20413  𝑛Locally cnlly 20492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-reu 2746  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-int 4238  df-iun 4283  df-iin 4284  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-oadd 7191  df-er 7368  df-en 7575  df-dom 7576  df-fin 7578  df-fi 7930  df-rest 15333  df-topgen 15354  df-top 19933  df-bases 19934  df-topon 19935  df-cld 20046  df-cls 20048  df-nei 20126  df-haus 20343  df-cmp 20414  df-nlly 20494
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator