![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fconst | Structured version Visualization version GIF version |
Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 14-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Ref | Expression |
---|---|
fconst.1 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
fconst | ⊢ (𝐴 × {𝐵}):𝐴⟶{𝐵} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fconst.1 | . . 3 ⊢ 𝐵 ∈ V | |
2 | fconstmpt 5368 | . . 3 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
3 | 1, 2 | fnmpti 6233 | . 2 ⊢ (𝐴 × {𝐵}) Fn 𝐴 |
4 | rnxpss 5783 | . 2 ⊢ ran (𝐴 × {𝐵}) ⊆ {𝐵} | |
5 | df-f 6105 | . 2 ⊢ ((𝐴 × {𝐵}):𝐴⟶{𝐵} ↔ ((𝐴 × {𝐵}) Fn 𝐴 ∧ ran (𝐴 × {𝐵}) ⊆ {𝐵})) | |
6 | 3, 4, 5 | mpbir2an 703 | 1 ⊢ (𝐴 × {𝐵}):𝐴⟶{𝐵} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2157 Vcvv 3385 ⊆ wss 3769 {csn 4368 × cxp 5310 ran crn 5313 Fn wfn 6096 ⟶wf 6097 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-sep 4975 ax-nul 4983 ax-pr 5097 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-ral 3094 df-rab 3098 df-v 3387 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-sn 4369 df-pr 4371 df-op 4375 df-br 4844 df-opab 4906 df-mpt 4923 df-id 5220 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-fun 6103 df-fn 6104 df-f 6105 |
This theorem is referenced by: fconstg 6307 fodomr 8353 ofsubeq0 11309 ser0f 13108 hashgval 13373 hashinf 13375 hashfxnn0 13377 prodf1f 14961 pwssplit1 19380 psrbag0 19816 xkofvcn 21816 ibl0 23894 dvcmul 24048 dvcmulf 24049 dvexp 24057 elqaalem3 24417 basellem7 25165 basellem9 25167 axlowdimlem8 26186 axlowdimlem9 26187 axlowdimlem10 26188 axlowdimlem11 26189 axlowdimlem12 26190 0oo 28169 occllem 28687 ho01i 29212 nlelchi 29445 hmopidmchi 29535 eulerpartlemt 30949 plymul02 31141 breprexpnat 31232 noetalem3 32378 fullfunfnv 32566 fullfunfv 32567 poimirlem16 33914 poimirlem19 33917 poimirlem23 33921 poimirlem24 33922 poimirlem25 33923 poimirlem28 33926 poimirlem29 33927 poimirlem30 33928 poimirlem31 33929 poimirlem32 33930 ftc1anclem5 33977 lfl0f 35090 diophrw 38108 pwssplit4 38444 ofsubid 39305 dvsconst 39311 dvsid 39312 binomcxplemnn0 39330 binomcxplemnotnn0 39337 aacllem 43349 |
Copyright terms: Public domain | W3C validator |