This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem kgencn2

Description: A function F : J --> K from a compactly generated space is continuous iff for all compact spaces z and continuous g : z --> J , the composite F o. g : z --> K is continuous. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion kgencn2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( ( 𝑘Gen ‘ 𝐽 ) Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑧 ∈ Comp ∀ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) ) ) )

Proof

Step Hyp Ref Expression
1 kgencn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( ( 𝑘Gen ‘ 𝐽 ) Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐹 ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) ) ) )
2 rncmp ⊢ ( ( 𝑧 ∈ Comp ∧ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ) → ( 𝐽 ↾t ran 𝑔 ) ∈ Comp )
3 2 adantl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ Comp ∧ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ) ) → ( 𝐽 ↾t ran 𝑔 ) ∈ Comp )
4 simprr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ Comp ∧ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ) ) → 𝑔 ∈ ( 𝑧 Cn 𝐽 ) )
5 eqid ⊢ ∪ 𝑧 = ∪ 𝑧
6 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
7 5 6 cnf ⊢ ( 𝑔 ∈ ( 𝑧 Cn 𝐽 ) → 𝑔 : ∪ 𝑧 ⟶ ∪ 𝐽 )
8 frn ⊢ ( 𝑔 : ∪ 𝑧 ⟶ ∪ 𝐽 → ran 𝑔 ⊆ ∪ 𝐽 )
9 4 7 8 3syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ Comp ∧ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ) ) → ran 𝑔 ⊆ ∪ 𝐽 )
10 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
11 10 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ Comp ∧ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ) ) → 𝑋 = ∪ 𝐽 )
12 9 11 sseqtrrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ Comp ∧ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ) ) → ran 𝑔 ⊆ 𝑋 )
13 vex ⊢ 𝑔 ∈ V
14 13 rnex ⊢ ran 𝑔 ∈ V
15 14 elpw ⊢ ( ran 𝑔 ∈ 𝒫 𝑋 ↔ ran 𝑔 ⊆ 𝑋 )
16 12 15 sylibr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ Comp ∧ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ) ) → ran 𝑔 ∈ 𝒫 𝑋 )
17 oveq2 ⊢ ( 𝑘 = ran 𝑔 → ( 𝐽 ↾t 𝑘 ) = ( 𝐽 ↾t ran 𝑔 ) )
18 17 eleq1d ⊢ ( 𝑘 = ran 𝑔 → ( ( 𝐽 ↾t 𝑘 ) ∈ Comp ↔ ( 𝐽 ↾t ran 𝑔 ) ∈ Comp ) )
19 reseq2 ⊢ ( 𝑘 = ran 𝑔 → ( 𝐹 ↾ 𝑘 ) = ( 𝐹 ↾ ran 𝑔 ) )
20 17 oveq1d ⊢ ( 𝑘 = ran 𝑔 → ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) = ( ( 𝐽 ↾t ran 𝑔 ) Cn 𝐾 ) )
21 19 20 eleq12d ⊢ ( 𝑘 = ran 𝑔 → ( ( 𝐹 ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ↔ ( 𝐹 ↾ ran 𝑔 ) ∈ ( ( 𝐽 ↾t ran 𝑔 ) Cn 𝐾 ) ) )
22 18 21 imbi12d ⊢ ( 𝑘 = ran 𝑔 → ( ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐹 ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) ↔ ( ( 𝐽 ↾t ran 𝑔 ) ∈ Comp → ( 𝐹 ↾ ran 𝑔 ) ∈ ( ( 𝐽 ↾t ran 𝑔 ) Cn 𝐾 ) ) ) )
23 22 rspcv ⊢ ( ran 𝑔 ∈ 𝒫 𝑋 → ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐹 ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) → ( ( 𝐽 ↾t ran 𝑔 ) ∈ Comp → ( 𝐹 ↾ ran 𝑔 ) ∈ ( ( 𝐽 ↾t ran 𝑔 ) Cn 𝐾 ) ) ) )
24 16 23 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ Comp ∧ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ) ) → ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐹 ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) → ( ( 𝐽 ↾t ran 𝑔 ) ∈ Comp → ( 𝐹 ↾ ran 𝑔 ) ∈ ( ( 𝐽 ↾t ran 𝑔 ) Cn 𝐾 ) ) ) )
25 3 24 mpid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ Comp ∧ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ) ) → ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐹 ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) → ( 𝐹 ↾ ran 𝑔 ) ∈ ( ( 𝐽 ↾t ran 𝑔 ) Cn 𝐾 ) ) )
26 simplll ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ Comp ∧ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
27 ssidd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ Comp ∧ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ) ) → ran 𝑔 ⊆ ran 𝑔 )
28 cnrest2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ran 𝑔 ⊆ ran 𝑔 ∧ ran 𝑔 ⊆ 𝑋 ) → ( 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ↔ 𝑔 ∈ ( 𝑧 Cn ( 𝐽 ↾t ran 𝑔 ) ) ) )
29 26 27 12 28 syl3anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ Comp ∧ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ) ) → ( 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ↔ 𝑔 ∈ ( 𝑧 Cn ( 𝐽 ↾t ran 𝑔 ) ) ) )
30 4 29 mpbid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ Comp ∧ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ) ) → 𝑔 ∈ ( 𝑧 Cn ( 𝐽 ↾t ran 𝑔 ) ) )
31 cnco ⊢ ( ( 𝑔 ∈ ( 𝑧 Cn ( 𝐽 ↾t ran 𝑔 ) ) ∧ ( 𝐹 ↾ ran 𝑔 ) ∈ ( ( 𝐽 ↾t ran 𝑔 ) Cn 𝐾 ) ) → ( ( 𝐹 ↾ ran 𝑔 ) ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) )
32 31 ex ⊢ ( 𝑔 ∈ ( 𝑧 Cn ( 𝐽 ↾t ran 𝑔 ) ) → ( ( 𝐹 ↾ ran 𝑔 ) ∈ ( ( 𝐽 ↾t ran 𝑔 ) Cn 𝐾 ) → ( ( 𝐹 ↾ ran 𝑔 ) ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) ) )
33 30 32 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ Comp ∧ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ) ) → ( ( 𝐹 ↾ ran 𝑔 ) ∈ ( ( 𝐽 ↾t ran 𝑔 ) Cn 𝐾 ) → ( ( 𝐹 ↾ ran 𝑔 ) ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) ) )
34 ssid ⊢ ran 𝑔 ⊆ ran 𝑔
35 cores ⊢ ( ran 𝑔 ⊆ ran 𝑔 → ( ( 𝐹 ↾ ran 𝑔 ) ∘ 𝑔 ) = ( 𝐹 ∘ 𝑔 ) )
36 34 35 ax-mp ⊢ ( ( 𝐹 ↾ ran 𝑔 ) ∘ 𝑔 ) = ( 𝐹 ∘ 𝑔 )
37 36 eleq1i ⊢ ( ( ( 𝐹 ↾ ran 𝑔 ) ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) ↔ ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) )
38 33 37 imbitrdi ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ Comp ∧ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ) ) → ( ( 𝐹 ↾ ran 𝑔 ) ∈ ( ( 𝐽 ↾t ran 𝑔 ) Cn 𝐾 ) → ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) ) )
39 25 38 syld ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ Comp ∧ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ) ) → ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐹 ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) → ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) ) )
40 39 ralrimdvva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐹 ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) → ∀ 𝑧 ∈ Comp ∀ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) ) )
41 oveq1 ⊢ ( 𝑧 = ( 𝐽 ↾t 𝑘 ) → ( 𝑧 Cn 𝐽 ) = ( ( 𝐽 ↾t 𝑘 ) Cn 𝐽 ) )
42 oveq1 ⊢ ( 𝑧 = ( 𝐽 ↾t 𝑘 ) → ( 𝑧 Cn 𝐾 ) = ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) )
43 42 eleq2d ⊢ ( 𝑧 = ( 𝐽 ↾t 𝑘 ) → ( ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) ↔ ( 𝐹 ∘ 𝑔 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) )
44 41 43 raleqbidv ⊢ ( 𝑧 = ( 𝐽 ↾t 𝑘 ) → ( ∀ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) ↔ ∀ 𝑔 ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐽 ) ( 𝐹 ∘ 𝑔 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) )
45 44 rspcv ⊢ ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( ∀ 𝑧 ∈ Comp ∀ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) → ∀ 𝑔 ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐽 ) ( 𝐹 ∘ 𝑔 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) )
46 elpwi ⊢ ( 𝑘 ∈ 𝒫 𝑋 → 𝑘 ⊆ 𝑋 )
47 46 adantl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → 𝑘 ⊆ 𝑋 )
48 47 resabs1d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ( I ↾ 𝑋 ) ↾ 𝑘 ) = ( I ↾ 𝑘 ) )
49 idcn ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐽 ) )
50 49 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐽 ) )
51 10 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → 𝑋 = ∪ 𝐽 )
52 47 51 sseqtrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → 𝑘 ⊆ ∪ 𝐽 )
53 6 cnrest ⊢ ( ( ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐽 ) ∧ 𝑘 ⊆ ∪ 𝐽 ) → ( ( I ↾ 𝑋 ) ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐽 ) )
54 50 52 53 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ( I ↾ 𝑋 ) ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐽 ) )
55 48 54 eqeltrrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( I ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐽 ) )
56 coeq2 ⊢ ( 𝑔 = ( I ↾ 𝑘 ) → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ ( I ↾ 𝑘 ) ) )
57 56 eleq1d ⊢ ( 𝑔 = ( I ↾ 𝑘 ) → ( ( 𝐹 ∘ 𝑔 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ↔ ( 𝐹 ∘ ( I ↾ 𝑘 ) ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) )
58 57 rspcv ⊢ ( ( I ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐽 ) → ( ∀ 𝑔 ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐽 ) ( 𝐹 ∘ 𝑔 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) → ( 𝐹 ∘ ( I ↾ 𝑘 ) ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) )
59 55 58 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ∀ 𝑔 ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐽 ) ( 𝐹 ∘ 𝑔 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) → ( 𝐹 ∘ ( I ↾ 𝑘 ) ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) )
60 coires1 ⊢ ( 𝐹 ∘ ( I ↾ 𝑘 ) ) = ( 𝐹 ↾ 𝑘 )
61 60 eleq1i ⊢ ( ( 𝐹 ∘ ( I ↾ 𝑘 ) ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ↔ ( 𝐹 ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) )
62 59 61 imbitrdi ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ∀ 𝑔 ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐽 ) ( 𝐹 ∘ 𝑔 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) → ( 𝐹 ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) )
63 45 62 syl9r ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( ∀ 𝑧 ∈ Comp ∀ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) → ( 𝐹 ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) ) )
64 63 com23 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑘 ∈ 𝒫 𝑋 ) → ( ∀ 𝑧 ∈ Comp ∀ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) → ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐹 ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) ) )
65 64 ralrimdva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑧 ∈ Comp ∀ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) → ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐹 ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) ) )
66 40 65 impbid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐹 ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) ↔ ∀ 𝑧 ∈ Comp ∀ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) ) )
67 66 pm5.32da ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑘 ∈ 𝒫 𝑋 ( ( 𝐽 ↾t 𝑘 ) ∈ Comp → ( 𝐹 ↾ 𝑘 ) ∈ ( ( 𝐽 ↾t 𝑘 ) Cn 𝐾 ) ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑧 ∈ Comp ∀ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) ) ) )
68 1 67 bitrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( ( 𝑘Gen ‘ 𝐽 ) Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑧 ∈ Comp ∀ 𝑔 ∈ ( 𝑧 Cn 𝐽 ) ( 𝐹 ∘ 𝑔 ) ∈ ( 𝑧 Cn 𝐾 ) ) ) )