# 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 e. 1stc -> J e. ran kGen )`

### Proof

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