Metamath Proof Explorer

Theorem kgencn2

Description: A function F : J --> K from a compactly generated space is continuous iff for all compact spaces z and continuous g : z --> J , the composite F o. g : z --> K is continuous. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion kgencn2 
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( ( kGen ` J ) Cn K ) <-> ( F : X --> Y /\ A. z e. Comp A. g e. ( z Cn J ) ( F o. g ) e. ( z Cn K ) ) ) )

Proof

Step Hyp Ref Expression
1 kgencn 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( ( kGen ` J ) Cn K ) <-> ( F : X --> Y /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) ) ) )
2 rncmp 
 |-  ( ( z e. Comp /\ g e. ( z Cn J ) ) -> ( J |`t ran g ) e. Comp )
3 2 adantl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ ( z e. Comp /\ g e. ( z Cn J ) ) ) -> ( J |`t ran g ) e. Comp )
4 simprr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ ( z e. Comp /\ g e. ( z Cn J ) ) ) -> g e. ( z Cn J ) )
5 eqid 
 |-  U. z = U. z
6 eqid 
 |-  U. J = U. J
7 5 6 cnf 
 |-  ( g e. ( z Cn J ) -> g : U. z --> U. J )
8 frn 
 |-  ( g : U. z --> U. J -> ran g C_ U. J )
9 4 7 8 3syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ ( z e. Comp /\ g e. ( z Cn J ) ) ) -> ran g C_ U. J )
10 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
11 10 ad3antrrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ ( z e. Comp /\ g e. ( z Cn J ) ) ) -> X = U. J )
12 9 11 sseqtrrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ ( z e. Comp /\ g e. ( z Cn J ) ) ) -> ran g C_ X )
13 vex 
 |-  g e. _V
14 13 rnex 
 |-  ran g e. _V
15 14 elpw 
 |-  ( ran g e. ~P X <-> ran g C_ X )
16 12 15 sylibr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ ( z e. Comp /\ g e. ( z Cn J ) ) ) -> ran g e. ~P X )
17 oveq2 
 |-  ( k = ran g -> ( J |`t k ) = ( J |`t ran g ) )
18 17 eleq1d 
 |-  ( k = ran g -> ( ( J |`t k ) e. Comp <-> ( J |`t ran g ) e. Comp ) )
19 reseq2 
 |-  ( k = ran g -> ( F |` k ) = ( F |` ran g ) )
20 17 oveq1d 
 |-  ( k = ran g -> ( ( J |`t k ) Cn K ) = ( ( J |`t ran g ) Cn K ) )
21 19 20 eleq12d 
 |-  ( k = ran g -> ( ( F |` k ) e. ( ( J |`t k ) Cn K ) <-> ( F |` ran g ) e. ( ( J |`t ran g ) Cn K ) ) )
22 18 21 imbi12d 
 |-  ( k = ran g -> ( ( ( J |`t k ) e. Comp -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) <-> ( ( J |`t ran g ) e. Comp -> ( F |` ran g ) e. ( ( J |`t ran g ) Cn K ) ) ) )
23 22 rspcv 
 |-  ( ran g e. ~P X -> ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) -> ( ( J |`t ran g ) e. Comp -> ( F |` ran g ) e. ( ( J |`t ran g ) Cn K ) ) ) )
24 16 23 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ ( z e. Comp /\ g e. ( z Cn J ) ) ) -> ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) -> ( ( J |`t ran g ) e. Comp -> ( F |` ran g ) e. ( ( J |`t ran g ) Cn K ) ) ) )
25 3 24 mpid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ ( z e. Comp /\ g e. ( z Cn J ) ) ) -> ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) -> ( F |` ran g ) e. ( ( J |`t ran g ) Cn K ) ) )
26 simplll 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ ( z e. Comp /\ g e. ( z Cn J ) ) ) -> J e. ( TopOn ` X ) )
27 ssidd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ ( z e. Comp /\ g e. ( z Cn J ) ) ) -> ran g C_ ran g )
28 cnrest2 
 |-  ( ( J e. ( TopOn ` X ) /\ ran g C_ ran g /\ ran g C_ X ) -> ( g e. ( z Cn J ) <-> g e. ( z Cn ( J |`t ran g ) ) ) )
29 26 27 12 28 syl3anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ ( z e. Comp /\ g e. ( z Cn J ) ) ) -> ( g e. ( z Cn J ) <-> g e. ( z Cn ( J |`t ran g ) ) ) )
30 4 29 mpbid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ ( z e. Comp /\ g e. ( z Cn J ) ) ) -> g e. ( z Cn ( J |`t ran g ) ) )
31 cnco 
 |-  ( ( g e. ( z Cn ( J |`t ran g ) ) /\ ( F |` ran g ) e. ( ( J |`t ran g ) Cn K ) ) -> ( ( F |` ran g ) o. g ) e. ( z Cn K ) )
32 31 ex 
 |-  ( g e. ( z Cn ( J |`t ran g ) ) -> ( ( F |` ran g ) e. ( ( J |`t ran g ) Cn K ) -> ( ( F |` ran g ) o. g ) e. ( z Cn K ) ) )
33 30 32 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ ( z e. Comp /\ g e. ( z Cn J ) ) ) -> ( ( F |` ran g ) e. ( ( J |`t ran g ) Cn K ) -> ( ( F |` ran g ) o. g ) e. ( z Cn K ) ) )
34 ssid 
 |-  ran g C_ ran g
