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 1 st 𝜔 J ran 𝑘Gen

Proof

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