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 5607 | . 2 ⊢ (𝑋 × {𝑃}) = (𝑥 ∈ 𝑋 ↦ 𝑃) | |
2 | cnmptid.j | . . 3 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | |
3 | cnmptc.k | . . 3 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) | |
4 | cnmptc.p | . . 3 ⊢ (𝜑 → 𝑃 ∈ 𝑌) | |
5 | cnconst2 21883 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑌) → (𝑋 × {𝑃}) ∈ (𝐽 Cn 𝐾)) | |
6 | 2, 3, 4, 5 | syl3anc 1366 | . 2 ⊢ (𝜑 → (𝑋 × {𝑃}) ∈ (𝐽 Cn 𝐾)) |
7 | 1, 6 | eqeltrrid 2916 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑃) ∈ (𝐽 Cn 𝐾)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2108 {csn 4559 ↦ cmpt 5137 × cxp 5546 ‘cfv 6348 (class class class)co 7148 TopOnctopon 21510 Cn ccn 21824 |
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 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7453 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1084 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-mo 2616 df-eu 2648 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-ne 3015 df-ral 3141 df-rex 3142 df-rab 3145 df-v 3495 df-sbc 3771 df-csb 3882 df-dif 3937 df-un 3939 df-in 3941 df-ss 3950 df-nul 4290 df-if 4466 df-pw 4539 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4831 df-iun 4912 df-br 5058 df-opab 5120 df-mpt 5138 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-fv 6356 df-ov 7151 df-oprab 7152 df-mpo 7153 df-1st 7681 df-2nd 7682 df-map 8400 df-topgen 16709 df-top 21494 df-topon 21511 df-cn 21827 df-cnp 21828 |
This theorem is referenced by: cnmpt2c 22270 xkoinjcn 22287 txconn 22289 imasnopn 22290 imasncld 22291 imasncls 22292 istgp2 22691 tmdmulg 22692 tmdgsum 22695 tmdlactcn 22702 clsnsg 22710 tgpt0 22719 tlmtgp 22796 nmcn 23444 fsumcn 23470 expcn 23472 divccn 23473 cncfmptc 23511 cdivcncf 23517 iirevcn 23526 iihalf1cn 23528 iihalf2cn 23530 icchmeo 23537 evth 23555 evth2 23556 pcocn 23613 pcopt 23618 pcopt2 23619 pcoass 23620 csscld 23844 clsocv 23845 dvcnvlem 24565 plycn 24843 psercn2 25003 resqrtcn 25322 sqrtcn 25323 atansopn 25502 efrlim 25539 ipasslem7 28605 occllem 29072 rmulccn 31164 cxpcncf1 31859 txsconnlem 32480 cvxpconn 32482 cvmlift2lem2 32544 cvmlift2lem3 32545 cvmliftphtlem 32557 sinccvglem 32908 knoppcnlem10 33834 areacirclem2 34975 fprodcn 41871 |
Copyright terms: Public domain | W3C validator |