MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  llycmpkgen2 Structured version   Visualization version   GIF version

Theorem llycmpkgen2 21263
Description: A locally compact space is compactly generated. (This variant of llycmpkgen 21265 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.)
Hypotheses
Ref Expression
iskgen3.1 𝑋 = 𝐽
llycmpkgen2.2 (𝜑𝐽 ∈ Top)
llycmpkgen2.3 ((𝜑𝑥𝑋) → ∃𝑘 ∈ ((nei‘𝐽)‘{𝑥})(𝐽t 𝑘) ∈ Comp)
Assertion
Ref Expression
llycmpkgen2 (𝜑𝐽 ∈ ran 𝑘Gen)
Distinct variable groups:   𝑥,𝑘,𝐽   𝜑,𝑘,𝑥   𝑘,𝑋
Allowed substitution hint:   𝑋(𝑥)

Proof of Theorem llycmpkgen2
Dummy variables 𝑢 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 llycmpkgen2.2 . 2 (𝜑𝐽 ∈ Top)
2 elssuni 4433 . . . . . . . . . . 11 (𝑢 ∈ (𝑘Gen‘𝐽) → 𝑢 (𝑘Gen‘𝐽))
32adantl 482 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) → 𝑢 (𝑘Gen‘𝐽))
4 iskgen3.1 . . . . . . . . . . . . 13 𝑋 = 𝐽
54kgenuni 21252 . . . . . . . . . . . 12 (𝐽 ∈ Top → 𝑋 = (𝑘Gen‘𝐽))
61, 5syl 17 . . . . . . . . . . 11 (𝜑𝑋 = (𝑘Gen‘𝐽))
76adantr 481 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) → 𝑋 = (𝑘Gen‘𝐽))
83, 7sseqtr4d 3621 . . . . . . . . 9 ((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) → 𝑢𝑋)
98sselda 3583 . . . . . . . 8 (((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) → 𝑥𝑋)
10 llycmpkgen2.3 . . . . . . . . 9 ((𝜑𝑥𝑋) → ∃𝑘 ∈ ((nei‘𝐽)‘{𝑥})(𝐽t 𝑘) ∈ Comp)
1110adantlr 750 . . . . . . . 8 (((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑋) → ∃𝑘 ∈ ((nei‘𝐽)‘{𝑥})(𝐽t 𝑘) ∈ Comp)
129, 11syldan 487 . . . . . . 7 (((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) → ∃𝑘 ∈ ((nei‘𝐽)‘{𝑥})(𝐽t 𝑘) ∈ Comp)
131ad3antrrr 765 . . . . . . . . 9 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → 𝐽 ∈ Top)
14 difss 3715 . . . . . . . . . 10 (𝑋 ∖ (𝑘𝑢)) ⊆ 𝑋
154ntropn 20763 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ (𝑋 ∖ (𝑘𝑢)) ⊆ 𝑋) → ((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∈ 𝐽)
1613, 14, 15sylancl 693 . . . . . . . . 9 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → ((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∈ 𝐽)
17 simprl 793 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → 𝑘 ∈ ((nei‘𝐽)‘{𝑥}))
184neii1 20820 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑘 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑘𝑋)
1913, 17, 18syl2anc 692 . . . . . . . . . 10 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → 𝑘𝑋)
204ntropn 20763 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝑘𝑋) → ((int‘𝐽)‘𝑘) ∈ 𝐽)
2113, 19, 20syl2anc 692 . . . . . . . . 9 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → ((int‘𝐽)‘𝑘) ∈ 𝐽)
22 inopn 20629 . . . . . . . . 9 ((𝐽 ∈ Top ∧ ((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∈ 𝐽 ∧ ((int‘𝐽)‘𝑘) ∈ 𝐽) → (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ ((int‘𝐽)‘𝑘)) ∈ 𝐽)
2313, 16, 21, 22syl3anc 1323 . . . . . . . 8 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ ((int‘𝐽)‘𝑘)) ∈ 𝐽)
24 inss1 3811 . . . . . . . . . . 11 (((int‘𝐽)‘((𝑢𝑘) ∪ (𝑋𝑘))) ∩ 𝑘) ⊆ ((int‘𝐽)‘((𝑢𝑘) ∪ (𝑋𝑘)))
25 simplr 791 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → 𝑥𝑢)
264ntrss2 20771 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑘𝑋) → ((int‘𝐽)‘𝑘) ⊆ 𝑘)
2713, 19, 26syl2anc 692 . . . . . . . . . . . . . 14 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → ((int‘𝐽)‘𝑘) ⊆ 𝑘)
289adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → 𝑥𝑋)
2928snssd 4309 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → {𝑥} ⊆ 𝑋)
304neiint 20818 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ {𝑥} ⊆ 𝑋𝑘𝑋) → (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ↔ {𝑥} ⊆ ((int‘𝐽)‘𝑘)))
3113, 29, 19, 30syl3anc 1323 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ↔ {𝑥} ⊆ ((int‘𝐽)‘𝑘)))
3217, 31mpbid 222 . . . . . . . . . . . . . . 15 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → {𝑥} ⊆ ((int‘𝐽)‘𝑘))
33 vex 3189 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
3433snss 4286 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((int‘𝐽)‘𝑘) ↔ {𝑥} ⊆ ((int‘𝐽)‘𝑘))
3532, 34sylibr 224 . . . . . . . . . . . . . 14 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → 𝑥 ∈ ((int‘𝐽)‘𝑘))
3627, 35sseldd 3584 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → 𝑥𝑘)
3725, 36elind 3776 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → 𝑥 ∈ (𝑢𝑘))
38 simpllr 798 . . . . . . . . . . . . . . 15 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → 𝑢 ∈ (𝑘Gen‘𝐽))
39 simprr 795 . . . . . . . . . . . . . . 15 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → (𝐽t 𝑘) ∈ Comp)
40 kgeni 21250 . . . . . . . . . . . . . . 15 ((𝑢 ∈ (𝑘Gen‘𝐽) ∧ (𝐽t 𝑘) ∈ Comp) → (𝑢𝑘) ∈ (𝐽t 𝑘))
4138, 39, 40syl2anc 692 . . . . . . . . . . . . . 14 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → (𝑢𝑘) ∈ (𝐽t 𝑘))
42 vex 3189 . . . . . . . . . . . . . . . 16 𝑘 ∈ V
43 resttop 20874 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑘 ∈ V) → (𝐽t 𝑘) ∈ Top)
4413, 42, 43sylancl 693 . . . . . . . . . . . . . . 15 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → (𝐽t 𝑘) ∈ Top)
45 inss2 3812 . . . . . . . . . . . . . . . 16 (𝑢𝑘) ⊆ 𝑘
464restuni 20876 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑘𝑋) → 𝑘 = (𝐽t 𝑘))
4713, 19, 46syl2anc 692 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → 𝑘 = (𝐽t 𝑘))
4845, 47syl5sseq 3632 . . . . . . . . . . . . . . 15 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → (𝑢𝑘) ⊆ (𝐽t 𝑘))
49 eqid 2621 . . . . . . . . . . . . . . . 16 (𝐽t 𝑘) = (𝐽t 𝑘)
5049isopn3 20780 . . . . . . . . . . . . . . 15 (((𝐽t 𝑘) ∈ Top ∧ (𝑢𝑘) ⊆ (𝐽t 𝑘)) → ((𝑢𝑘) ∈ (𝐽t 𝑘) ↔ ((int‘(𝐽t 𝑘))‘(𝑢𝑘)) = (𝑢𝑘)))
5144, 48, 50syl2anc 692 . . . . . . . . . . . . . 14 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → ((𝑢𝑘) ∈ (𝐽t 𝑘) ↔ ((int‘(𝐽t 𝑘))‘(𝑢𝑘)) = (𝑢𝑘)))
5241, 51mpbid 222 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → ((int‘(𝐽t 𝑘))‘(𝑢𝑘)) = (𝑢𝑘))
5345a1i 11 . . . . . . . . . . . . . 14 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → (𝑢𝑘) ⊆ 𝑘)
54 eqid 2621 . . . . . . . . . . . . . . 15 (𝐽t 𝑘) = (𝐽t 𝑘)
554, 54restntr 20896 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑘𝑋 ∧ (𝑢𝑘) ⊆ 𝑘) → ((int‘(𝐽t 𝑘))‘(𝑢𝑘)) = (((int‘𝐽)‘((𝑢𝑘) ∪ (𝑋𝑘))) ∩ 𝑘))
5613, 19, 53, 55syl3anc 1323 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → ((int‘(𝐽t 𝑘))‘(𝑢𝑘)) = (((int‘𝐽)‘((𝑢𝑘) ∪ (𝑋𝑘))) ∩ 𝑘))
5752, 56eqtr3d 2657 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → (𝑢𝑘) = (((int‘𝐽)‘((𝑢𝑘) ∪ (𝑋𝑘))) ∩ 𝑘))
5837, 57eleqtrd 2700 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → 𝑥 ∈ (((int‘𝐽)‘((𝑢𝑘) ∪ (𝑋𝑘))) ∩ 𝑘))
5924, 58sseldi 3581 . . . . . . . . . 10 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → 𝑥 ∈ ((int‘𝐽)‘((𝑢𝑘) ∪ (𝑋𝑘))))
60 undif3 3864 . . . . . . . . . . . . 13 ((𝑢𝑘) ∪ (𝑋𝑘)) = (((𝑢𝑘) ∪ 𝑋) ∖ (𝑘 ∖ (𝑢𝑘)))
61 incom 3783 . . . . . . . . . . . . . . . 16 (𝑢𝑘) = (𝑘𝑢)
6261difeq2i 3703 . . . . . . . . . . . . . . 15 (𝑘 ∖ (𝑢𝑘)) = (𝑘 ∖ (𝑘𝑢))
63 difin 3839 . . . . . . . . . . . . . . 15 (𝑘 ∖ (𝑘𝑢)) = (𝑘𝑢)
6462, 63eqtri 2643 . . . . . . . . . . . . . 14 (𝑘 ∖ (𝑢𝑘)) = (𝑘𝑢)
6564difeq2i 3703 . . . . . . . . . . . . 13 (((𝑢𝑘) ∪ 𝑋) ∖ (𝑘 ∖ (𝑢𝑘))) = (((𝑢𝑘) ∪ 𝑋) ∖ (𝑘𝑢))
6660, 65eqtri 2643 . . . . . . . . . . . 12 ((𝑢𝑘) ∪ (𝑋𝑘)) = (((𝑢𝑘) ∪ 𝑋) ∖ (𝑘𝑢))
6745, 19syl5ss 3594 . . . . . . . . . . . . . 14 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → (𝑢𝑘) ⊆ 𝑋)
68 ssequn1 3761 . . . . . . . . . . . . . 14 ((𝑢𝑘) ⊆ 𝑋 ↔ ((𝑢𝑘) ∪ 𝑋) = 𝑋)
6967, 68sylib 208 . . . . . . . . . . . . 13 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → ((𝑢𝑘) ∪ 𝑋) = 𝑋)
7069difeq1d 3705 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → (((𝑢𝑘) ∪ 𝑋) ∖ (𝑘𝑢)) = (𝑋 ∖ (𝑘𝑢)))
7166, 70syl5eq 2667 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → ((𝑢𝑘) ∪ (𝑋𝑘)) = (𝑋 ∖ (𝑘𝑢)))
7271fveq2d 6152 . . . . . . . . . 10 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → ((int‘𝐽)‘((𝑢𝑘) ∪ (𝑋𝑘))) = ((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))))
7359, 72eleqtrd 2700 . . . . . . . . 9 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → 𝑥 ∈ ((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))))
7473, 35elind 3776 . . . . . . . 8 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → 𝑥 ∈ (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ ((int‘𝐽)‘𝑘)))
75 sslin 3817 . . . . . . . . . 10 (((int‘𝐽)‘𝑘) ⊆ 𝑘 → (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ ((int‘𝐽)‘𝑘)) ⊆ (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ 𝑘))
7627, 75syl 17 . . . . . . . . 9 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ ((int‘𝐽)‘𝑘)) ⊆ (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ 𝑘))
774ntrss2 20771 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ (𝑋 ∖ (𝑘𝑢)) ⊆ 𝑋) → ((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ⊆ (𝑋 ∖ (𝑘𝑢)))
7813, 14, 77sylancl 693 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → ((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ⊆ (𝑋 ∖ (𝑘𝑢)))
7978difss2d 3718 . . . . . . . . . . . 12 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → ((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ⊆ 𝑋)
80 reldisj 3992 . . . . . . . . . . . 12 (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ⊆ 𝑋 → ((((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ (𝑘𝑢)) = ∅ ↔ ((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ⊆ (𝑋 ∖ (𝑘𝑢))))
8179, 80syl 17 . . . . . . . . . . 11 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → ((((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ (𝑘𝑢)) = ∅ ↔ ((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ⊆ (𝑋 ∖ (𝑘𝑢))))
8278, 81mpbird 247 . . . . . . . . . 10 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ (𝑘𝑢)) = ∅)
83 inssdif0 3921 . . . . . . . . . 10 ((((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ 𝑘) ⊆ 𝑢 ↔ (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ (𝑘𝑢)) = ∅)
8482, 83sylibr 224 . . . . . . . . 9 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ 𝑘) ⊆ 𝑢)
8576, 84sstrd 3593 . . . . . . . 8 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ ((int‘𝐽)‘𝑘)) ⊆ 𝑢)
86 eleq2 2687 . . . . . . . . . 10 (𝑧 = (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ ((int‘𝐽)‘𝑘)) → (𝑥𝑧𝑥 ∈ (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ ((int‘𝐽)‘𝑘))))
87 sseq1 3605 . . . . . . . . . 10 (𝑧 = (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ ((int‘𝐽)‘𝑘)) → (𝑧𝑢 ↔ (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ ((int‘𝐽)‘𝑘)) ⊆ 𝑢))
8886, 87anbi12d 746 . . . . . . . . 9 (𝑧 = (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ ((int‘𝐽)‘𝑘)) → ((𝑥𝑧𝑧𝑢) ↔ (𝑥 ∈ (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ ((int‘𝐽)‘𝑘)) ∧ (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ ((int‘𝐽)‘𝑘)) ⊆ 𝑢)))
8988rspcev 3295 . . . . . . . 8 (((((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ ((int‘𝐽)‘𝑘)) ∈ 𝐽 ∧ (𝑥 ∈ (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ ((int‘𝐽)‘𝑘)) ∧ (((int‘𝐽)‘(𝑋 ∖ (𝑘𝑢))) ∩ ((int‘𝐽)‘𝑘)) ⊆ 𝑢)) → ∃𝑧𝐽 (𝑥𝑧𝑧𝑢))
9023, 74, 85, 89syl12anc 1321 . . . . . . 7 ((((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) ∧ (𝑘 ∈ ((nei‘𝐽)‘{𝑥}) ∧ (𝐽t 𝑘) ∈ Comp)) → ∃𝑧𝐽 (𝑥𝑧𝑧𝑢))
9112, 90rexlimddv 3028 . . . . . 6 (((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) ∧ 𝑥𝑢) → ∃𝑧𝐽 (𝑥𝑧𝑧𝑢))
9291ralrimiva 2960 . . . . 5 ((𝜑𝑢 ∈ (𝑘Gen‘𝐽)) → ∀𝑥𝑢𝑧𝐽 (𝑥𝑧𝑧𝑢))
9392ex 450 . . . 4 (𝜑 → (𝑢 ∈ (𝑘Gen‘𝐽) → ∀𝑥𝑢𝑧𝐽 (𝑥𝑧𝑧𝑢)))
94 eltop2 20690 . . . . 5 (𝐽 ∈ Top → (𝑢𝐽 ↔ ∀𝑥𝑢𝑧𝐽 (𝑥𝑧𝑧𝑢)))
951, 94syl 17 . . . 4 (𝜑 → (𝑢𝐽 ↔ ∀𝑥𝑢𝑧𝐽 (𝑥𝑧𝑧𝑢)))
9693, 95sylibrd 249 . . 3 (𝜑 → (𝑢 ∈ (𝑘Gen‘𝐽) → 𝑢𝐽))
9796ssrdv 3589 . 2 (𝜑 → (𝑘Gen‘𝐽) ⊆ 𝐽)
98 iskgen2 21261 . 2 (𝐽 ∈ ran 𝑘Gen ↔ (𝐽 ∈ Top ∧ (𝑘Gen‘𝐽) ⊆ 𝐽))
991, 97, 98sylanbrc 697 1 (𝜑𝐽 ∈ ran 𝑘Gen)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2907  wrex 2908  Vcvv 3186  cdif 3552  cun 3553  cin 3554  wss 3555  c0 3891  {csn 4148   cuni 4402  ran crn 5075  cfv 5847  (class class class)co 6604  t crest 16002  Topctop 20617  intcnt 20731  neicnei 20811  Compccmp 21099  𝑘Genckgen 21246
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-oadd 7509  df-er 7687  df-en 7900  df-fin 7903  df-fi 8261  df-rest 16004  df-topgen 16025  df-top 20621  df-bases 20622  df-topon 20623  df-ntr 20734  df-nei 20812  df-cmp 21100  df-kgen 21247
This theorem is referenced by:  cmpkgen  21264  llycmpkgen  21265
  Copyright terms: Public domain W3C validator