# 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}=\bigcup {J}$
llycmpkgen2.2 ${⊢}{\phi }\to {J}\in \mathrm{Top}$
llycmpkgen2.3 ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \exists {k}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{J}{↾}_{𝑡}{k}\in \mathrm{Comp}$
Assertion llycmpkgen2 ${⊢}{\phi }\to {J}\in \mathrm{ran}\mathrm{𝑘Gen}$

### Proof

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