Theorem reldmmpo 7548

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 7521	. 2 ⊢ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
2		rngop.1	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
3		df-mpo 7419	. . . . 5 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
4	2, 3	eqtri 2783	. . . 4 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
5	4	dmeqi 5888	. . 3 ⊢ dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
6	5	releqi 5758	. 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 5655  Rel wrel 5660  {coprab 7415   ∈ cmpo 7416

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 2732  ax-sep 5251  ax-pr 5398

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-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rab 3413  df-v 3452  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 5661  df-rel 5662  df-dm 5665  df-oprab 7418  df-mpo 7419

This theorem is used by:  reldmmap  8835  reldmrelexp  15095  reldmsets  17258  reldmress  17325  reldmprds  17534  gsum0  18787  reldmghm  19343  oppglsm  19770  reldmdprd  20127  reldmlmhm  21210  zrhval  21721  reldmdsmm  21947  frlmrcl  21971  reldmpsr  22130  reldmmpl  22203  reldmopsr  22262  reldmevls  22301  reldmmhp  22366  vr1val  22418  reldmevls1  22543  evl1fval  22554  matbas0pc  22632  mdetfval  22809  madufval  22860  qtopres  23925  fgabs  24106  reldmtng  24865  reldmnghm  24939  reldmnmhm  24940  dvbsss  26130  reldmmdeg  26283  nbgrprc0  29795  wwlksn  30306  of0r  33153  reldmrloc  33698  erlval  33699  reldmresv  33769  bj-restsnid  37838  mzpmfp  43593  brovmptimex  44868  clnbgrprc0  48737  grimdmrel  48797  grlimdmrel  48897  1aryenef  49576  2aryenef  49587  resccat  50001  reldmfunc  50002  reldmoppf  50052  reldmup  50102  reldmup2  50109  reldmxpcALT  50174  fucofvalne  50252  reldmprcof  50302  reldmprcof2  50309  prcof1  50315  reldmlan  50538  reldmran  50539  reldmlan2  50544  reldmran2  50545  reldmlmd  50574  reldmcmd  50575