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 𝐾 ) ) ) ) )