Metamath Proof Explorer

Theorem kgencn

Description: A function from a compactly generated space is continuous iff it is continuous "on compacta". (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 kgentopon 
 |-  ( J e. ( TopOn ` X ) -> ( kGen ` J ) e. ( TopOn ` X ) )
2 iscn 
 |-  ( ( ( kGen ` J ) e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( ( kGen ` J ) Cn K ) <-> ( F : X --> Y /\ A. x e. K ( `' F " x ) e. ( kGen ` J ) ) ) )
3 1 2 sylan 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( ( kGen ` J ) Cn K ) <-> ( F : X --> Y /\ A. x e. K ( `' F " x ) e. ( kGen ` J ) ) ) )
4 cnvimass 
 |-  ( `' F " x ) C_ dom F
5 fdm 
 |-  ( F : X --> Y -> dom F = X )
6 5 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> dom F = X )
7 4 6 sseqtrid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( `' F " x ) C_ X )
8 elkgen 
 |-  ( J e. ( TopOn ` X ) -> ( ( `' F " x ) e. ( kGen ` J ) <-> ( ( `' F " x ) C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( ( `' F " x ) i^i k ) e. ( J |`t k ) ) ) ) )
9 8 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( ( `' F " x ) e. ( kGen ` J ) <-> ( ( `' F " x ) C_ X /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( ( `' F " x ) i^i k ) e. ( J |`t k ) ) ) ) )
10 7 9 mpbirand 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( ( `' F " x ) e. ( kGen ` J ) <-> A. k e. ~P X ( ( J |`t k ) e. Comp -> ( ( `' F " x ) i^i k ) e. ( J |`t k ) ) ) )
11 10 ralbidv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( A. x e. K ( `' F " x ) e. ( kGen ` J ) <-> A. x e. K A. k e. ~P X ( ( J |`t k ) e. Comp -> ( ( `' F " x ) i^i k ) e. ( J |`t k ) ) ) )
12 ralcom 
 |-  ( A. x e. K A. k e. ~P X ( ( J |`t k ) e. Comp -> ( ( `' F " x ) i^i k ) e. ( J |`t k ) ) <-> A. k e. ~P X A. x e. K ( ( J |`t k ) e. Comp -> ( ( `' F " x ) i^i k ) e. ( J |`t k ) ) )
13 simpr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> F : X --> Y )
14 elpwi 
 |-  ( k e. ~P X -> k C_ X )
15 fssres 
 |-  ( ( F : X --> Y /\ k C_ X ) -> ( F |` k ) : k --> Y )
16 13 14 15 syl2an 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> ( F |` k ) : k --> Y )
17 simpll 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> J e. ( TopOn ` X ) )
18 resttopon 
 |-  ( ( J e. ( TopOn ` X ) /\ k C_ X ) -> ( J |`t k ) e. ( TopOn ` k ) )
19 17 14 18 syl2an 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> ( J |`t k ) e. ( TopOn ` k ) )
20 simpllr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> K e. ( TopOn ` Y ) )
21 iscn 
 |-  ( ( ( J |`t k ) e. ( TopOn ` k ) /\ K e. ( TopOn ` Y ) ) -> ( ( F |` k ) e. ( ( J |`t k ) Cn K ) <-> ( ( F |` k ) : k --> Y /\ A. x e. K ( `' ( F |` k ) " x ) e. ( J |`t k ) ) ) )
22 19 20 21 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> ( ( F |` k ) e. ( ( J |`t k ) Cn K ) <-> ( ( F |` k ) : k --> Y /\ A. x e. K ( `' ( F |` k ) " x ) e. ( J |`t k ) ) ) )
23 16 22 mpbirand 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> ( ( F |` k ) e. ( ( J |`t k ) Cn K ) <-> A. x e. K ( `' ( F |` k ) " x ) e. ( J |`t k ) ) )
24 cnvresima 
 |-  ( `' ( F |` k ) " x ) = ( ( `' F " x ) i^i k )
25 24 eleq1i 
 |-  ( ( `' ( F |` k ) " x ) e. ( J |`t k ) <-> ( ( `' F " x ) i^i k ) e. ( J |`t k ) )
26 25 ralbii 
 |-  ( A. x e. K ( `' ( F |` k ) " x ) e. ( J |`t k ) <-> A. x e. K ( ( `' F " x ) i^i k ) e. ( J |`t k ) )
27 23 26 bitrdi 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> ( ( F |` k ) e. ( ( J |`t k ) Cn K ) <-> A. x e. K ( ( `' F " x ) i^i k ) e. ( J |`t k ) ) )
28 27 imbi2d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> ( ( ( J |`t k ) e. Comp -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) <-> ( ( J |`t k ) e. Comp -> A. x e. K ( ( `' F " x ) i^i k ) e. ( J |`t k ) ) ) )
29 r19.21v 
 |-  ( A. x e. K ( ( J |`t k ) e. Comp -> ( ( `' F " x ) i^i k ) e. ( J |`t k ) ) <-> ( ( J |`t k ) e. Comp -> A. x e. K ( ( `' F " x ) i^i k ) e. ( J |`t k ) ) )
30 28 29 bitr4di 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ k e. ~P X ) -> ( ( ( J |`t k ) e. Comp -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) <-> A. x e. K ( ( J |`t k ) e. Comp -> ( ( `' F " x ) i^i k ) e. ( J |`t k ) ) ) )
31 30 ralbidva 
 |-  ( ( ( 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. k e. ~P X A. x e. K ( ( J |`t k ) e. Comp -> ( ( `' F " x ) i^i k ) e. ( J |`t k ) ) ) )
32 12 31 bitr4id 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( A. x e. K A. k e. ~P X ( ( J |`t k ) e. Comp -> ( ( `' F " x ) i^i k ) e. ( J |`t k ) ) <-> A. k e. ~P X ( ( J |`t k ) e. Comp -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) ) )
33 11 32 bitrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( A. x e. K ( `' F " x ) e. ( kGen ` J ) <-> A. k e. ~P X ( ( J |`t k ) e. Comp -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) ) )
34 33 pm5.32da 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( F : X --> Y /\ A. x e. K ( `' F " x ) e. ( kGen ` J ) ) <-> ( F : X --> Y /\ A. k e. ~P X ( ( J |`t k ) e. Comp -> ( F |` k ) e. ( ( J |`t k ) Cn K ) ) ) ) )
35 3 34 bitrd 
 |-  ( ( 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 ) ) ) ) )