Metamath Proof Explorer

Theorem llycmpkgen2

Description: A locally compact space is compactly generated. (This variant of llycmpkgen uses the weaker definition of locally compact, "every point has a compact neighborhood", instead of "every point has a local base of compact neighborhoods".) (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypotheses iskgen3.1 
|- X = U. J
llycmpkgen2.2 
|- ( ph -> J e. Top )
llycmpkgen2.3 
|- ( ( ph /\ x e. X ) -> E. k e. ( ( nei ` J ) ` { x } ) ( J |`t k ) e. Comp )
Assertion llycmpkgen2 
|- ( ph -> J e. ran kGen )

Proof

Step Hyp Ref Expression
1 iskgen3.1 
 |-  X = U. J
2 llycmpkgen2.2 
 |-  ( ph -> J e. Top )
3 llycmpkgen2.3 
 |-  ( ( ph /\ x e. X ) -> E. k e. ( ( nei ` J ) ` { x } ) ( J |`t k ) e. Comp )
4 elssuni 
 |-  ( u e. ( kGen ` J ) -> u C_ U. ( kGen ` J ) )
5 4 adantl 
 |-  ( ( ph /\ u e. ( kGen ` J ) ) -> u C_ U. ( kGen ` J ) )
6 1 kgenuni 
 |-  ( J e. Top -> X = U. ( kGen ` J ) )
7 2 6 syl 
 |-  ( ph -> X = U. ( kGen ` J ) )
8 7 adantr 
 |-  ( ( ph /\ u e. ( kGen ` J ) ) -> X = U. ( kGen ` J ) )
9 5 8 sseqtrrd 
 |-  ( ( ph /\ u e. ( kGen ` J ) ) -> u C_ X )
10 9 sselda 
 |-  ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) -> x e. X )
11 3 adantlr 
 |-  ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. X ) -> E. k e. ( ( nei ` J ) ` { x } ) ( J |`t k ) e. Comp )
12 10 11 syldan 
 |-  ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) -> E. k e. ( ( nei ` J ) ` { x } ) ( J |`t k ) e. Comp )
13 2 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> J e. Top )
14 difss 
 |-  ( X \ ( k \ u ) ) C_ X
15 1 ntropn 
 |-  ( ( J e. Top /\ ( X \ ( k \ u ) ) C_ X ) -> ( ( int ` J ) ` ( X \ ( k \ u ) ) ) e. J )
16 13 14 15 sylancl 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( int ` J ) ` ( X \ ( k \ u ) ) ) e. J )
17 simprl 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> k e. ( ( nei ` J ) ` { x } ) )
18 1 neii1 
 |-  ( ( J e. Top /\ k e. ( ( nei ` J ) ` { x } ) ) -> k C_ X )
19 13 17 18 syl2anc 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> k C_ X )
20 1 ntropn 
 |-  ( ( J e. Top /\ k C_ X ) -> ( ( int ` J ) ` k ) e. J )
21 13 19 20 syl2anc 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( int ` J ) ` k ) e. J )
22 inopn 
 |-  ( ( J e. Top /\ ( ( int ` J ) ` ( X \ ( k \ u ) ) ) e. J /\ ( ( int ` J ) ` k ) e. J ) -> ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( ( int ` J ) ` k ) ) e. J )
23 13 16 21 22 syl3anc 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( ( int ` J ) ` k ) ) e. J )
24 simplr 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> x e. u )
25 1 ntrss2 
 |-  ( ( J e. Top /\ k C_ X ) -> ( ( int ` J ) ` k ) C_ k )
26 13 19 25 syl2anc 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( int ` J ) ` k ) C_ k )
27 10 adantr 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> x e. X )
28 27 snssd 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> { x } C_ X )
29 1 neiint 
 |-  ( ( J e. Top /\ { x } C_ X /\ k C_ X ) -> ( k e. ( ( nei ` J ) ` { x } ) <-> { x } C_ ( ( int ` J ) ` k ) ) )
30 13 28 19 29 syl3anc 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( k e. ( ( nei ` J ) ` { x } ) <-> { x } C_ ( ( int ` J ) ` k ) ) )
31 17 30 mpbid 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> { x } C_ ( ( int ` J ) ` k ) )
32 vex 
 |-  x e. _V
33 32 snss 
 |-  ( x e. ( ( int ` J ) ` k ) <-> { x } C_ ( ( int ` J ) ` k ) )
34 31 33 sylibr 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> x e. ( ( int ` J ) ` k ) )
35 26 34 sseldd 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> x e. k )
36 24 35 elind 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> x e. ( u i^i k ) )
37 simpllr 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> u e. ( kGen ` J ) )
38 simprr 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( J |`t k ) e. Comp )
39 kgeni 
 |-  ( ( u e. ( kGen ` J ) /\ ( J |`t k ) e. Comp ) -> ( u i^i k ) e. ( J |`t k ) )
