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 )