# Metamath Proof Explorer

## Theorem 1stckgen

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

Ref Expression
Assertion 1stckgen ${⊢}{J}\in {1}^{st}𝜔\to {J}\in \mathrm{ran}\mathrm{𝑘Gen}$

### Proof

Step Hyp Ref Expression
1 1stctop ${⊢}{J}\in {1}^{st}𝜔\to {J}\in \mathrm{Top}$
2 difss ${⊢}\bigcup {J}\setminus {x}\subseteq \bigcup {J}$
3 eqid ${⊢}\bigcup {J}=\bigcup {J}$
4 3 1stcelcls
5 2 4 mpan2
7 1 adantr ${⊢}\left({J}\in {1}^{st}𝜔\wedge {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)\to {J}\in \mathrm{Top}$
9 toptopon2 ${⊢}{J}\in \mathrm{Top}↔{J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
10 8 9 sylib
11 simprr
12 lmcl
13 10 11 12 syl2anc
14 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
15 vex ${⊢}{f}\in \mathrm{V}$
16 15 rnex ${⊢}\mathrm{ran}{f}\in \mathrm{V}$
17 snex ${⊢}\left\{{y}\right\}\in \mathrm{V}$
18 16 17 unex ${⊢}\mathrm{ran}{f}\cup \left\{{y}\right\}\in \mathrm{V}$
19 resttop ${⊢}\left({J}\in \mathrm{Top}\wedge \mathrm{ran}{f}\cup \left\{{y}\right\}\in \mathrm{V}\right)\to {J}{↾}_{𝑡}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\in \mathrm{Top}$
20 8 18 19 sylancl
21 toptopon2 ${⊢}{J}{↾}_{𝑡}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\in \mathrm{Top}↔{J}{↾}_{𝑡}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\in \mathrm{TopOn}\left(\bigcup \left({J}{↾}_{𝑡}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\right)\right)$
22 20 21 sylib
23 1zzd
24 eqid ${⊢}{J}{↾}_{𝑡}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)={J}{↾}_{𝑡}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)$
25 18 a1i
26 ssun2 ${⊢}\left\{{y}\right\}\subseteq \mathrm{ran}{f}\cup \left\{{y}\right\}$
27 vex ${⊢}{y}\in \mathrm{V}$
28 27 snss ${⊢}{y}\in \left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)↔\left\{{y}\right\}\subseteq \mathrm{ran}{f}\cup \left\{{y}\right\}$
29 26 28 mpbir ${⊢}{y}\in \left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)$
30 29 a1i
31 ffn ${⊢}{f}:ℕ⟶\bigcup {J}\setminus {x}\to {f}Fnℕ$
33 dffn3 ${⊢}{f}Fnℕ↔{f}:ℕ⟶\mathrm{ran}{f}$
34 32 33 sylib
35 ssun1 ${⊢}\mathrm{ran}{f}\subseteq \mathrm{ran}{f}\cup \left\{{y}\right\}$
36 fss ${⊢}\left({f}:ℕ⟶\mathrm{ran}{f}\wedge \mathrm{ran}{f}\subseteq \mathrm{ran}{f}\cup \left\{{y}\right\}\right)\to {f}:ℕ⟶\mathrm{ran}{f}\cup \left\{{y}\right\}$
37 34 35 36 sylancl
38 24 14 25 8 30 23 37 lmss
39 11 38 mpbid
40 37 ffvelrnda
41 simprl
42 41 ffvelrnda
43 42 eldifbd
44 40 43 eldifd
45 difin ${⊢}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\setminus \left(\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\cap {x}\right)=\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\setminus {x}$
46 frn ${⊢}{f}:ℕ⟶\bigcup {J}\setminus {x}\to \mathrm{ran}{f}\subseteq \bigcup {J}\setminus {x}$
48 47 difss2d
49 13 snssd
50 48 49 unssd
51 3 restuni ${⊢}\left({J}\in \mathrm{Top}\wedge \mathrm{ran}{f}\cup \left\{{y}\right\}\subseteq \bigcup {J}\right)\to \mathrm{ran}{f}\cup \left\{{y}\right\}=\bigcup \left({J}{↾}_{𝑡}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\right)$
52 8 50 51 syl2anc
53 52 difeq1d
54 45 53 syl5eqr
55 incom ${⊢}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\cap {x}={x}\cap \left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)$
56 simplr
57 fss ${⊢}\left({f}:ℕ⟶\bigcup {J}\setminus {x}\wedge \bigcup {J}\setminus {x}\subseteq \bigcup {J}\right)\to {f}:ℕ⟶\bigcup {J}$
58 41 2 57 sylancl
59 10 58 11 1stckgenlem
60 kgeni ${⊢}\left({x}\in \mathrm{𝑘Gen}\left({J}\right)\wedge {J}{↾}_{𝑡}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\in \mathrm{Comp}\right)\to {x}\cap \left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\in \left({J}{↾}_{𝑡}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\right)$
61 56 59 60 syl2anc
62 55 61 eqeltrid
63 eqid ${⊢}\bigcup \left({J}{↾}_{𝑡}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\right)=\bigcup \left({J}{↾}_{𝑡}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\right)$
64 63 opncld ${⊢}\left({J}{↾}_{𝑡}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\in \mathrm{Top}\wedge \left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\cap {x}\in \left({J}{↾}_{𝑡}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\right)\right)\to \bigcup \left({J}{↾}_{𝑡}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\right)\setminus \left(\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\cap {x}\right)\in \mathrm{Clsd}\left({J}{↾}_{𝑡}\left(\mathrm{ran}{f}\cup \left\{{y}\right\}\right)\right)$
65 20 62 64 syl2anc
66 54 65 eqeltrd
67 14 22 23 39 44 66 lmcld
68 67 eldifbd
69 13 68 eldifd
70 69 ex
71 70 exlimdv
72 6 71 sylbid ${⊢}\left({J}\in {1}^{st}𝜔\wedge {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)\to \left({y}\in \mathrm{cls}\left({J}\right)\left(\bigcup {J}\setminus {x}\right)\to {y}\in \left(\bigcup {J}\setminus {x}\right)\right)$
73 72 ssrdv ${⊢}\left({J}\in {1}^{st}𝜔\wedge {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)\to \mathrm{cls}\left({J}\right)\left(\bigcup {J}\setminus {x}\right)\subseteq \bigcup {J}\setminus {x}$
74 3 iscld4 ${⊢}\left({J}\in \mathrm{Top}\wedge \bigcup {J}\setminus {x}\subseteq \bigcup {J}\right)\to \left(\bigcup {J}\setminus {x}\in \mathrm{Clsd}\left({J}\right)↔\mathrm{cls}\left({J}\right)\left(\bigcup {J}\setminus {x}\right)\subseteq \bigcup {J}\setminus {x}\right)$
75 7 2 74 sylancl ${⊢}\left({J}\in {1}^{st}𝜔\wedge {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)\to \left(\bigcup {J}\setminus {x}\in \mathrm{Clsd}\left({J}\right)↔\mathrm{cls}\left({J}\right)\left(\bigcup {J}\setminus {x}\right)\subseteq \bigcup {J}\setminus {x}\right)$
76 73 75 mpbird ${⊢}\left({J}\in {1}^{st}𝜔\wedge {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)\to \bigcup {J}\setminus {x}\in \mathrm{Clsd}\left({J}\right)$
77 elssuni ${⊢}{x}\in \mathrm{𝑘Gen}\left({J}\right)\to {x}\subseteq \bigcup \mathrm{𝑘Gen}\left({J}\right)$
78 77 adantl ${⊢}\left({J}\in {1}^{st}𝜔\wedge {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)\to {x}\subseteq \bigcup \mathrm{𝑘Gen}\left({J}\right)$
79 3 kgenuni ${⊢}{J}\in \mathrm{Top}\to \bigcup {J}=\bigcup \mathrm{𝑘Gen}\left({J}\right)$
80 7 79 syl ${⊢}\left({J}\in {1}^{st}𝜔\wedge {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)\to \bigcup {J}=\bigcup \mathrm{𝑘Gen}\left({J}\right)$
81 78 80 sseqtrrd ${⊢}\left({J}\in {1}^{st}𝜔\wedge {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)\to {x}\subseteq \bigcup {J}$
82 3 isopn2 ${⊢}\left({J}\in \mathrm{Top}\wedge {x}\subseteq \bigcup {J}\right)\to \left({x}\in {J}↔\bigcup {J}\setminus {x}\in \mathrm{Clsd}\left({J}\right)\right)$
83 7 81 82 syl2anc ${⊢}\left({J}\in {1}^{st}𝜔\wedge {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)\to \left({x}\in {J}↔\bigcup {J}\setminus {x}\in \mathrm{Clsd}\left({J}\right)\right)$
84 76 83 mpbird ${⊢}\left({J}\in {1}^{st}𝜔\wedge {x}\in \mathrm{𝑘Gen}\left({J}\right)\right)\to {x}\in {J}$
85 84 ex ${⊢}{J}\in {1}^{st}𝜔\to \left({x}\in \mathrm{𝑘Gen}\left({J}\right)\to {x}\in {J}\right)$
86 85 ssrdv ${⊢}{J}\in {1}^{st}𝜔\to \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}$
87 iskgen2 ${⊢}{J}\in \mathrm{ran}\mathrm{𝑘Gen}↔\left({J}\in \mathrm{Top}\wedge \mathrm{𝑘Gen}\left({J}\right)\subseteq {J}\right)$
88 1 86 87 sylanbrc ${⊢}{J}\in {1}^{st}𝜔\to {J}\in \mathrm{ran}\mathrm{𝑘Gen}$