Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-pprod Structured version   Visualization version   GIF version

Definition df-pprod 31936
Description: Define the parallel product of two classes. Membership in this class is defined by pprodss4v 31966 and brpprod 31967. (Contributed by Scott Fenton, 11-Apr-2014.)
Assertion
Ref Expression
df-pprod pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V))))

Detailed syntax breakdown of Definition df-pprod
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cpprod 31912 . 2 class pprod(𝐴, 𝐵)
4 c1st 7151 . . . . 5 class 1st
5 cvv 3195 . . . . . 6 class V
65, 5cxp 5102 . . . . 5 class (V × V)
74, 6cres 5106 . . . 4 class (1st ↾ (V × V))
81, 7ccom 5108 . . 3 class (𝐴 ∘ (1st ↾ (V × V)))
9 c2nd 7152 . . . . 5 class 2nd
109, 6cres 5106 . . . 4 class (2nd ↾ (V × V))
112, 10ccom 5108 . . 3 class (𝐵 ∘ (2nd ↾ (V × V)))
128, 11ctxp 31911 . 2 class ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V))))
133, 12wceq 1481 1 wff pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V))))
Colors of variables: wff setvar class
This definition is referenced by:  dfpprod2  31964  pprodss4v  31966  brpprod  31967
  Copyright terms: Public domain W3C validator