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

Metamath Proof Explorer

Theorem cnmptk1

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

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

Proof

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