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 5609 | . . 3 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
3 | 1, 2 | fnmpti 6486 | . 2 ⊢ (𝐴 × {𝐵}) Fn 𝐴 |
4 | rnxpss 6024 | . 2 ⊢ ran (𝐴 × {𝐵}) ⊆ {𝐵} | |
5 | df-f 6354 | . 2 ⊢ ((𝐴 × {𝐵}):𝐴⟶{𝐵} ↔ ((𝐴 × {𝐵}) Fn 𝐴 ∧ ran (𝐴 × {𝐵}) ⊆ {𝐵})) | |
6 | 3, 4, 5 | mpbir2an 709 | 1 ⊢ (𝐴 × {𝐵}):𝐴⟶{𝐵} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 Vcvv 3495 ⊆ wss 3936 {csn 4561 × cxp 5548 ran crn 5551 Fn wfn 6345 ⟶wf 6346 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-sep 5196 ax-nul 5203 ax-pr 5322 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rab 3147 df-v 3497 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4562 df-pr 4564 df-op 4568 df-br 5060 df-opab 5122 df-mpt 5140 df-id 5455 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-fun 6352 df-fn 6353 df-f 6354 |
This theorem is referenced by: fconstg 6561 fodomr 8662 ofsubeq0 11629 ser0f 13417 hashgval 13687 hashinf 13689 hashfxnn0 13691 prodf1f 15242 pwssplit1 19825 psrbag0 20268 xkofvcn 22286 rrx0el 23995 ibl0 24381 dvcmul 24535 dvcmulf 24536 dvexp 24544 elqaalem3 24904 basellem7 25658 basellem9 25660 axlowdimlem8 26729 axlowdimlem9 26730 axlowdimlem10 26731 axlowdimlem11 26732 axlowdimlem12 26733 0oo 28560 occllem 29074 ho01i 29599 nlelchi 29832 hmopidmchi 29922 eulerpartlemt 31624 plymul02 31811 breprexpnat 31900 noetalem3 33214 fullfunfnv 33402 fullfunfv 33403 poimirlem16 34902 poimirlem19 34905 poimirlem23 34909 poimirlem24 34910 poimirlem25 34911 poimirlem28 34914 poimirlem29 34915 poimirlem30 34916 poimirlem31 34917 poimirlem32 34918 ftc1anclem5 34965 lfl0f 36199 diophrw 39349 pwssplit4 39682 ofsubid 40649 dvsconst 40655 dvsid 40656 binomcxplemnn0 40674 binomcxplemnotnn0 40681 aacllem 44895 |
Copyright terms: Public domain | W3C validator |