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  18593  reldmghm  19128  oppglsm  19556  reldmdprd  19913  reldmlmhm  20964  zrhval  21449  reldmdsmm  21675  frlmrcl  21699  reldmpsr  21856  reldmmpl  21930  reldmopsr  21985  reldmevls  22024  reldmmhp  22057  vr1val  22109  reldmevls1  22237  evl1fval  22248  matbas0pc  22329  mdetfval  22506  madufval  22557  qtopres  23618  fgabs  23799  reldmtng  24559  reldmnghm  24633  reldmnmhm  24634  dvbsss  25836  reldmmdeg  25995  nbgrprc0  29314  wwlksn  29817  of0r  32652  reldmrloc  33224  erlval  33225  reldmresv  33293  bj-restsnid  37068  mzpmfp  42728  brovmptimex  44009  clnbgrprc0  47814  grimdmrel  47873  grlimdmrel  47972  1aryenef  48627  2aryenef  48638  resccat  49056  reldmfunc  49057  reldmoppf  49107  reldmup  49157  reldmup2  49164  reldmxpcALT  49229  fucofvalne  49307  reldmprcof  49357  reldmprcof2  49364  prcof1  49370  reldmlan  49593  reldmran  49594  reldmlan2  49599  reldmran2  49600  reldmlmd  49629  reldmcmd  49630