Metamath Proof Explorer

Theorem hausllycmp

Description: A compact Hausdorff space is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion hausllycmp 
|- ( ( J e. Haus /\ J e. Comp ) -> J e. N-Locally Comp )

Proof

Step Hyp Ref Expression
1 haustop 
 |-  ( J e. Haus -> J e. Top )
2 1 adantr 
 |-  ( ( J e. Haus /\ J e. Comp ) -> J e. Top )
3 eqid 
 |-  U. J = U. J
4 eqid 
 |-  { 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 
 |-  ( ( ( J e. Haus /\ J e. Comp ) /\ ( x e. J /\ y e. x ) ) -> J e. Haus )
6 difssd 
 |-  ( ( ( J e. Haus /\ J e. Comp ) /\ ( x e. J /\ y e. x ) ) -> ( U. J \ x ) C_ U. J )
7 simplr 
 |-  ( ( ( J e. Haus /\ J e. Comp ) /\ ( x e. J /\ y e. x ) ) -> J e. Comp )
8 1 ad2antrr 
 |-  ( ( ( J e. Haus /\ J e. Comp ) /\ ( x e. J /\ y e. x ) ) -> J e. Top )
9 simprl 
 |-  ( ( ( J e. Haus /\ J e. Comp ) /\ ( x e. J /\ y e. x ) ) -> x e. J )
10 3 opncld 
 |-  ( ( J e. Top /\ x e. J ) -> ( U. J \ x ) e. ( Clsd ` J ) )
11 8 9 10 syl2anc 
 |-  ( ( ( J e. Haus /\ J e. Comp ) /\ ( x e. J /\ y e. x ) ) -> ( U. J \ x ) e. ( Clsd ` J ) )
12 cmpcld 
 |-  ( ( J e. Comp /\ ( U. J \ x ) e. ( Clsd ` J ) ) -> ( J |`t ( U. J \ x ) ) e. Comp )
13 7 11 12 syl2anc 
 |-  ( ( ( J e. Haus /\ J e. Comp ) /\ ( x e. J /\ y e. x ) ) -> ( J |`t ( U. J \ x ) ) e. Comp )
14 simprr 
 |-  ( ( ( J e. Haus /\ J e. Comp ) /\ ( x e. J /\ y e. x ) ) -> y e. x )
15 elssuni 
 |-  ( x e. J -> x C_ U. J )
16 15 ad2antrl 
 |-  ( ( ( J e. Haus /\ J e. Comp ) /\ ( x e. J /\ y e. x ) ) -> x C_ U. J )
17 dfss4 
 |-  ( x C_ U. J <-> ( U. J \ ( U. J \ x ) ) = x )
18 16 17 sylib 
 |-  ( ( ( J e. Haus /\ J e. Comp ) /\ ( x e. J /\ y e. x ) ) -> ( U. J \ ( U. J \ x ) ) = x )
19 14 18 eleqtrrd 
 |-  ( ( ( J e. Haus /\ J e. Comp ) /\ ( x e. J /\ y e. x ) ) -> y e. ( U. J \ ( U. J \ x ) ) )
20 3 4 5 6 13 19 hauscmplem 
 |-  ( ( ( 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 ) ) ) )
21 18 sseq2d 
 |-  ( ( ( 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 ) )
22 21 anbi2d 
 |-  ( ( ( 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 ) ) )
23 22 rexbidv 
 |-  ( ( ( 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 ) ) )
24 20 23 mpbid 
 |-  ( ( ( J e. Haus /\ J e. Comp ) /\ ( x e. J /\ y e. x ) ) -> E. u e. J ( y e. u /\ ( ( cls ` J ) ` u ) C_ x ) )
25 8 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( J e. Top /\ u e. J /\ y e. u ) -> u e. ( ( nei ` J ) ` { y } ) )
29 25 26 27 28 syl3anc 
 |-  ( ( ( ( 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 
 |-  ( u e. J -> u C_ U. J )
31 30 ad2antrl 
 |-  ( ( ( ( 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 )
32 3 sscls 
 |-  ( ( J e. Top /\ u C_ U. J ) -> u C_ ( ( cls ` J ) ` u ) )
33 25 31 32 syl2anc 
 |-  ( ( ( ( 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 ) )
34 3 clsss3 
 |-  ( ( J e. Top /\ u C_ U. J ) -> ( ( cls ` J ) ` u ) C_ U. J )
35 25 31 34 syl2anc 
 |-  ( ( ( ( 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 )
36 3 ssnei2 
 |-  ( ( ( 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 } ) )
37 25 29 33 35 36 syl22anc 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  x e. _V
40 39 elpw2 
 |-  ( ( ( cls ` J ) ` u ) e. ~P x <-> ( ( cls ` J ) ` u ) C_ x )
41 38 40 sylibr 
 |-  ( ( ( ( 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 )
42 37 41 elind 
 |-  ( ( ( ( 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 ) )
43 7 adantr 
 |-  ( ( ( ( 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 )
44 3 clscld 
 |-  ( ( J e. Top /\ u C_ U. J ) -> ( ( cls ` J ) ` u ) e. ( Clsd ` J ) )
45 25 31 44 syl2anc 
 |-  ( ( ( ( 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 
 |-  ( ( J e. Comp /\ ( ( cls ` J ) ` u ) e. ( Clsd ` J ) ) -> ( J |`t ( ( cls ` J ) ` u ) ) e. Comp )
47 43 45 46 syl2anc 
 |-  ( ( ( ( J e. Haus /\ J e. Comp ) /\ ( x e. J /\ y e. x ) ) /\ ( u e. J /\ ( y e. u /\ ( ( cls ` J ) ` u ) C_ x ) ) ) -> ( J |`t ( ( cls ` J ) ` u ) ) e. Comp )
48 oveq2 
 |-  ( v = ( ( cls ` J ) ` u ) -> ( J |`t v ) = ( J |`t ( ( cls ` J ) ` u ) ) )
49 48 eleq1d 
 |-  ( v = ( ( cls ` J ) ` u ) -> ( ( J |`t v ) e. Comp <-> ( J |`t ( ( cls ` J ) ` u ) ) e. Comp ) )
50 49 rspcev 
 |-  ( ( ( ( cls ` J ) ` u ) e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) /\ ( J |`t ( ( cls ` J ) ` u ) ) e. Comp ) -> E. v e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t v ) e. Comp )
51 42 47 50 syl2anc 
 |-  ( ( ( ( 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 ) ( J |`t v ) e. Comp )
52 24 51 rexlimddv 
 |-  ( ( ( J e. Haus /\ J e. Comp ) /\ ( x e. J /\ y e. x ) ) -> E. v e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t v ) e. Comp )
53 52 ralrimivva 
 |-  ( ( J e. Haus /\ J e. Comp ) -> A. x e. J A. y e. x E. v e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t v ) e. Comp )
54 isnlly 
 |-  ( J e. N-Locally Comp <-> ( J e. Top /\ A. x e. J A. y e. x E. v e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t v ) e. Comp ) )
55 2 53 54 sylanbrc 
 |-  ( ( J e. Haus /\ J e. Comp ) -> J e. N-Locally Comp )