Theorem reldmmpo 7561

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 7534	. 2 ⊢ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
2		rngop.1	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
3		df-mpo 7432	. . . . 5 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
4	2, 3	eqtri 2786	. . . 4 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
5	4	dmeqi 5890	. . 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 1569   ∈ wcel 2146  dom cdm 5654  Rel wrel 5659  {coprab 7428   ∈ cmpo 7429

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-br 5106  df-opab 5170  df-xp 5660  df-rel 5661  df-dm 5664  df-oprab 7431  df-mpo 7432

This theorem is used by:  reldmmap  8866  reldmrelexp  15186  reldmsets  17355  reldmress  17422  reldmprds  17631  gsum0  18885  reldmghm  19441  oppglsm  19868  reldmdprd  20225  reldmlmhm  21312  zrhval  21825  reldmdsmm  22051  frlmrcl  22075  reldmpsr  22234  reldmmpl  22307  reldmopsr  22366  reldmevls  22405  reldmmhp  22470  vr1val  22522  reldmevls1  22647  evl1fval  22658  matbas0pc  22736  mdetfval  22913  madufval  22964  qtopres  24029  fgabs  24210  reldmtng  24969  reldmnghm  25043  reldmnmhm  25044  dvbsss  26234  reldmmdeg  26387  nbgrprc0  29927  wwlksn  30438  of0r  33327  reldmrloc  33871  erlval  33872  reldmresv  33942  bj-restsnid  38147  reldmfrlm  43704  mzpmfp  43898  brovmptimex  45167  clnbgrprc0  49057  grimdmrel  49117  grlimdmrel  49217  1aryenef  49896  2aryenef  49907  resccat  50327  reldmfunc  50328  reldmoppf  50380  reldmup  50430  reldmup2  50437  reldmxpcALT  50508  fucofvalne  50586  reldmprcof  50649  reldmprcof2  50656  prcof1  50662  reldmlan  50933  reldmran  50934  reldmlan2  50939  reldmran2  50940  reldmlmd  50969  reldmcmd  50970