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 syl6bb ⊢ ( ( ( ( 𝐽 ∈ ( 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 syl6bbr ⊢ ( ( ( ( 𝐽 ∈ ( 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 𝐾 ) ) ) ) )