Metamath Proof Explorer

Theorem cmpkgen

Description: A compact space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion cmpkgen ⊢ J ∈ Comp → J ∈ ran ⁡ 𝑘Gen

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 cmptop ⊢ J ∈ Comp → J ∈ Top
3 2 adantr ⊢ J ∈ Comp ∧ x ∈ ⋃ J → J ∈ Top
4 1 topopn ⊢ J ∈ Top → ⋃ J ∈ J
5 3 4 syl ⊢ J ∈ Comp ∧ x ∈ ⋃ J → ⋃ J ∈ J
6 simpr ⊢ J ∈ Comp ∧ x ∈ ⋃ J → x ∈ ⋃ J
7 6 snssd ⊢ J ∈ Comp ∧ x ∈ ⋃ J → x ⊆ ⋃ J
8 opnneiss ⊢ J ∈ Top ∧ ⋃ J ∈ J ∧ x ⊆ ⋃ J → ⋃ J ∈ nei ⁡ J ⁡ x
9 3 5 7 8 syl3anc ⊢ J ∈ Comp ∧ x ∈ ⋃ J → ⋃ J ∈ nei ⁡ J ⁡ x
10 1 restid ⊢ J ∈ Top → J ↾ 𝑡 ⋃ J = J
11 3 10 syl ⊢ J ∈ Comp ∧ x ∈ ⋃ J → J ↾ 𝑡 ⋃ J = J
12 simpl ⊢ J ∈ Comp ∧ x ∈ ⋃ J → J ∈ Comp
13 11 12 eqeltrd ⊢ J ∈ Comp ∧ x ∈ ⋃ J → J ↾ 𝑡 ⋃ J ∈ Comp
14 oveq2 ⊢ k = ⋃ J → J ↾ 𝑡 k = J ↾ 𝑡 ⋃ J
15 14 eleq1d ⊢ k = ⋃ J → J ↾ 𝑡 k ∈ Comp ↔ J ↾ 𝑡 ⋃ J ∈ Comp
16 15 rspcev ⊢ ⋃ J ∈ nei ⁡ J ⁡ x ∧ J ↾ 𝑡 ⋃ J ∈ Comp → ∃ k ∈ nei ⁡ J ⁡ x J ↾ 𝑡 k ∈ Comp
17 9 13 16 syl2anc ⊢ J ∈ Comp ∧ x ∈ ⋃ J → ∃ k ∈ nei ⁡ J ⁡ x J ↾ 𝑡 k ∈ Comp
18 1 2 17 llycmpkgen2 ⊢ J ∈ Comp → J ∈ ran ⁡ 𝑘Gen