Theorem cnmptk1 23741

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

Hypotheses

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

Assertion

Ref	Expression
cnmptk1	⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐶)) ∈ (𝐽 Cn (𝑀 ↑ko 𝐾)))

Distinct variable groups:   𝑥,𝑦,𝐽   𝑥,𝐾,𝑦   𝑥,𝐿,𝑦   𝑥,𝑀,𝑦   𝑥,𝑧,𝑍,𝑦   𝑧,𝐴   𝑥,𝐵   𝜑,𝑥,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦   𝑧,𝐶   𝑦,𝐵

Allowed substitution hints:   𝜑(𝑧)   𝐴(𝑥,𝑦)   𝐵(𝑧)   𝐶(𝑥,𝑦)   𝐽(𝑧)   𝐾(𝑧)   𝐿(𝑧)   𝑀(𝑧)   𝑋(𝑧)   𝑌(𝑧)

Proof of Theorem cnmptk1

Dummy variable 𝑤 is distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∈ wcel 2142  ∀wral 3076   ↦ cmpt 5181   ∘ ccom 5651  ⟶wf 6517  ‘cfv 6521  (class class class)co 7396  Topctop 22953  TopOnctopon 22970   Cn ccn 23284   ↑_ko cxko 23621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4906  df-iun 4951  df-iin 4952  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-1st 7970  df-2nd 7971  df-1o 8437  df-2o 8438  df-map 8810  df-en 8928  df-dom 8929  df-fin 8931  df-fi 9357  df-rest 17451  df-topgen 17472  df-top 22954  df-topon 22971  df-bases 23006  df-cn 23287  df-cmp 23447  df-xko 23623

This theorem is referenced by:  cnmpt2k  23748