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

Metamath Proof Explorer

Theorem cmpkgen

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

Ref Expression
Assertion cmpkgen ( 𝐽 ∈ Comp → 𝐽 ∈ ran 𝑘Gen )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
2 cmptop ⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
3 2 adantr ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝐽 ∈ Top )
4 1 topopn ⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽 )
5 3 4 syl ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑥 ∈ ∪ 𝐽 ) → ∪ 𝐽 ∈ 𝐽 )
6 simpr ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝑥 ∈ ∪ 𝐽 )
7 6 snssd ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑥 ∈ ∪ 𝐽 ) → { 𝑥 } ⊆ ∪ 𝐽 )
8 opnneiss ⊢ ( ( 𝐽 ∈ Top ∧ ∪ 𝐽 ∈ 𝐽 ∧ { 𝑥 } ⊆ ∪ 𝐽 ) → ∪ 𝐽 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
9 3 5 7 8 syl3anc ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑥 ∈ ∪ 𝐽 ) → ∪ 𝐽 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
10 1 restid ⊢ ( 𝐽 ∈ Top → ( 𝐽 ↾t ∪ 𝐽 ) = 𝐽 )
11 3 10 syl ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑥 ∈ ∪ 𝐽 ) → ( 𝐽 ↾t ∪ 𝐽 ) = 𝐽 )
12 simpl ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝐽 ∈ Comp )
13 11 12 eqeltrd ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑥 ∈ ∪ 𝐽 ) → ( 𝐽 ↾t ∪ 𝐽 ) ∈ Comp )
14 oveq2 ⊢ ( 𝑘 = ∪ 𝐽 → ( 𝐽 ↾t 𝑘 ) = ( 𝐽 ↾t ∪ 𝐽 ) )
15 14 eleq1d ⊢ ( 𝑘 = ∪ 𝐽 → ( ( 𝐽 ↾t 𝑘 ) ∈ Comp ↔ ( 𝐽 ↾t ∪ 𝐽 ) ∈ Comp ) )
16 15 rspcev ⊢ ( ( ∪ 𝐽 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ∧ ( 𝐽 ↾t ∪ 𝐽 ) ∈ Comp ) → ∃ 𝑘 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝐽 ↾t 𝑘 ) ∈ Comp )
17 9 13 16 syl2anc ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑥 ∈ ∪ 𝐽 ) → ∃ 𝑘 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ( 𝐽 ↾t 𝑘 ) ∈ Comp )
18 1 2 17 llycmpkgen2 ⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ ran 𝑘Gen )