Theorem cnmptc 23618

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

Syntax hints:   → wi 4   ∈ wcel 2114  {csn 4582   ↦ cmpt 5181   × cxp 5630  ‘cfv 6500  (class class class)co 7368  TopOnctopon 22866   Cn ccn 23180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-1st 7943  df-2nd 7944  df-map 8777  df-topgen 17375  df-top 22850  df-topon 22867  df-cn 23183  df-cnp 23184

This theorem is referenced by:  cnmpt2c  23626  xkoinjcn  23643  txconn  23645  imasnopn  23646  imasncld  23647  imasncls  23648  istgp2  24047  tmdmulg  24048  tmdgsum  24051  tmdlactcn  24058  clsnsg  24066  tgpt0  24075  tlmtgp  24152  nmcn  24801  fsumcn  24829  expcn  24831  divccn  24832  expcnOLD  24833  divccnOLD  24834  cncfmptc  24873  cdivcncf  24882  iirevcn  24892  iihalf1cn  24894  iihalf1cnOLD  24895  iihalf2cn  24897  iihalf2cnOLD  24898  icchmeo  24906  icchmeoOLD  24907  evth  24926  evth2  24927  pcocn  24985  pcopt  24990  pcopt2  24991  pcoass  24992  csscld  25217  clsocv  25218  dvcnvlem  25948  plycn  26234  plycnOLD  26235  psercn2  26400  psercn2OLD  26401  resqrtcn  26727  sqrtcn  26728  atansopn  26910  efrlim  26947  efrlimOLD  26948  ipasslem7  30924  occllem  31391  rmulccn  34106  cxpcncf1  34773  txsconnlem  35456  cvxpconn  35458  cvmlift2lem2  35520  cvmlift2lem3  35521  cvmliftphtlem  35533  sinccvglem  35888  knoppcnlem10  36724  areacirclem2  37960  fprodcn  45960