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

Metamath Proof Explorer

Theorem cnmptkp

Description: The evaluation of the inner function in 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 ‘ 𝑍 ) )
cnmptkp.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) )
cnmptkp.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
cnmptkp.c ⊢ ( 𝑦 = 𝐵 → 𝐴 = 𝐶 )
Assertion cnmptkp ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ∈ ( 𝐽 Cn 𝐿 ) )

Proof

Step Hyp Ref Expression
1 cnmptk1.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 cnmptk1.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3 cnmptk1.l ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
4 cnmptkp.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) )
5 cnmptkp.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
6 cnmptkp.c ⊢ ( 𝑦 = 𝐵 → 𝐴 = 𝐶 )
7 eqid ⊢ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) = ( 𝑦 ∈ 𝑌 ↦ 𝐴 )
8 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑌 )
9 6 eleq1d ⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∈ ∪ 𝐿 ↔ 𝐶 ∈ ∪ 𝐿 ) )
10 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
11 topontop ⊢ ( 𝐿 ∈ ( TopOn ‘ 𝑍 ) → 𝐿 ∈ Top )
12 3 11 syl ⊢ ( 𝜑 → 𝐿 ∈ Top )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐿 ∈ Top )
14 toptopon2 ⊢ ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
15 13 14 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
16 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
17 2 16 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
18 eqid ⊢ ( 𝐿 ↑ko 𝐾 ) = ( 𝐿 ↑ko 𝐾 )
19 18 xkotopon ⊢ ( ( 𝐾 ∈ Top ∧ 𝐿 ∈ Top ) → ( 𝐿 ↑ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) )
20 17 12 19 syl2anc ⊢ ( 𝜑 → ( 𝐿 ↑ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) )
21 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐿 ↑ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn ( 𝐿 ↑ko 𝐾 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) : 𝑋 ⟶ ( 𝐾 Cn 𝐿 ) )
22 1 20 4 21 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) : 𝑋 ⟶ ( 𝐾 Cn 𝐿 ) )
23 22 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐿 ) )
24 cnf2 ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) ∧ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐿 ) ) → ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) : 𝑌 ⟶ ∪ 𝐿 )
25 10 15 23 24 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) : 𝑌 ⟶ ∪ 𝐿 )
26 7 fmpt ⊢ ( ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿 ↔ ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) : 𝑌 ⟶ ∪ 𝐿 )
27 25 26 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿 )
28 9 27 8 rspcdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ∪ 𝐿 )
29 7 6 8 28 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝐵 ) = 𝐶 )
30 29 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
31 toponuni ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐾 )
32 2 31 syl ⊢ ( 𝜑 → 𝑌 = ∪ 𝐾 )
33 5 32 eleqtrd ⊢ ( 𝜑 → 𝐵 ∈ ∪ 𝐾 )
34 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
35 34 xkopjcn ⊢ ( ( 𝐾 ∈ Top ∧ 𝐿 ∈ Top ∧ 𝐵 ∈ ∪ 𝐾 ) → ( 𝑤 ∈ ( 𝐾 Cn 𝐿 ) ↦ ( 𝑤 ‘ 𝐵 ) ) ∈ ( ( 𝐿 ↑ko 𝐾 ) Cn 𝐿 ) )
36 17 12 33 35 syl3anc ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐾 Cn 𝐿 ) ↦ ( 𝑤 ‘ 𝐵 ) ) ∈ ( ( 𝐿 ↑ko 𝐾 ) Cn 𝐿 ) )
37 fveq1 ⊢ ( 𝑤 = ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) → ( 𝑤 ‘ 𝐵 ) = ( ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝐵 ) )
38 1 4 20 36 37 cnmpt11 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝐵 ) ) ∈ ( 𝐽 Cn 𝐿 ) )
39 30 38 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ∈ ( 𝐽 Cn 𝐿 ) )