Theorem reldmmpo 7503

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.

Step	Hyp	Ref	Expression
1		reldmoprab 7476	. 2 ⊢ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
2		rngop.1	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
3		df-mpo 7374	. . . . 5 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
4	2, 3	eqtri 2752	. . . 4 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
5	4	dmeqi 5858	. . 3 ⊢ dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
6	5	releqi 5732	. 2 ⊢ (Rel dom 𝐹 ↔ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)})
7	1, 6	mpbir 231	1 ⊢ Rel dom 𝐹

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  dom cdm 5631  Rel wrel 5636  {coprab 7370   ∈ cmpo 7371

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-rel 5638  df-dm 5641  df-oprab 7373  df-mpo 7374

This theorem is referenced by:  reldmmap  8785  reldmrelexp  14963  reldmsets  17111  reldmress  17178  reldmprds  17387  gsum0  18587  reldmghm  19122  oppglsm  19548  reldmdprd  19905  reldmlmhm  20908  zrhval  21393  reldmdsmm  21618  frlmrcl  21642  reldmpsr  21799  reldmmpl  21873  reldmopsr  21928  reldmevls  21967  reldmmhp  22000  vr1val  22052  reldmevls1  22180  evl1fval  22191  matbas0pc  22272  mdetfval  22449  madufval  22500  qtopres  23561  fgabs  23742  reldmtng  24502  reldmnghm  24576  reldmnmhm  24577  dvbsss  25779  reldmmdeg  25938  nbgrprc0  29237  wwlksn  29740  of0r  32575  reldmrloc  33181  erlval  33182  reldmresv  33273  bj-restsnid  37048  mzpmfp  42708  brovmptimex  43989  clnbgrprc0  47794  grimdmrel  47853  grlimdmrel  47952  1aryenef  48607  2aryenef  48618  resccat  49036  reldmfunc  49037  reldmoppf  49087  reldmup  49137  reldmup2  49144  reldmxpcALT  49209  fucofvalne  49287  reldmprcof  49337  reldmprcof2  49344  prcof1  49350  reldmlan  49573  reldmran  49574  reldmlan2  49579  reldmran2  49580  reldmlmd  49609  reldmcmd  49610