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 )