![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnmptc | Structured version Visualization version GIF version |
Description: A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
Ref | Expression |
---|---|
cnmptid.j | ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
cnmptc.k | ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
cnmptc.p | ⊢ (𝜑 → 𝑃 ∈ 𝑌) |
Ref | Expression |
---|---|
cnmptc | ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑃) ∈ (𝐽 Cn 𝐾)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fconstmpt 5411 | . 2 ⊢ (𝑋 × {𝑃}) = (𝑥 ∈ 𝑋 ↦ 𝑃) | |
2 | cnmptid.j | . . 3 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | |
3 | cnmptc.k | . . 3 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) | |
4 | cnmptc.p | . . 3 ⊢ (𝜑 → 𝑃 ∈ 𝑌) | |
5 | cnconst2 21495 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑌) → (𝑋 × {𝑃}) ∈ (𝐽 Cn 𝐾)) | |
6 | 2, 3, 4, 5 | syl3anc 1439 | . 2 ⊢ (𝜑 → (𝑋 × {𝑃}) ∈ (𝐽 Cn 𝐾)) |
7 | 1, 6 | syl5eqelr 2864 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑃) ∈ (𝐽 Cn 𝐾)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 {csn 4398 ↦ cmpt 4965 × cxp 5353 ‘cfv 6135 (class class class)co 6922 TopOnctopon 21122 Cn ccn 21436 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pow 5077 ax-pr 5138 ax-un 7226 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-csb 3752 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-iun 4755 df-br 4887 df-opab 4949 df-mpt 4966 df-id 5261 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-res 5367 df-ima 5368 df-iota 6099 df-fun 6137 df-fn 6138 df-f 6139 df-fv 6143 df-ov 6925 df-oprab 6926 df-mpt2 6927 df-1st 7445 df-2nd 7446 df-map 8142 df-topgen 16490 df-top 21106 df-topon 21123 df-cn 21439 df-cnp 21440 |
This theorem is referenced by: cnmpt2c 21882 xkoinjcn 21899 txconn 21901 imasnopn 21902 imasncld 21903 imasncls 21904 istgp2 22303 tmdmulg 22304 tmdgsum 22307 tmdlactcn 22314 clsnsg 22321 tgpt0 22330 tlmtgp 22407 nmcn 23055 fsumcn 23081 expcn 23083 divccn 23084 cncfmptc 23122 cdivcncf 23128 iirevcn 23137 iihalf1cn 23139 iihalf2cn 23141 icchmeo 23148 evth 23166 evth2 23167 pcocn 23224 pcopt 23229 pcopt2 23230 pcoass 23231 csscld 23455 clsocv 23456 dvcnvlem 24176 plycn 24454 psercn2 24614 resqrtcn 24930 sqrtcn 24931 atansopn 25110 efrlim 25148 ipasslem7 28263 occllem 28734 rmulccn 30572 cxpcncf1 31275 txsconnlem 31821 cvxpconn 31823 cvmlift2lem2 31885 cvmlift2lem3 31886 cvmliftphtlem 31898 sinccvglem 32163 knoppcnlem10 33075 areacirclem2 34126 fprodcn 40740 |
Copyright terms: Public domain | W3C validator |