MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reldmdprd Structured version   Visualization version   GIF version

Theorem reldmdprd 19241
Description: The domain of the internal direct product operation is a relation. (Contributed by Mario Carneiro, 25-Apr-2016.) (Proof shortened by AV, 11-Jul-2019.)
Assertion
Ref Expression
reldmdprd Rel dom DProd

Proof of Theorem reldmdprd
Dummy variables 𝑔 𝑓 𝑠 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-dprd 19239 . 2 DProd = (𝑔 ∈ Grp, 𝑠 ∈ { ∣ (:dom ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom (∀𝑦 ∈ (dom ∖ {𝑥})(𝑥) ⊆ ((Cntz‘𝑔)‘(𝑦)) ∧ ((𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘ ( “ (dom ∖ {𝑥})))) = {(0g𝑔)}))} ↦ ran (𝑓 ∈ {X𝑥 ∈ dom 𝑠(𝑠𝑥) ∣ finSupp (0g𝑔)} ↦ (𝑔 Σg 𝑓)))
21reldmmpo 7303 1 Rel dom DProd
Colors of variables: wff setvar class
Syntax hints:  wa 399   = wceq 1542  {cab 2717  wral 3054  {crab 3058  cdif 3841  cin 3843  wss 3844  {csn 4517   cuni 4797   class class class wbr 5031  cmpt 5111  dom cdm 5526  ran crn 5527  cima 5529  Rel wrel 5531  wf 6336  cfv 6340  (class class class)co 7173  Xcixp 8510   finSupp cfsupp 8909  0gc0g 16819   Σg cgsu 16820  mrClscmrc 16960  Grpcgrp 18222  SubGrpcsubg 18394  Cntzccntz 18566   DProd cdprd 19237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-sep 5168  ax-nul 5175  ax-pr 5297
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-v 3401  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-nul 4213  df-if 4416  df-sn 4518  df-pr 4520  df-op 4524  df-br 5032  df-opab 5094  df-xp 5532  df-rel 5533  df-dm 5536  df-oprab 7177  df-mpo 7178  df-dprd 19239
This theorem is referenced by:  dprddomprc  19244  dprdval0prc  19246  dprdval  19247  dprdgrp  19249  dprdf  19250  dprdssv  19260  subgdmdprd  19278  dprd2da  19286  dpjfval  19299
  Copyright terms: Public domain W3C validator