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 7294 | . 2 ⊢ Rel dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
2 | rngop.1 | . . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | |
3 | df-mpo 7196 | . . . . 5 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
4 | 2, 3 | eqtri 2759 | . . . 4 ⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
5 | 4 | dmeqi 5758 | . . 3 ⊢ dom 𝐹 = dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
6 | 5 | releqi 5634 | . 2 ⊢ (Rel dom 𝐹 ↔ Rel dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}) |
7 | 1, 6 | mpbir 234 | 1 ⊢ Rel dom 𝐹 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 399 = wceq 1543 ∈ wcel 2112 dom cdm 5536 Rel wrel 5541 {coprab 7192 ∈ cmpo 7193 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-sep 5177 ax-nul 5184 ax-pr 5307 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-nfc 2879 df-rab 3060 df-v 3400 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4224 df-if 4426 df-sn 4528 df-pr 4530 df-op 4534 df-br 5040 df-opab 5102 df-xp 5542 df-rel 5543 df-dm 5546 df-oprab 7195 df-mpo 7196 |
This theorem is referenced by: reldmmap 8495 reldmrelexp 14549 reldmsets 16693 reldmress 16734 reldmprds 16907 gsum0 18110 reldmghm 18575 oppglsm 18985 reldmdprd 19338 reldmlmhm 20016 zrhval 20428 reldmdsmm 20649 frlmrcl 20673 reldmpsr 20827 reldmmpl 20906 reldmopsr 20956 reldmevls 20998 vr1val 21067 reldmevls1 21187 evl1fval 21198 matbas0pc 21260 mdetfval 21437 madufval 21488 qtopres 22549 fgabs 22730 reldmtng 23490 reldmnghm 23564 reldmnmhm 23565 dvbsss 24753 reldmmdeg 24906 nbgrprc0 27376 wwlksn 27875 reldmresv 31198 bj-restsnid 34942 mzpmfp 40213 brovmptimex 41255 1aryenef 45607 2aryenef 45618 |
Copyright terms: Public domain | W3C validator |