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

Metamath Proof Explorer

Theorem cnmpt1k

Description: The composition of a one-arg function with a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses cnmptk1.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
cnmptk1.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
cnmptk1.l ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
cnmpt1k.m ⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ 𝑊 ) )
cnmpt1k.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐿 ) )
cnmpt1k.b ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ( 𝐾 Cn ( 𝑀 ↑ko 𝐿 ) ) )
cnmpt1k.c ⊢ ( 𝑧 = 𝐴 → 𝐵 = 𝐶 )
Assertion cnmpt1k ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∈ ( 𝐾 Cn ( 𝑀 ↑ko 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 cnmptk1.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 cnmptk1.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3 cnmptk1.l ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
4 cnmpt1k.m ⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ 𝑊 ) )
5 cnmpt1k.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐿 ) )
6 cnmpt1k.b ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ( 𝐾 Cn ( 𝑀 ↑ko 𝐿 ) ) )
7 cnmpt1k.c ⊢ ( 𝑧 = 𝐴 → 𝐵 = 𝐶 )
8 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑍 ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn 𝐿 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑍 )
9 1 3 5 8 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑍 )
10 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 )
11 10 fmpt ⊢ ( ∀ 𝑥 ∈ 𝑋 𝐴 ∈ 𝑍 ↔ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑍 )
12 9 11 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐴 ∈ 𝑍 )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ∀ 𝑥 ∈ 𝑋 𝐴 ∈ 𝑍 )
14 eqidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
15 eqidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) = ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) )
16 13 14 15 7 fmptcof ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
17 16 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) )
18 topontop ⊢ ( 𝐿 ∈ ( TopOn ‘ 𝑍 ) → 𝐿 ∈ Top )
19 3 18 syl ⊢ ( 𝜑 → 𝐿 ∈ Top )
20 topontop ⊢ ( 𝑀 ∈ ( TopOn ‘ 𝑊 ) → 𝑀 ∈ Top )
21 4 20 syl ⊢ ( 𝜑 → 𝑀 ∈ Top )
22 eqid ⊢ ( 𝑀 ↑ko 𝐿 ) = ( 𝑀 ↑ko 𝐿 )
23 22 xkotopon ⊢ ( ( 𝐿 ∈ Top ∧ 𝑀 ∈ Top ) → ( 𝑀 ↑ko 𝐿 ) ∈ ( TopOn ‘ ( 𝐿 Cn 𝑀 ) ) )
24 19 21 23 syl2anc ⊢ ( 𝜑 → ( 𝑀 ↑ko 𝐿 ) ∈ ( TopOn ‘ ( 𝐿 Cn 𝑀 ) ) )
25 21 5 xkoco1cn ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐿 Cn 𝑀 ) ↦ ( 𝑤 ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) ∈ ( ( 𝑀 ↑ko 𝐿 ) Cn ( 𝑀 ↑ko 𝐽 ) ) )
26 coeq1 ⊢ ( 𝑤 = ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) → ( 𝑤 ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) )
27 2 6 24 25 26 cnmpt11 ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) ∈ ( 𝐾 Cn ( 𝑀 ↑ko 𝐽 ) ) )
28 17 27 eqeltrrd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) ∈ ( 𝐾 Cn ( 𝑀 ↑ko 𝐽 ) ) )