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 ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) β†’ ( 𝐹 ∈ ( ( π‘˜Gen β€˜ 𝐽 ) Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( 𝐹 β†Ύ π‘˜ ) ∈ ( ( 𝐽 β†Ύt π‘˜ ) Cn 𝐾 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 kgentopon ⊒ ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) β†’ ( π‘˜Gen β€˜ 𝐽 ) ∈ ( TopOn β€˜ 𝑋 ) )
2 iscn ⊒ ( ( ( π‘˜Gen β€˜ 𝐽 ) ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) β†’ ( 𝐹 ∈ ( ( π‘˜Gen β€˜ 𝐽 ) Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝐾 ( β—‘ 𝐹 β€œ π‘₯ ) ∈ ( π‘˜Gen β€˜ 𝐽 ) ) ) )
3 1 2 sylan ⊒ ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) β†’ ( 𝐹 ∈ ( ( π‘˜Gen β€˜ 𝐽 ) Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝐾 ( β—‘ 𝐹 β€œ π‘₯ ) ∈ ( π‘˜Gen β€˜ 𝐽 ) ) ) )
4 cnvimass ⊒ ( β—‘ 𝐹 β€œ π‘₯ ) βŠ† dom 𝐹
5 fdm ⊒ ( 𝐹 : 𝑋 ⟢ π‘Œ β†’ dom 𝐹 = 𝑋 )
6 5 adantl ⊒ ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ dom 𝐹 = 𝑋 )
7 4 6 sseqtrid ⊒ ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( β—‘ 𝐹 β€œ π‘₯ ) βŠ† 𝑋 )
8 elkgen ⊒ ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) β†’ ( ( β—‘ 𝐹 β€œ π‘₯ ) ∈ ( π‘˜Gen β€˜ 𝐽 ) ↔ ( ( β—‘ 𝐹 β€œ π‘₯ ) βŠ† 𝑋 ∧ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( ( β—‘ 𝐹 β€œ π‘₯ ) ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) ) )
9 8 ad2antrr ⊒ ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( ( β—‘ 𝐹 β€œ π‘₯ ) ∈ ( π‘˜Gen β€˜ 𝐽 ) ↔ ( ( β—‘ 𝐹 β€œ π‘₯ ) βŠ† 𝑋 ∧ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( ( β—‘ 𝐹 β€œ π‘₯ ) ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) ) )
10 7 9 mpbirand ⊒ ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( ( β—‘ 𝐹 β€œ π‘₯ ) ∈ ( π‘˜Gen β€˜ 𝐽 ) ↔ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( ( β—‘ 𝐹 β€œ π‘₯ ) ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) )
11 10 ralbidv ⊒ ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( βˆ€ π‘₯ ∈ 𝐾 ( β—‘ 𝐹 β€œ π‘₯ ) ∈ ( π‘˜Gen β€˜ 𝐽 ) ↔ βˆ€ π‘₯ ∈ 𝐾 βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( ( β—‘ 𝐹 β€œ π‘₯ ) ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) )
12 ralcom ⊒ ( βˆ€ π‘₯ ∈ 𝐾 βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( ( β—‘ 𝐹 β€œ π‘₯ ) ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ↔ βˆ€ π‘˜ ∈ 𝒫 𝑋 βˆ€ π‘₯ ∈ 𝐾 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( ( β—‘ 𝐹 β€œ π‘₯ ) ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) )
13 simpr ⊒ ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ 𝐹 : 𝑋 ⟢ π‘Œ )
14 elpwi ⊒ ( π‘˜ ∈ 𝒫 𝑋 β†’ π‘˜ βŠ† 𝑋 )
15 fssres ⊒ ( ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ π‘˜ βŠ† 𝑋 ) β†’ ( 𝐹 β†Ύ π‘˜ ) : π‘˜ ⟢ π‘Œ )
16 13 14 15 syl2an ⊒ ( ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ π‘˜ ∈ 𝒫 𝑋 ) β†’ ( 𝐹 β†Ύ π‘˜ ) : π‘˜ ⟢ π‘Œ )
17 simpll ⊒ ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ 𝐽 ∈ ( TopOn β€˜ 𝑋 ) )
18 resttopon ⊒ ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ π‘˜ βŠ† 𝑋 ) β†’ ( 𝐽 β†Ύt π‘˜ ) ∈ ( TopOn β€˜ π‘˜ ) )
19 17 14 18 syl2an ⊒ ( ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ π‘˜ ∈ 𝒫 𝑋 ) β†’ ( 𝐽 β†Ύt π‘˜ ) ∈ ( TopOn β€˜ π‘˜ ) )
20 simpllr ⊒ ( ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ π‘˜ ∈ 𝒫 𝑋 ) β†’ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) )
21 iscn ⊒ ( ( ( 𝐽 β†Ύt π‘˜ ) ∈ ( TopOn β€˜ π‘˜ ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) β†’ ( ( 𝐹 β†Ύ π‘˜ ) ∈ ( ( 𝐽 β†Ύt π‘˜ ) Cn 𝐾 ) ↔ ( ( 𝐹 β†Ύ π‘˜ ) : π‘˜ ⟢ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝐾 ( β—‘ ( 𝐹 β†Ύ π‘˜ ) β€œ π‘₯ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) )
22 19 20 21 syl2anc ⊒ ( ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ π‘˜ ∈ 𝒫 𝑋 ) β†’ ( ( 𝐹 β†Ύ π‘˜ ) ∈ ( ( 𝐽 β†Ύt π‘˜ ) Cn 𝐾 ) ↔ ( ( 𝐹 β†Ύ π‘˜ ) : π‘˜ ⟢ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝐾 ( β—‘ ( 𝐹 β†Ύ π‘˜ ) β€œ π‘₯ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) )
23 16 22 mpbirand ⊒ ( ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ π‘˜ ∈ 𝒫 𝑋 ) β†’ ( ( 𝐹 β†Ύ π‘˜ ) ∈ ( ( 𝐽 β†Ύt π‘˜ ) Cn 𝐾 ) ↔ βˆ€ π‘₯ ∈ 𝐾 ( β—‘ ( 𝐹 β†Ύ π‘˜ ) β€œ π‘₯ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) )
24 cnvresima ⊒ ( β—‘ ( 𝐹 β†Ύ π‘˜ ) β€œ π‘₯ ) = ( ( β—‘ 𝐹 β€œ π‘₯ ) ∩ π‘˜ )
25 24 eleq1i ⊒ ( ( β—‘ ( 𝐹 β†Ύ π‘˜ ) β€œ π‘₯ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ↔ ( ( β—‘ 𝐹 β€œ π‘₯ ) ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) )
26 25 ralbii ⊒ ( βˆ€ π‘₯ ∈ 𝐾 ( β—‘ ( 𝐹 β†Ύ π‘˜ ) β€œ π‘₯ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ↔ βˆ€ π‘₯ ∈ 𝐾 ( ( β—‘ 𝐹 β€œ π‘₯ ) ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) )
27 23 26 bitrdi ⊒ ( ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ π‘˜ ∈ 𝒫 𝑋 ) β†’ ( ( 𝐹 β†Ύ π‘˜ ) ∈ ( ( 𝐽 β†Ύt π‘˜ ) Cn 𝐾 ) ↔ βˆ€ π‘₯ ∈ 𝐾 ( ( β—‘ 𝐹 β€œ π‘₯ ) ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) )
28 27 imbi2d ⊒ ( ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ π‘˜ ∈ 𝒫 𝑋 ) β†’ ( ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( 𝐹 β†Ύ π‘˜ ) ∈ ( ( 𝐽 β†Ύt π‘˜ ) Cn 𝐾 ) ) ↔ ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ βˆ€ π‘₯ ∈ 𝐾 ( ( β—‘ 𝐹 β€œ π‘₯ ) ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) )
29 r19.21v ⊒ ( βˆ€ π‘₯ ∈ 𝐾 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( ( β—‘ 𝐹 β€œ π‘₯ ) ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ↔ ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ βˆ€ π‘₯ ∈ 𝐾 ( ( β—‘ 𝐹 β€œ π‘₯ ) ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) )
30 28 29 bitr4di ⊒ ( ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ π‘˜ ∈ 𝒫 𝑋 ) β†’ ( ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( 𝐹 β†Ύ π‘˜ ) ∈ ( ( 𝐽 β†Ύt π‘˜ ) Cn 𝐾 ) ) ↔ βˆ€ π‘₯ ∈ 𝐾 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( ( β—‘ 𝐹 β€œ π‘₯ ) ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) )
31 30 ralbidva ⊒ ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( 𝐹 β†Ύ π‘˜ ) ∈ ( ( 𝐽 β†Ύt π‘˜ ) Cn 𝐾 ) ) ↔ βˆ€ π‘˜ ∈ 𝒫 𝑋 βˆ€ π‘₯ ∈ 𝐾 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( ( β—‘ 𝐹 β€œ π‘₯ ) ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) )
32 12 31 bitr4id ⊒ ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( βˆ€ π‘₯ ∈ 𝐾 βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( ( β—‘ 𝐹 β€œ π‘₯ ) ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ↔ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( 𝐹 β†Ύ π‘˜ ) ∈ ( ( 𝐽 β†Ύt π‘˜ ) Cn 𝐾 ) ) ) )
33 11 32 bitrd ⊒ ( ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( βˆ€ π‘₯ ∈ 𝐾 ( β—‘ 𝐹 β€œ π‘₯ ) ∈ ( π‘˜Gen β€˜ 𝐽 ) ↔ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( 𝐹 β†Ύ π‘˜ ) ∈ ( ( 𝐽 β†Ύt π‘˜ ) Cn 𝐾 ) ) ) )
34 33 pm5.32da ⊒ ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) β†’ ( ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝐾 ( β—‘ 𝐹 β€œ π‘₯ ) ∈ ( π‘˜Gen β€˜ 𝐽 ) ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( 𝐹 β†Ύ π‘˜ ) ∈ ( ( 𝐽 β†Ύt π‘˜ ) Cn 𝐾 ) ) ) ) )
35 3 34 bitrd ⊒ ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) β†’ ( 𝐹 ∈ ( ( π‘˜Gen β€˜ 𝐽 ) Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( 𝐹 β†Ύ π‘˜ ) ∈ ( ( 𝐽 β†Ύt π‘˜ ) Cn 𝐾 ) ) ) ) )