40 37 38 39 syl2anc 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( u i^i k ) e. ( J |`t k ) )
41 vex 
 |-  k e. _V
42 resttop 
 |-  ( ( J e. Top /\ k e. _V ) -> ( J |`t k ) e. Top )
43 13 41 42 sylancl 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( J |`t k ) e. Top )
44 inss2 
 |-  ( u i^i k ) C_ k
45 1 restuni 
 |-  ( ( J e. Top /\ k C_ X ) -> k = U. ( J |`t k ) )
46 13 19 45 syl2anc 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> k = U. ( J |`t k ) )
47 44 46 sseqtrid 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( u i^i k ) C_ U. ( J |`t k ) )
48 eqid 
 |-  U. ( J |`t k ) = U. ( J |`t k )
49 48 isopn3 
 |-  ( ( ( J |`t k ) e. Top /\ ( u i^i k ) C_ U. ( J |`t k ) ) -> ( ( u i^i k ) e. ( J |`t k ) <-> ( ( int ` ( J |`t k ) ) ` ( u i^i k ) ) = ( u i^i k ) ) )
50 43 47 49 syl2anc 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( u i^i k ) e. ( J |`t k ) <-> ( ( int ` ( J |`t k ) ) ` ( u i^i k ) ) = ( u i^i k ) ) )
51 40 50 mpbid 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( int ` ( J |`t k ) ) ` ( u i^i k ) ) = ( u i^i k ) )
52 44 a1i 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( u i^i k ) C_ k )
53 eqid 
 |-  ( J |`t k ) = ( J |`t k )
54 1 53 restntr 
 |-  ( ( J e. Top /\ k C_ X /\ ( u i^i k ) C_ k ) -> ( ( int ` ( J |`t k ) ) ` ( u i^i k ) ) = ( ( ( int ` J ) ` ( ( u i^i k ) u. ( X \ k ) ) ) i^i k ) )
55 13 19 52 54 syl3anc 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( int ` ( J |`t k ) ) ` ( u i^i k ) ) = ( ( ( int ` J ) ` ( ( u i^i k ) u. ( X \ k ) ) ) i^i k ) )
56 51 55 eqtr3d 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( u i^i k ) = ( ( ( int ` J ) ` ( ( u i^i k ) u. ( X \ k ) ) ) i^i k ) )
57 36 56 eleqtrd 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> x e. ( ( ( int ` J ) ` ( ( u i^i k ) u. ( X \ k ) ) ) i^i k ) )
58 57 elin1d 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> x e. ( ( int ` J ) ` ( ( u i^i k ) u. ( X \ k ) ) ) )
59 undif3 
 |-  ( ( u i^i k ) u. ( X \ k ) ) = ( ( ( u i^i k ) u. X ) \ ( k \ ( u i^i k ) ) )
60 incom 
 |-  ( u i^i k ) = ( k i^i u )
61 60 difeq2i 
 |-  ( k \ ( u i^i k ) ) = ( k \ ( k i^i u ) )
62 difin 
 |-  ( k \ ( k i^i u ) ) = ( k \ u )
63 61 62 eqtri 
 |-  ( k \ ( u i^i k ) ) = ( k \ u )
64 63 difeq2i 
 |-  ( ( ( u i^i k ) u. X ) \ ( k \ ( u i^i k ) ) ) = ( ( ( u i^i k ) u. X ) \ ( k \ u ) )
65 59 64 eqtri 
 |-  ( ( u i^i k ) u. ( X \ k ) ) = ( ( ( u i^i k ) u. X ) \ ( k \ u ) )
66 44 19 sstrid 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( u i^i k ) C_ X )
67 ssequn1 
 |-  ( ( u i^i k ) C_ X <-> ( ( u i^i k ) u. X ) = X )
68 66 67 sylib 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( u i^i k ) u. X ) = X )
69 68 difeq1d 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( ( u i^i k ) u. X ) \ ( k \ u ) ) = ( X \ ( k \ u ) ) )
70 65 69 eqtrid 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( u i^i k ) u. ( X \ k ) ) = ( X \ ( k \ u ) ) )
71 70 fveq2d 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( int ` J ) ` ( ( u i^i k ) u. ( X \ k ) ) ) = ( ( int ` J ) ` ( X \ ( k \ u ) ) ) )
72 58 71 eleqtrd 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> x e. ( ( int ` J ) ` ( X \ ( k \ u ) ) ) )
73 72 34 elind 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> x e. ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( ( int ` J ) ` k ) ) )
74 sslin 
 |-  ( ( ( int ` J ) ` k ) C_ k -> ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( ( int ` J ) ` k ) ) C_ ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i k ) )
75 26 74 syl 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( ( int ` J ) ` k ) ) C_ ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i k ) )
76 1 ntrss2 
 |-  ( ( J e. Top /\ ( X \ ( k \ u ) ) C_ X ) -> ( ( int ` J ) ` ( X \ ( k \ u ) ) ) C_ ( X \ ( k \ u ) ) )
77 13 14 76 sylancl 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( int ` J ) ` ( X \ ( k \ u ) ) ) C_ ( X \ ( k \ u ) ) )
78 77 difss2d 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( int ` J ) ` ( X \ ( k \ u ) ) ) C_ X )
79 reldisj 
 |-  ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) C_ X -> ( ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( k \ u ) ) = (/) <-> ( ( int ` J ) ` ( X \ ( k \ u ) ) ) C_ ( X \ ( k \ u ) ) ) )
80 78 79 syl 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( k \ u ) ) = (/) <-> ( ( int ` J ) ` ( X \ ( k \ u ) ) ) C_ ( X \ ( k \ u ) ) ) )
81 77 80 mpbird 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( k \ u ) ) = (/) )
82 inssdif0 
 |-  ( ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i k ) C_ u <-> ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( k \ u ) ) = (/) )
83 81 82 sylibr 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i k ) C_ u )
84 75 83 sstrd 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( ( int ` J ) ` k ) ) C_ u )
85 eleq2 
 |-  ( z = ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( ( int ` J ) ` k ) ) -> ( x e. z <-> x e. ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( ( int ` J ) ` k ) ) ) )
86 sseq1 
 |-  ( z = ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( ( int ` J ) ` k ) ) -> ( z C_ u <-> ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( ( int ` J ) ` k ) ) C_ u ) )
87 85 86 anbi12d 
 |-  ( z = ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( ( int ` J ) ` k ) ) -> ( ( x e. z /\ z C_ u ) <-> ( x e. ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( ( int ` J ) ` k ) ) /\ ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( ( int ` J ) ` k ) ) C_ u ) ) )
88 87 rspcev 
 |-  ( ( ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( ( int ` J ) ` k ) ) e. J /\ ( x e. ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( ( int ` J ) ` k ) ) /\ ( ( ( int ` J ) ` ( X \ ( k \ u ) ) ) i^i ( ( int ` J ) ` k ) ) C_ u ) ) -> E. z e. J ( x e. z /\ z C_ u ) )
89 23 73 84 88 syl12anc 
 |-  ( ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) /\ ( k e. ( ( nei ` J ) ` { x } ) /\ ( J |`t k ) e. Comp ) ) -> E. z e. J ( x e. z /\ z C_ u ) )