35 cores 
 |-  ( ran g C_ ran g -> ( ( F |` ran g ) o. g ) = ( F o. g ) )
36 34 35 ax-mp 
 |-  ( ( F |` ran g ) o. g ) = ( F o. g )
37 36 eleq1i 
 |-  ( ( ( F |` ran g ) o. g ) e. ( z Cn K ) <-> ( F o. g ) e. ( z Cn K ) )
38 33 37 syl6ib 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ ( z e. Comp /\ g e. ( z Cn J ) ) ) -> ( ( F |` ran g ) e. ( ( J |`t ran g ) Cn K ) -> ( F o. g ) e. ( z Cn K ) ) )
39 25 38 syld 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ ( z e. Comp /\ g e. ( z Cn J ) ) ) -> ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) -> ( F o. g ) e. ( z Cn K ) ) )
40 39 ralrimdvva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) -> A. z e. Comp A. g e. ( z Cn J ) ( F o. g ) e. ( z Cn K ) ) )
41 oveq1 
 |-  ( z = ( J |`t k ) -> ( z Cn J ) = ( ( J |`t k ) Cn J ) )
42 oveq1 
 |-  ( z = ( J |`t k ) -> ( z Cn K ) = ( ( J |`t k ) Cn K ) )
43 42 eleq2d 
 |-  ( z = ( J |`t k ) -> ( ( F o. g ) e. ( z Cn K ) <-> ( F o. g ) e. ( ( J |`t k ) Cn K ) ) )
44 41 43 raleqbidv 
 |-  ( z = ( J |`t k ) -> ( A. g e. ( z Cn J ) ( F o. g ) e. ( z Cn K ) <-> A. g e. ( ( J |`t k ) Cn J ) ( F o. g ) e. ( ( J |`t k ) Cn K ) ) )
45 44 rspcv 
 |-  ( ( J |`t k ) e. Comp -> ( A. z e. Comp A. g e. ( z Cn J ) ( F o. g ) e. ( z Cn K ) -> A. g e. ( ( J |`t k ) Cn J ) ( F o. g ) e. ( ( J |`t k ) Cn K ) ) )
46 elpwi 
 |-  ( k e. ~P X -> k C_ X )
47 46 adantl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> k C_ X )
48 47 resabs1d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> ( ( _I |` X ) |` k ) = ( _I |` k ) )
49 idcn 
 |-  ( J e. ( TopOn ` X ) -> ( _I |` X ) e. ( J Cn J ) )
50 49 ad3antrrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> ( _I |` X ) e. ( J Cn J ) )
51 10 ad3antrrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> X = U. J )
52 47 51 sseqtrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> k C_ U. J )
53 6 cnrest 
 |-  ( ( ( _I |` X ) e. ( J Cn J ) /\ k C_ U. J ) -> ( ( _I |` X ) |` k ) e. ( ( J |`t k ) Cn J ) )
54 50 52 53 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> ( ( _I |` X ) |` k ) e. ( ( J |`t k ) Cn J ) )
55 48 54 eqeltrrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> ( _I |` k ) e. ( ( J |`t k ) Cn J ) )
56 coeq2 
 |-  ( g = ( _I |` k ) -> ( F o. g ) = ( F o. ( _I |` k ) ) )
57 56 eleq1d 
 |-  ( g = ( _I |` k ) -> ( ( F o. g ) e. ( ( J |`t k ) Cn K ) <-> ( F o. ( _I |` k ) ) e. ( ( J |`t k ) Cn K ) ) )
58 57 rspcv 
 |-  ( ( _I |` k ) e. ( ( J |`t k ) Cn J ) -> ( A. g e. ( ( J |`t k ) Cn J ) ( F o. g ) e. ( ( J |`t k ) Cn K ) -> ( F o. ( _I |` k ) ) e. ( ( J |`t k ) Cn K ) ) )
59 55 58 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> ( A. g e. ( ( J |`t k ) Cn J ) ( F o. g ) e. ( ( J |`t k ) Cn K ) -> ( F o. ( _I |` k ) ) e. ( ( J |`t k ) Cn K ) ) )
60 coires1 
 |-  ( F o. ( _I |` k ) ) = ( F |` k )
61 60 eleq1i 
 |-  ( ( F o. ( _I |` k ) ) e. ( ( J |`t k ) Cn K ) <-> ( F |` k ) e. ( ( J |`t k ) Cn K ) )
62 59 61 syl6ib 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> ( A. g e. ( ( J |`t k ) Cn J ) ( F o. g ) e. ( ( J |`t k ) Cn K ) -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) )
63 45 62 syl9r 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> ( ( J |`t k ) e. Comp -> ( A. z e. Comp A. g e. ( z Cn J ) ( F o. g ) e. ( z Cn K ) -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) ) )
64 63 com23 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> ( A. z e. Comp A. g e. ( z Cn J ) ( F o. g ) e. ( z Cn K ) -> ( ( J |`t k ) e. Comp -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) ) )
65 64 ralrimdva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( A. z e. Comp A. g e. ( z Cn J ) ( F o. g ) e. ( z Cn K ) -> A. k e. ~P X ( ( J |`t k ) e. Comp -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) ) )
66 40 65 impbid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( A. k e. ~P X ( ( J |`t k ) e. Comp -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) <-> A. z e. Comp A. g e. ( z Cn J ) ( F o. g ) e. ( z Cn K ) ) )
67 66 pm5.32da 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( F : X --> Y /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) ) <-> ( F : X --> Y /\ A. z e. Comp A. g e. ( z Cn J ) ( F o. g ) e. ( z Cn K ) ) ) )
68 1 67 bitrd 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( ( kGen ` J ) Cn K ) <-> ( F : X --> Y /\ A. z e. Comp A. g e. ( z Cn J ) ( F o. g ) e. ( z Cn K ) ) ) )