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 TopOn X K TopOn Y F 𝑘Gen J Cn K F : X Y k 𝒫 X J 𝑡 k Comp F k J 𝑡 k Cn K

Proof

Step Hyp Ref Expression
1 kgentopon J TopOn X 𝑘Gen J TopOn X
2 iscn 𝑘Gen J TopOn X K TopOn Y F 𝑘Gen J Cn K F : X Y x K F -1 x 𝑘Gen J
3 1 2 sylan J TopOn X K TopOn Y F 𝑘Gen J Cn K F : X Y x K F -1 x 𝑘Gen J
4 cnvimass F -1 x dom F
5 fdm F : X Y dom F = X
6 5 adantl J TopOn X K TopOn Y F : X Y dom F = X
7 4 6 sseqtrid J TopOn X K TopOn Y F : X Y F -1 x X
8 elkgen J TopOn X F -1 x 𝑘Gen J F -1 x X k 𝒫 X J 𝑡 k Comp F -1 x k J 𝑡 k
9 8 ad2antrr J TopOn X K TopOn Y F : X Y F -1 x 𝑘Gen J F -1 x X k 𝒫 X J 𝑡 k Comp F -1 x k J 𝑡 k
10 7 9 mpbirand J TopOn X K TopOn Y F : X Y F -1 x 𝑘Gen J k 𝒫 X J 𝑡 k Comp F -1 x k J 𝑡 k
11 10 ralbidv J TopOn X K TopOn Y F : X Y x K F -1 x 𝑘Gen J x K k 𝒫 X J 𝑡 k Comp F -1 x k J 𝑡 k
12 ralcom x K k 𝒫 X J 𝑡 k Comp F -1 x k J 𝑡 k k 𝒫 X x K J 𝑡 k Comp F -1 x k J 𝑡 k
13 simpr J TopOn X K TopOn Y F : X Y F : X Y
14 elpwi k 𝒫 X k X
15 fssres F : X Y k X F k : k Y
16 13 14 15 syl2an J TopOn X K TopOn Y F : X Y k 𝒫 X F k : k Y
17 simpll J TopOn X K TopOn Y F : X Y J TopOn X
18 resttopon J TopOn X k X J 𝑡 k TopOn k
19 17 14 18 syl2an J TopOn X K TopOn Y F : X Y k 𝒫 X J 𝑡 k TopOn k
20 simpllr J TopOn X K TopOn Y F : X Y k 𝒫 X K TopOn Y
21 iscn J 𝑡 k TopOn k K TopOn Y F k J 𝑡 k Cn K F k : k Y x K F k -1 x J 𝑡 k
22 19 20 21 syl2anc J TopOn X K TopOn Y F : X Y k 𝒫 X F k J 𝑡 k Cn K F k : k Y x K F k -1 x J 𝑡 k
23 16 22 mpbirand J TopOn X K TopOn Y F : X Y k 𝒫 X F k J 𝑡 k Cn K x K F k -1 x J 𝑡 k
24 cnvresima F k -1 x = F -1 x k
25 24 eleq1i F k -1 x J 𝑡 k F -1 x k J 𝑡 k
26 25 ralbii x K F k -1 x J 𝑡 k x K F -1 x k J 𝑡 k
27 23 26 bitrdi J TopOn X K TopOn Y F : X Y k 𝒫 X F k J 𝑡 k Cn K x K F -1 x k J 𝑡 k
28 27 imbi2d J TopOn X K TopOn Y F : X Y k 𝒫 X J 𝑡 k Comp F k J 𝑡 k Cn K J 𝑡 k Comp x K F -1 x k J 𝑡 k
29 r19.21v x K J 𝑡 k Comp F -1 x k J 𝑡 k J 𝑡 k Comp x K F -1 x k J 𝑡 k
30 28 29 bitr4di J TopOn X K TopOn Y F : X Y k 𝒫 X J 𝑡 k Comp F k J 𝑡 k Cn K x K J 𝑡 k Comp F -1 x k J 𝑡 k
31 30 ralbidva J TopOn X K TopOn Y F : X Y k 𝒫 X J 𝑡 k Comp F k J 𝑡 k Cn K k 𝒫 X x K J 𝑡 k Comp F -1 x k J 𝑡 k
32 12 31 bitr4id J TopOn X K TopOn Y F : X Y x K k 𝒫 X J 𝑡 k Comp F -1 x k J 𝑡 k k 𝒫 X J 𝑡 k Comp F k J 𝑡 k Cn K
33 11 32 bitrd J TopOn X K TopOn Y F : X Y x K F -1 x 𝑘Gen J k 𝒫 X J 𝑡 k Comp F k J 𝑡 k Cn K
34 33 pm5.32da J TopOn X K TopOn Y F : X Y x K F -1 x 𝑘Gen J F : X Y k 𝒫 X J 𝑡 k Comp F k J 𝑡 k Cn K
35 3 34 bitrd J TopOn X K TopOn Y F 𝑘Gen J Cn K F : X Y k 𝒫 X J 𝑡 k Comp F k J 𝑡 k Cn K