90 12 89 rexlimddv 
 |-  ( ( ( ph /\ u e. ( kGen ` J ) ) /\ x e. u ) -> E. z e. J ( x e. z /\ z C_ u ) )
91 90 ralrimiva 
 |-  ( ( ph /\ u e. ( kGen ` J ) ) -> A. x e. u E. z e. J ( x e. z /\ z C_ u ) )
92 91 ex 
 |-  ( ph -> ( u e. ( kGen ` J ) -> A. x e. u E. z e. J ( x e. z /\ z C_ u ) ) )
93 eltop2 
 |-  ( J e. Top -> ( u e. J <-> A. x e. u E. z e. J ( x e. z /\ z C_ u ) ) )
94 2 93 syl 
 |-  ( ph -> ( u e. J <-> A. x e. u E. z e. J ( x e. z /\ z C_ u ) ) )
95 92 94 sylibrd 
 |-  ( ph -> ( u e. ( kGen ` J ) -> u e. J ) )
96 95 ssrdv 
 |-  ( ph -> ( kGen ` J ) C_ J )
97 iskgen2 
 |-  ( J e. ran kGen <-> ( J e. Top /\ ( kGen ` J ) C_ J ) )
98 2 96 97 sylanbrc 
 |-  ( ph -> J e. ran kGen )