This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐽 ∈ Top → 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 elssuni ⊢ ( 𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽 )
2 1 a1i ⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽 ) )
3 elrestr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑘 ∈ 𝒫 ∪ 𝐽 ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) )
4 3 3expa ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑘 ∈ 𝒫 ∪ 𝐽 ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) )
5 4 an32s ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑘 ∈ 𝒫 ∪ 𝐽 ) → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) )
6 5 a1d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑘 ∈ 𝒫 ∪ 𝐽 ) → ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) )
7 6 ralrimiva ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → ∀ 𝑘 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) )
8 7 ex ⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ 𝐽 → ∀ 𝑘 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) )
9 2 8 jcad ⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ 𝐽 → ( 𝑥 ⊆ ∪ 𝐽 ∧ ∀ 𝑘 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )
10 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
11 elkgen ⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( 𝑥 ⊆ ∪ 𝐽 ∧ ∀ 𝑘 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )
12 10 11 sylbi ⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( 𝑥 ⊆ ∪ 𝐽 ∧ ∀ 𝑘 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝑥 ∩ 𝑘 ) ∈ ( 𝐽 ↾t 𝑘 ) ) ) ) )
13 9 12 sylibrd ⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ 𝐽 → 𝑥 ∈ ( 𝑘Gen ‘ 𝐽 ) ) )
14 13 ssrdv ⊢ ( 𝐽 ∈ Top → 𝐽 ⊆ ( 𝑘Gen ‘ 𝐽 ) )