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 simpr ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) → 𝐹 : 𝑋𝑌 )
13 elpwi ( 𝑘 ∈ 𝒫 𝑋𝑘𝑋 )
14 fssres ( ( 𝐹 : 𝑋𝑌𝑘𝑋 ) → ( 𝐹𝑘 ) : 𝑘𝑌 )
15 12 13 14 syl2an ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( 𝐹𝑘 ) : 𝑘𝑌 )
16 simpll ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
17 resttopon ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑘𝑋 ) → ( 𝐽t 𝑘 ) ∈ ( TopOn ‘ 𝑘 ) )
18 16 13 17 syl2an ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( 𝐽t 𝑘 ) ∈ ( TopOn ‘ 𝑘 ) )
19 simpllr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
20 iscn ( ( ( 𝐽t 𝑘 ) ∈ ( TopOn ‘ 𝑘 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝐹𝑘 ) ∈ ( ( 𝐽t 𝑘 ) Cn 𝐾 ) ↔ ( ( 𝐹𝑘 ) : 𝑘𝑌 ∧ ∀ 𝑥𝐾 ( ( 𝐹𝑘 ) “ 𝑥 ) ∈ ( 𝐽t 𝑘 ) ) ) )
21 18 19 20 syl2anc ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ( 𝐹𝑘 ) ∈ ( ( 𝐽t 𝑘 ) Cn 𝐾 ) ↔ ( ( 𝐹𝑘 ) : 𝑘𝑌 ∧ ∀ 𝑥𝐾 ( ( 𝐹𝑘 ) “ 𝑥 ) ∈ ( 𝐽t 𝑘 ) ) ) )
22 15 21 mpbirand ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ( 𝐹𝑘 ) ∈ ( ( 𝐽t 𝑘 ) Cn 𝐾 ) ↔ ∀ 𝑥𝐾 ( ( 𝐹𝑘 ) “ 𝑥 ) ∈ ( 𝐽t 𝑘 ) ) )
23 cnvresima ( ( 𝐹𝑘 ) “ 𝑥 ) = ( ( 𝐹𝑥 ) ∩ 𝑘 )
24 23 eleq1i ( ( ( 𝐹𝑘 ) “ 𝑥 ) ∈ ( 𝐽t 𝑘 ) ↔ ( ( 𝐹𝑥 ) ∩ 𝑘 ) ∈ ( 𝐽t 𝑘 ) )
25 24 ralbii ( ∀ 𝑥𝐾 ( ( 𝐹𝑘 ) “ 𝑥 ) ∈ ( 𝐽t 𝑘 ) ↔ ∀ 𝑥𝐾 ( ( 𝐹𝑥 ) ∩ 𝑘 ) ∈ ( 𝐽t 𝑘 ) )
26 22 25 syl6bb ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ( 𝐹𝑘 ) ∈ ( ( 𝐽t 𝑘 ) Cn 𝐾 ) ↔ ∀ 𝑥𝐾 ( ( 𝐹𝑥 ) ∩ 𝑘 ) ∈ ( 𝐽t 𝑘 ) ) )
27 26 imbi2d ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ( ( 𝐽t 𝑘 ) ∈ Comp → ( 𝐹𝑘 ) ∈ ( ( 𝐽t 𝑘 ) Cn 𝐾 ) ) ↔ ( ( 𝐽t 𝑘 ) ∈ Comp → ∀ 𝑥𝐾 ( ( 𝐹𝑥 ) ∩ 𝑘 ) ∈ ( 𝐽t 𝑘 ) ) ) )
28 r19.21v ( ∀ 𝑥𝐾 ( ( 𝐽t 𝑘 ) ∈ Comp → ( ( 𝐹𝑥 ) ∩ 𝑘 ) ∈ ( 𝐽t 𝑘 ) ) ↔ ( ( 𝐽t 𝑘 ) ∈ Comp → ∀ 𝑥𝐾 ( ( 𝐹𝑥 ) ∩ 𝑘 ) ∈ ( 𝐽t 𝑘 ) ) )
29 27 28 syl6bbr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ( ( 𝐽t 𝑘 ) ∈ Comp → ( 𝐹𝑘 ) ∈ ( ( 𝐽t 𝑘 ) Cn 𝐾 ) ) ↔ ∀ 𝑥𝐾 ( ( 𝐽t 𝑘 ) ∈ Comp → ( ( 𝐹𝑥 ) ∩ 𝑘 ) ∈ ( 𝐽t 𝑘 ) ) ) )
30 29 ralbidva ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) → ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽t 𝑘 ) ∈ Comp → ( 𝐹𝑘 ) ∈ ( ( 𝐽t 𝑘 ) Cn 𝐾 ) ) ↔ ∀ 𝑘 ∈ 𝒫 𝑋𝑥𝐾 ( ( 𝐽t 𝑘 ) ∈ Comp → ( ( 𝐹𝑥 ) ∩ 𝑘 ) ∈ ( 𝐽t 𝑘 ) ) ) )
31 ralcom ( ∀ 𝑥𝐾𝑘 ∈ 𝒫 𝑋 ( ( 𝐽t 𝑘 ) ∈ Comp → ( ( 𝐹𝑥 ) ∩ 𝑘 ) ∈ ( 𝐽t 𝑘 ) ) ↔ ∀ 𝑘 ∈ 𝒫 𝑋𝑥𝐾 ( ( 𝐽t 𝑘 ) ∈ Comp → ( ( 𝐹𝑥 ) ∩ 𝑘 ) ∈ ( 𝐽t 𝑘 ) ) )
32 30 31 syl6rbbr ( ( ( 𝐽 ∈ ( 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 𝐾 ) ) ) ) )