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 eqtr3id
 |-  ( ( ( 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 )