Metamath Proof Explorer

Theorem hausllycmp

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

Ref Expression
Assertion hausllycmp ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) → 𝐽 ∈ 𝑛-Locally Comp )

Proof

Step Hyp Ref Expression
1 haustop ⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Top )
2 1 adantr ⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) → 𝐽 ∈ Top )
3 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
4 eqid ⊢ { 𝑧 ∈ 𝐽 ∣ ∃ 𝑣 ∈ 𝐽 ( 𝑦 ∈ 𝑣 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑣 ) ⊆ ( ∪ 𝐽 ∖ 𝑧 ) ) } = { 𝑧 ∈ 𝐽 ∣ ∃ 𝑣 ∈ 𝐽 ( 𝑦 ∈ 𝑣 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑣 ) ⊆ ( ∪ 𝐽 ∖ 𝑧 ) ) }
5 simpll ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝐽 ∈ Haus )
6 difssd ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( ∪ 𝐽 ∖ 𝑥 ) ⊆ ∪ 𝐽 )
7 simplr ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝐽 ∈ Comp )
8 1 ad2antrr ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝐽 ∈ Top )
9 simprl ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑥 ∈ 𝐽 )
10 3 opncld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
11 8 9 10 syl2anc ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( ∪ 𝐽 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
12 cmpcld ⊢ ( ( 𝐽 ∈ Comp ∧ ( ∪ 𝐽 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽 ↾t ( ∪ 𝐽 ∖ 𝑥 ) ) ∈ Comp )
13 7 11 12 syl2anc ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝐽 ↾t ( ∪ 𝐽 ∖ 𝑥 ) ) ∈ Comp )
14 simprr ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑦 ∈ 𝑥 )
15 elssuni ⊢ ( 𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽 )
16 15 ad2antrl ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑥 ⊆ ∪ 𝐽 )
17 dfss4 ⊢ ( 𝑥 ⊆ ∪ 𝐽 ↔ ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) = 𝑥 )
18 16 17 sylib ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) = 𝑥 )
19 14 18 eleqtrrd ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑦 ∈ ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) )
20 3 4 5 6 13 19 hauscmplem ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) ) )
21 18 sseq2d ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) )
22 21 anbi2d ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) ) ↔ ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) )
23 22 rexbidv ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) ) ↔ ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) )
24 20 23 mpbid ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) )
25 8 adantr ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) ) → 𝐽 ∈ Top )
26 simprl ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) ) → 𝑢 ∈ 𝐽 )
27 simprrl ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) ) → 𝑦 ∈ 𝑢 )
28 opnneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ 𝑢 ) → 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
29 25 26 27 28 syl3anc ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) ) → 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
30 elssuni ⊢ ( 𝑢 ∈ 𝐽 → 𝑢 ⊆ ∪ 𝐽 )
31 30 ad2antrl ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) ) → 𝑢 ⊆ ∪ 𝐽 )
32 3 sscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑢 ⊆ ∪ 𝐽 ) → 𝑢 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) )
33 25 31 32 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) ) → 𝑢 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) )
34 3 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑢 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ ∪ 𝐽 )
35 25 31 34 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ ∪ 𝐽 )
36 3 ssnei2 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ) ∧ ( 𝑢 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ ∪ 𝐽 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
37 25 29 33 35 36 syl22anc ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
38 simprrr ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 )
39 vex ⊢ 𝑥 ∈ V
40 39 elpw2 ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ∈ 𝒫 𝑥 ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 )
41 38 40 sylibr ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ∈ 𝒫 𝑥 )
42 37 41 elind ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) )
43 7 adantr ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) ) → 𝐽 ∈ Comp )
44 3 clscld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑢 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ∈ ( Clsd ‘ 𝐽 ) )
45 25 31 44 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ∈ ( Clsd ‘ 𝐽 ) )
46 cmpcld ⊢ ( ( 𝐽 ∈ Comp ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ) ∈ Comp )
47 43 45 46 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) ) → ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ) ∈ Comp )
48 oveq2 ⊢ ( 𝑣 = ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) → ( 𝐽 ↾t 𝑣 ) = ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ) )
49 48 eleq1d ⊢ ( 𝑣 = ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) → ( ( 𝐽 ↾t 𝑣 ) ∈ Comp ↔ ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ) ∈ Comp ) )
50 49 rspcev ⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ∧ ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ) ∈ Comp ) → ∃ 𝑣 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑣 ) ∈ Comp )
51 42 47 50 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑦 ∈ 𝑢 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑢 ) ⊆ 𝑥 ) ) ) → ∃ 𝑣 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑣 ) ∈ Comp )
52 24 51 rexlimddv ⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ∃ 𝑣 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑣 ) ∈ Comp )
53 52 ralrimivva ⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) → ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑣 ) ∈ Comp )
54 isnlly ⊢ ( 𝐽 ∈ 𝑛-Locally Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑣 ) ∈ Comp ) )
55 2 53 54 sylanbrc ⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ Comp ) → 𝐽 ∈ 𝑛-Locally Comp )