Metamath Proof Explorer

Theorem llycmpkgen

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

Ref Expression
Assertion llycmpkgen ( 𝐽 ∈ 𝑛-Locally Comp β†’ 𝐽 ∈ ran π‘˜Gen )

Proof

Step Hyp Ref Expression
1 eqid ⊒ βˆͺ 𝐽 = βˆͺ 𝐽
2 nllytop ⊒ ( 𝐽 ∈ 𝑛-Locally Comp β†’ 𝐽 ∈ Top )
3 simpl ⊒ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ π‘₯ ∈ βˆͺ 𝐽 ) β†’ 𝐽 ∈ 𝑛-Locally Comp )
4 1 topopn ⊒ ( 𝐽 ∈ Top β†’ βˆͺ 𝐽 ∈ 𝐽 )
5 2 4 syl ⊒ ( 𝐽 ∈ 𝑛-Locally Comp β†’ βˆͺ 𝐽 ∈ 𝐽 )
6 5 adantr ⊒ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ π‘₯ ∈ βˆͺ 𝐽 ) β†’ βˆͺ 𝐽 ∈ 𝐽 )
7 simpr ⊒ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ π‘₯ ∈ βˆͺ 𝐽 ) β†’ π‘₯ ∈ βˆͺ 𝐽 )
8 nllyi ⊒ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ βˆͺ 𝐽 ∈ 𝐽 ∧ π‘₯ ∈ βˆͺ 𝐽 ) β†’ βˆƒ π‘˜ ∈ ( ( nei β€˜ 𝐽 ) β€˜ { π‘₯ } ) ( π‘˜ βŠ† βˆͺ 𝐽 ∧ ( 𝐽 β†Ύt π‘˜ ) ∈ Comp ) )
9 3 6 7 8 syl3anc ⊒ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ π‘₯ ∈ βˆͺ 𝐽 ) β†’ βˆƒ π‘˜ ∈ ( ( nei β€˜ 𝐽 ) β€˜ { π‘₯ } ) ( π‘˜ βŠ† βˆͺ 𝐽 ∧ ( 𝐽 β†Ύt π‘˜ ) ∈ Comp ) )
10 simpr ⊒ ( ( π‘˜ βŠ† βˆͺ 𝐽 ∧ ( 𝐽 β†Ύt π‘˜ ) ∈ Comp ) β†’ ( 𝐽 β†Ύt π‘˜ ) ∈ Comp )
11 10 reximi ⊒ ( βˆƒ π‘˜ ∈ ( ( nei β€˜ 𝐽 ) β€˜ { π‘₯ } ) ( π‘˜ βŠ† βˆͺ 𝐽 ∧ ( 𝐽 β†Ύt π‘˜ ) ∈ Comp ) β†’ βˆƒ π‘˜ ∈ ( ( nei β€˜ 𝐽 ) β€˜ { π‘₯ } ) ( 𝐽 β†Ύt π‘˜ ) ∈ Comp )
12 9 11 syl ⊒ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ π‘₯ ∈ βˆͺ 𝐽 ) β†’ βˆƒ π‘˜ ∈ ( ( nei β€˜ 𝐽 ) β€˜ { π‘₯ } ) ( 𝐽 β†Ύt π‘˜ ) ∈ Comp )
13 1 2 12 llycmpkgen2 ⊒ ( 𝐽 ∈ 𝑛-Locally Comp β†’ 𝐽 ∈ ran π‘˜Gen )