Theorem cnmptc 23579

Description: A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)

Hypotheses

Ref	Expression
cnmptid.j	⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
cnmptc.k	⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
cnmptc.p	⊢ (𝜑 → 𝑃 ∈ 𝑌)

Assertion

Ref	Expression
cnmptc	⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑃) ∈ (𝐽 Cn 𝐾))

Distinct variable groups:   𝜑,𝑥   𝑥,𝐽   𝑥,𝑋   𝑥,𝑌   𝑥,𝐾   𝑥,𝑃

Proof of Theorem cnmptc

Step	Hyp	Ref	Expression
1		fconstmpt 5740	. 2 ⊢ (𝑋 × {𝑃}) = (𝑥 ∈ 𝑋 ↦ 𝑃)
2		cnmptid.j	. . 3 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
3		cnmptc.k	. . 3 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
4		cnmptc.p	. . 3 ⊢ (𝜑 → 𝑃 ∈ 𝑌)
5		cnconst2 23200	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑌) → (𝑋 × {𝑃}) ∈ (𝐽 Cn 𝐾))
6	2, 3, 4, 5	syl3anc 1369	. 2 ⊢ (𝜑 → (𝑋 × {𝑃}) ∈ (𝐽 Cn 𝐾))
7	1, 6	eqeltrrid 2834	1 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑃) ∈ (𝐽 Cn 𝐾))

Syntax hints:   → wi 4   ∈ wcel 2099  {csn 4629   ↦ cmpt 5231   × cxp 5676  ‘cfv 6548  (class class class)co 7420  TopOnctopon 22825   Cn ccn 23141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-fv 6556  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 7993  df-2nd 7994  df-map 8847  df-topgen 17425  df-top 22809  df-topon 22826  df-cn 23144  df-cnp 23145

This theorem is referenced by:  cnmpt2c  23587  xkoinjcn  23604  txconn  23606  imasnopn  23607  imasncld  23608  imasncls  23609  istgp2  24008  tmdmulg  24009  tmdgsum  24012  tmdlactcn  24019  clsnsg  24027  tgpt0  24036  tlmtgp  24113  nmcn  24773  fsumcn  24801  expcn  24803  divccn  24804  expcnOLD  24805  divccnOLD  24806  cncfmptc  24845  cdivcncf  24854  iirevcn  24864  iihalf1cn  24866  iihalf1cnOLD  24867  iihalf2cn  24869  iihalf2cnOLD  24870  icchmeo  24878  icchmeoOLD  24879  evth  24898  evth2  24899  pcocn  24957  pcopt  24962  pcopt2  24963  pcoass  24964  csscld  25190  clsocv  25191  dvcnvlem  25921  plycn  26208  plycnOLD  26209  psercn2  26372  psercn2OLD  26373  resqrtcn  26697  sqrtcn  26698  atansopn  26877  efrlim  26914  efrlimOLD  26915  ipasslem7  30659  occllem  31126  rmulccn  33529  cxpcncf1  34227  txsconnlem  34850  cvxpconn  34852  cvmlift2lem2  34914  cvmlift2lem3  34915  cvmliftphtlem  34927  sinccvglem  35276  knoppcnlem10  35977  areacirclem2  37182  fprodcn  44988