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

Theorem reldmdprd 19859
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 19857 . 2 DProd = (𝑔 ∈ Grp, 𝑠 ∈ { ∣ (:dom ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom (∀𝑦 ∈ (dom ∖ {𝑥})(𝑥) ⊆ ((Cntz‘𝑔)‘(𝑦)) ∧ ((𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘ ( “ (dom ∖ {𝑥})))) = {(0g𝑔)}))} ↦ ran (𝑓 ∈ {X𝑥 ∈ dom 𝑠(𝑠𝑥) ∣ finSupp (0g𝑔)} ↦ (𝑔 Σg 𝑓)))
21reldmmpo 7538 1 Rel dom DProd
Colors of variables: wff setvar class
Syntax hints:  wa 397   = wceq 1542  {cab 2710  wral 3062  {crab 3433  cdif 3944  cin 3946  wss 3947  {csn 4627   cuni 4907   class class class wbr 5147  cmpt 5230  dom cdm 5675  ran crn 5676  cima 5678  Rel wrel 5680  wf 6536  cfv 6540  (class class class)co 7404  Xcixp 8887   finSupp cfsupp 9357  0gc0g 17381   Σg cgsu 17382  mrClscmrc 17523  Grpcgrp 18815  SubGrpcsubg 18994  Cntzccntz 19173   DProd cdprd 19855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682  df-dm 5685  df-oprab 7408  df-mpo 7409  df-dprd 19857
This theorem is referenced by:  dprddomprc  19862  dprdval0prc  19864  dprdval  19865  dprdgrp  19867  dprdf  19868  dprdssv  19878  subgdmdprd  19896  dprd2da  19904  dpjfval  19917
  Copyright terms: Public domain W3C validator