Theorem reldmmpo 7554

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 7527	. 2 ⊢ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
2		rngop.1	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
3		df-mpo 7425	. . . . 5 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
4	2, 3	eqtri 2784	. . . 4 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
5	4	dmeqi 5886	. . 3 ⊢ dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
6	5	releqi 5754	. 2 ⊢ (Rel dom 𝐹 ↔ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)})
7	1, 6	mpbir 234	1 ⊢ Rel dom 𝐹

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  dom cdm 5651  Rel wrel 5656  {coprab 7421   ∈ cmpo 7422

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-dm 5661  df-oprab 7424  df-mpo 7425

This theorem is used by:  reldmmap  8855  reldmrelexp  15174  reldmsets  17343  reldmress  17410  reldmprds  17619  gsum0  18873  reldmghm  19429  oppglsm  19856  reldmdprd  20213  reldmlmhm  21300  zrhval  21813  reldmdsmm  22039  frlmrcl  22063  reldmpsr  22222  reldmmpl  22295  reldmopsr  22354  reldmevls  22393  reldmmhp  22458  vr1val  22510  reldmevls1  22635  evl1fval  22646  matbas0pc  22724  mdetfval  22901  madufval  22952  qtopres  24017  fgabs  24198  reldmtng  24957  reldmnghm  25031  reldmnmhm  25032  dvbsss  26222  reldmmdeg  26375  nbgrprc0  29915  wwlksn  30426  of0r  33273  reldmrloc  33818  erlval  33819  reldmresv  33889  bj-restsnid  38008  reldmfrlm  43564  mzpmfp  43757  brovmptimex  45026  clnbgrprc0  48917  grimdmrel  48977  grlimdmrel  49077  1aryenef  49756  2aryenef  49767  resccat  50181  reldmfunc  50182  reldmoppf  50232  reldmup  50282  reldmup2  50289  reldmxpcALT  50354  fucofvalne  50432  reldmprcof  50482  reldmprcof2  50489  prcof1  50495  reldmlan  50718  reldmran  50719  reldmlan2  50724  reldmran2  50725  reldmlmd  50754  reldmcmd  50755