Theorem cnmptc 23510

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 5729	. 2 ⊢ (𝑋 × {𝑃}) = (𝑥 ∈ 𝑋 ↦ 𝑃)
2		cnmptid.j	. . 3 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
3		cnmptc.k	. . 3 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
4		cnmptc.p	. . 3 ⊢ (𝜑 → 𝑃 ∈ 𝑌)
5		cnconst2 23131	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑌) → (𝑋 × {𝑃}) ∈ (𝐽 Cn 𝐾))
6	2, 3, 4, 5	syl3anc 1368	. 2 ⊢ (𝜑 → (𝑋 × {𝑃}) ∈ (𝐽 Cn 𝐾))
7	1, 6	eqeltrrid 2830	1 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑃) ∈ (𝐽 Cn 𝐾))

Syntax hints:   → wi 4   ∈ wcel 2098  {csn 4621   ↦ cmpt 5222   × cxp 5665  ‘cfv 6534  (class class class)co 7402  TopOnctopon 22756   Cn ccn 23072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-id 5565  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-fv 6542  df-ov 7405  df-oprab 7406  df-mpo 7407  df-1st 7969  df-2nd 7970  df-map 8819  df-topgen 17394  df-top 22740  df-topon 22757  df-cn 23075  df-cnp 23076

This theorem is referenced by:  cnmpt2c  23518  xkoinjcn  23535  txconn  23537  imasnopn  23538  imasncld  23539  imasncls  23540  istgp2  23939  tmdmulg  23940  tmdgsum  23943  tmdlactcn  23950  clsnsg  23958  tgpt0  23967  tlmtgp  24044  nmcn  24704  fsumcn  24732  expcn  24734  divccn  24735  expcnOLD  24736  divccnOLD  24737  cncfmptc  24776  cdivcncf  24785  iirevcn  24795  iihalf1cn  24797  iihalf1cnOLD  24798  iihalf2cn  24800  iihalf2cnOLD  24801  icchmeo  24809  icchmeoOLD  24810  evth  24829  evth2  24830  pcocn  24888  pcopt  24893  pcopt2  24894  pcoass  24895  csscld  25121  clsocv  25122  dvcnvlem  25852  plycn  26139  plycnOLD  26140  psercn2  26300  psercn2OLD  26301  resqrtcn  26625  sqrtcn  26626  atansopn  26805  efrlim  26842  efrlimOLD  26843  ipasslem7  30584  occllem  31051  rmulccn  33428  cxpcncf1  34126  txsconnlem  34749  cvxpconn  34751  cvmlift2lem2  34813  cvmlift2lem3  34814  cvmliftphtlem  34826  sinccvglem  35175  knoppcnlem10  35879  areacirclem2  37081  fprodcn  44862