| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > reldmmpo | Structured version Visualization version GIF version | ||
| Description: The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
| Ref | Expression |
|---|---|
| rngop.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
| Ref | Expression |
|---|---|
| reldmmpo | ⊢ Rel dom 𝐹 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | reldmoprab 7540 | . 2 ⊢ Rel dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
| 2 | rngop.1 | . . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | |
| 3 | df-mpo 7436 | . . . . 5 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
| 4 | 2, 3 | eqtri 2765 | . . . 4 ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
| 5 | 4 | dmeqi 5915 | . . 3 ⊢ dom 𝐹 = dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
| 6 | 5 | releqi 5787 | . 2 ⊢ (Rel dom 𝐹 ↔ Rel dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}) |
| 7 | 1, 6 | mpbir 231 | 1 ⊢ Rel dom 𝐹 |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 = wceq 1540 ∈ wcel 2108 dom cdm 5685 Rel wrel 5690 {coprab 7432 ∈ cmpo 7433 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-xp 5691 df-rel 5692 df-dm 5695 df-oprab 7435 df-mpo 7436 |
| This theorem is referenced by: reldmmap 8875 reldmrelexp 15060 reldmsets 17202 reldmress 17276 reldmprds 17493 gsum0 18697 reldmghm 19232 oppglsm 19660 reldmdprd 20017 reldmlmhm 21024 zrhval 21518 reldmdsmm 21753 frlmrcl 21777 reldmpsr 21934 reldmmpl 22008 reldmopsr 22063 reldmevls 22108 reldmmhp 22141 vr1val 22193 reldmevls1 22321 evl1fval 22332 matbas0pc 22413 mdetfval 22592 madufval 22643 qtopres 23706 fgabs 23887 reldmtng 24651 reldmnghm 24733 reldmnmhm 24734 dvbsss 25937 reldmmdeg 26096 nbgrprc0 29351 wwlksn 29857 of0r 32688 reldmrloc 33261 erlval 33262 reldmresv 33352 bj-restsnid 37088 mzpmfp 42758 brovmptimex 44040 clnbgrprc0 47807 grimdmrel 47866 grlimdmrel 47947 1aryenef 48566 2aryenef 48577 reldmup 48932 upfval 48933 reldmup2 48938 reldmxpcALT 48953 fucofvalne 49020 |
| Copyright terms: Public domain | W3C validator |