![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reldmmpo | Structured version Visualization version GIF version |
Description: The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
Ref | Expression |
---|---|
rngop.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
Ref | Expression |
---|---|
reldmmpo | ⊢ Rel dom 𝐹 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reldmoprab 7517 | . 2 ⊢ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
2 | rngop.1 | . . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | |
3 | df-mpo 7417 | . . . . 5 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | |
4 | 2, 3 | eqtri 2759 | . . . 4 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
5 | 4 | dmeqi 5904 | . . 3 ⊢ dom 𝐹 = dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
6 | 5 | releqi 5777 | . 2 ⊢ (Rel dom 𝐹 ↔ Rel dom {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}) |
7 | 1, 6 | mpbir 230 | 1 ⊢ Rel dom 𝐹 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 395 = wceq 1540 ∈ wcel 2105 dom cdm 5676 Rel wrel 5681 {coprab 7413 ∈ cmpo 7414 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-opab 5211 df-xp 5682 df-rel 5683 df-dm 5686 df-oprab 7416 df-mpo 7417 |
This theorem is referenced by: reldmmap 8832 reldmrelexp 14973 reldmsets 17103 reldmress 17180 reldmprds 17399 gsum0 18610 reldmghm 19130 oppglsm 19552 reldmdprd 19909 reldmlmhm 20781 zrhval 21277 reldmdsmm 21508 frlmrcl 21532 reldmpsr 21687 reldmmpl 21767 reldmopsr 21820 reldmevls 21867 vr1val 21936 reldmevls1 22057 evl1fval 22068 matbas0pc 22130 mdetfval 22309 madufval 22360 qtopres 23423 fgabs 23604 reldmtng 24368 reldmnghm 24450 reldmnmhm 24451 dvbsss 25652 reldmmdeg 25808 nbgrprc0 28859 wwlksn 29359 reldmresv 32711 bj-restsnid 36272 mzpmfp 41788 brovmptimex 43081 1aryenef 47419 2aryenef 47430 |
Copyright terms: Public domain | W3C validator |