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 )