Theorem reldmmpo 7523

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 7496	. 2 ⊢ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
2		rngop.1	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
3		df-mpo 7392	. . . . 5 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
4	2, 3	eqtri 2752	. . . 4 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
5	4	dmeqi 5868	. . 3 ⊢ dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
6	5	releqi 5740	. 2 ⊢ (Rel dom 𝐹 ↔ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)})
7	1, 6	mpbir 231	1 ⊢ Rel dom 𝐹

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  dom cdm 5638  Rel wrel 5643  {coprab 7388   ∈ cmpo 7389

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-dm 5648  df-oprab 7391  df-mpo 7392

This theorem is referenced by:  reldmmap  8808  reldmrelexp  14987  reldmsets  17135  reldmress  17202  reldmprds  17411  gsum0  18611  reldmghm  19146  oppglsm  19572  reldmdprd  19929  reldmlmhm  20932  zrhval  21417  reldmdsmm  21642  frlmrcl  21666  reldmpsr  21823  reldmmpl  21897  reldmopsr  21952  reldmevls  21991  reldmmhp  22024  vr1val  22076  reldmevls1  22204  evl1fval  22215  matbas0pc  22296  mdetfval  22473  madufval  22524  qtopres  23585  fgabs  23766  reldmtng  24526  reldmnghm  24600  reldmnmhm  24601  dvbsss  25803  reldmmdeg  25962  nbgrprc0  29261  wwlksn  29767  of0r  32602  reldmrloc  33208  erlval  33209  reldmresv  33300  bj-restsnid  37075  mzpmfp  42735  brovmptimex  44016  clnbgrprc0  47821  grimdmrel  47880  grlimdmrel  47979  1aryenef  48634  2aryenef  48645  resccat  49063  reldmfunc  49064  reldmoppf  49114  reldmup  49164  reldmup2  49171  reldmxpcALT  49236  fucofvalne  49314  reldmprcof  49364  reldmprcof2  49371  prcof1  49377  reldmlan  49600  reldmran  49601  reldmlan2  49606  reldmran2  49607  reldmlmd  49636  reldmcmd  49637