Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  reldmmpo Structured version   Visualization version   GIF version

Theorem reldmmpo 7268
 Description: The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.)
Hypothesis
Ref Expression
rngop.1 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
Assertion
Ref Expression
reldmmpo Rel dom 𝐹
Distinct variable groups:   𝑦,𝐴   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem reldmmpo
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 reldmoprab 7242 . 2 Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
2 rngop.1 . . . . 5 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
3 df-mpo 7144 . . . . 5 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
42, 3eqtri 2824 . . . 4 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
54dmeqi 5741 . . 3 dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
65releqi 5620 . 2 (Rel dom 𝐹 ↔ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)})
71, 6mpbir 234 1 Rel dom 𝐹
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399   = wceq 1538   ∈ wcel 2112  dom cdm 5523  Rel wrel 5528  {coprab 7140   ∈ cmpo 7141 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-xp 5529  df-rel 5530  df-dm 5533  df-oprab 7143  df-mpo 7144 This theorem is referenced by:  reldmmap  8402  reldmrelexp  14376  reldmsets  16507  reldmress  16546  reldmprds  16718  gsum0  17890  reldmghm  18353  oppglsm  18763  reldmdprd  19116  reldmlmhm  19794  zrhval  20205  reldmdsmm  20426  frlmrcl  20450  reldmpsr  20603  reldmmpl  20669  reldmopsr  20717  reldmevls  20760  vr1val  20825  reldmevls1  20945  evl1fval  20956  matbas0pc  21018  mdetfval  21195  madufval  21246  qtopres  22307  fgabs  22488  reldmtng  23248  reldmnghm  23322  reldmnmhm  23323  dvbsss  24509  reldmmdeg  24662  nbgrprc0  27128  wwlksn  27627  reldmresv  30954  bj-restsnid  34503  mzpmfp  39685  brovmptimex  40727  1aryenef  45056  2aryenef  45067
 Copyright terms: Public domain W3C validator