Metamath Proof Explorer

Theorem kgenss

Description: The compact generator generates a finer topology than the original. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion kgenss ⊢ J ∈ Top → J ⊆ 𝑘Gen ⁡ J

Proof

Step Hyp Ref Expression
1 elssuni ⊢ x ∈ J → x ⊆ ⋃ J
2 1 a1i ⊢ J ∈ Top → x ∈ J → x ⊆ ⋃ J
3 elrestr ⊢ J ∈ Top ∧ k ∈ 𝒫 ⋃ J ∧ x ∈ J → x ∩ k ∈ J ↾ 𝑡 k
4 3 3expa ⊢ J ∈ Top ∧ k ∈ 𝒫 ⋃ J ∧ x ∈ J → x ∩ k ∈ J ↾ 𝑡 k
5 4 an32s ⊢ J ∈ Top ∧ x ∈ J ∧ k ∈ 𝒫 ⋃ J → x ∩ k ∈ J ↾ 𝑡 k
6 5 a1d ⊢ J ∈ Top ∧ x ∈ J ∧ k ∈ 𝒫 ⋃ J → J ↾ 𝑡 k ∈ Comp → x ∩ k ∈ J ↾ 𝑡 k
7 6 ralrimiva ⊢ J ∈ Top ∧ x ∈ J → ∀ k ∈ 𝒫 ⋃ J J ↾ 𝑡 k ∈ Comp → x ∩ k ∈ J ↾ 𝑡 k
8 7 ex ⊢ J ∈ Top → x ∈ J → ∀ k ∈ 𝒫 ⋃ J J ↾ 𝑡 k ∈ Comp → x ∩ k ∈ J ↾ 𝑡 k
9 2 8 jcad ⊢ J ∈ Top → x ∈ J → x ⊆ ⋃ J ∧ ∀ k ∈ 𝒫 ⋃ J J ↾ 𝑡 k ∈ Comp → x ∩ k ∈ J ↾ 𝑡 k
10 toptopon2 ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ ⋃ J
11 elkgen ⊢ J ∈ TopOn ⁡ ⋃ J → x ∈ 𝑘Gen ⁡ J ↔ x ⊆ ⋃ J ∧ ∀ k ∈ 𝒫 ⋃ J J ↾ 𝑡 k ∈ Comp → x ∩ k ∈ J ↾ 𝑡 k
12 10 11 sylbi ⊢ J ∈ Top → x ∈ 𝑘Gen ⁡ J ↔ x ⊆ ⋃ J ∧ ∀ k ∈ 𝒫 ⋃ J J ↾ 𝑡 k ∈ Comp → x ∩ k ∈ J ↾ 𝑡 k
13 9 12 sylibrd ⊢ J ∈ Top → x ∈ J → x ∈ 𝑘Gen ⁡ J
14 13 ssrdv ⊢ J ∈ Top → J ⊆ 𝑘Gen ⁡ J