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 ⊢ 𝑋 = ∪ 𝐽
llycmpkgen2.2 ⊢ ( 𝜑 → 𝐽 ∈ Top )
llycmpkgen2.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑘 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝐽 ↾t 𝑘 ) ∈ Comp )
Assertion llycmpkgen2 ( 𝜑 → 𝐽 ∈ ran 𝑘Gen )

Proof

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