![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fconstg | Structured version Visualization version GIF version |
Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 19-Oct-2004.) |
Ref | Expression |
---|---|
fconstg | ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sneq 4482 | . . . 4 ⊢ (𝑥 = 𝐵 → {𝑥} = {𝐵}) | |
2 | 1 | xpeq2d 5473 | . . 3 ⊢ (𝑥 = 𝐵 → (𝐴 × {𝑥}) = (𝐴 × {𝐵})) |
3 | feq1 6363 | . . . 4 ⊢ ((𝐴 × {𝑥}) = (𝐴 × {𝐵}) → ((𝐴 × {𝑥}):𝐴⟶{𝑥} ↔ (𝐴 × {𝐵}):𝐴⟶{𝑥})) | |
4 | feq3 6365 | . . . 4 ⊢ ({𝑥} = {𝐵} → ((𝐴 × {𝐵}):𝐴⟶{𝑥} ↔ (𝐴 × {𝐵}):𝐴⟶{𝐵})) | |
5 | 3, 4 | sylan9bb 510 | . . 3 ⊢ (((𝐴 × {𝑥}) = (𝐴 × {𝐵}) ∧ {𝑥} = {𝐵}) → ((𝐴 × {𝑥}):𝐴⟶{𝑥} ↔ (𝐴 × {𝐵}):𝐴⟶{𝐵})) |
6 | 2, 1, 5 | syl2anc 584 | . 2 ⊢ (𝑥 = 𝐵 → ((𝐴 × {𝑥}):𝐴⟶{𝑥} ↔ (𝐴 × {𝐵}):𝐴⟶{𝐵})) |
7 | vex 3440 | . . 3 ⊢ 𝑥 ∈ V | |
8 | 7 | fconst 6433 | . 2 ⊢ (𝐴 × {𝑥}):𝐴⟶{𝑥} |
9 | 6, 8 | vtoclg 3510 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1522 ∈ wcel 2081 {csn 4472 × cxp 5441 ⟶wf 6221 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pr 5221 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rab 3114 df-v 3439 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-br 4963 df-opab 5025 df-mpt 5042 df-id 5348 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-fun 6227 df-fn 6228 df-f 6229 |
This theorem is referenced by: fnconstg 6435 fconst6g 6436 xpsng 6764 fvconst2g 6831 fconst2g 6832 xkoptsub 21946 mbfconstlem 23911 i1fmulclem 23986 i1fmulc 23987 itg2mulclem 24030 dvcmulf 24225 dvef 24260 coemulc 24528 resf1o 30154 locfinref 30722 ccatmulgnn0dir 31429 frlmvscadiccat 38672 |
Copyright terms: Public domain | W3C validator |