![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reldmprds | Structured version Visualization version GIF version |
Description: The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
Ref | Expression |
---|---|
reldmprds | ⊢ Rel dom Xs |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-prds 17394 | . 2 ⊢ Xs = (𝑠 ∈ V, 𝑟 ∈ V ↦ ⦋X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({〈(Base‘ndx), 𝑣〉, 〈(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))〉, 〈(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))〉} ∪ {〈(Scalar‘ndx), 𝑠〉, 〈( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))〉, 〈(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))〉}) ∪ ({〈(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))〉, 〈(le‘ndx), {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}〉, 〈(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))〉} ∪ {〈(Hom ‘ndx), ℎ〉, 〈(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(〈((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)〉(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))〉}))) | |
2 | 1 | reldmmpo 7536 | 1 ⊢ Rel dom Xs |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 395 ∀wral 3053 Vcvv 3466 ⦋csb 3886 ∪ cun 3939 ⊆ wss 3941 {csn 4621 {cpr 4623 {ctp 4625 〈cop 4627 class class class wbr 5139 {copab 5201 ↦ cmpt 5222 × cxp 5665 dom cdm 5667 ran crn 5668 ∘ ccom 5671 Rel wrel 5672 ‘cfv 6534 (class class class)co 7402 ∈ cmpo 7404 1st c1st 7967 2nd c2nd 7968 Xcixp 8888 supcsup 9432 0cc0 11107 ℝ*cxr 11245 < clt 11246 ndxcnx 17127 Basecbs 17145 +gcplusg 17198 .rcmulr 17199 Scalarcsca 17201 ·𝑠 cvsca 17202 ·𝑖cip 17203 TopSetcts 17204 lecple 17205 distcds 17207 Hom chom 17209 compcco 17210 TopOpenctopn 17368 ∏tcpt 17385 Σg cgsu 17387 Xscprds 17392 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-sep 5290 ax-nul 5297 ax-pr 5418 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-rab 3425 df-v 3468 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-nul 4316 df-if 4522 df-sn 4622 df-pr 4624 df-op 4628 df-br 5140 df-opab 5202 df-xp 5673 df-rel 5674 df-dm 5677 df-oprab 7406 df-mpo 7407 df-prds 17394 |
This theorem is referenced by: dsmmval 21599 dsmmval2 21601 dsmmbas2 21602 dsmmfi 21603 |
Copyright terms: Public domain | W3C validator |