MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  coass Unicode version

Theorem coass 5164
Description: Associative law for class composition. Theorem 27 of [Suppes] p. 64. Also Exercise 21 of [Enderton] p. 53. Interestingly, this law holds for any classes whatsoever, not just functions or even relations. (Contributed by NM, 27-Jan-1997.)
Assertion
Ref Expression
coass  |-  ( ( A  o.  B )  o.  C )  =  ( A  o.  ( B  o.  C )
)

Proof of Theorem coass
StepHypRef Expression
1 relco 5144 . 2  |-  Rel  (
( A  o.  B
)  o.  C )
2 relco 5144 . 2  |-  Rel  ( A  o.  ( B  o.  C ) )
3 excom 1765 . . . 4  |-  ( E. z E. w ( x C z  /\  ( z B w  /\  w A y ) )  <->  E. w E. z ( x C z  /\  ( z B w  /\  w A y ) ) )
4 anass 633 . . . . 5  |-  ( ( ( x C z  /\  z B w )  /\  w A y )  <->  ( x C z  /\  (
z B w  /\  w A y ) ) )
542exbii 1581 . . . 4  |-  ( E. w E. z ( ( x C z  /\  z B w )  /\  w A y )  <->  E. w E. z ( x C z  /\  ( z B w  /\  w A y ) ) )
63, 5bitr4i 245 . . 3  |-  ( E. z E. w ( x C z  /\  ( z B w  /\  w A y ) )  <->  E. w E. z ( ( x C z  /\  z B w )  /\  w A y ) )
7 vex 2760 . . . . . . 7  |-  z  e. 
_V
8 vex 2760 . . . . . . 7  |-  y  e. 
_V
97, 8brco 4826 . . . . . 6  |-  ( z ( A  o.  B
) y  <->  E. w
( z B w  /\  w A y ) )
109anbi2i 678 . . . . 5  |-  ( ( x C z  /\  z ( A  o.  B ) y )  <-> 
( x C z  /\  E. w ( z B w  /\  w A y ) ) )
1110exbii 1580 . . . 4  |-  ( E. z ( x C z  /\  z ( A  o.  B ) y )  <->  E. z
( x C z  /\  E. w ( z B w  /\  w A y ) ) )
12 vex 2760 . . . . 5  |-  x  e. 
_V
1312, 8opelco 4827 . . . 4  |-  ( <.
x ,  y >.  e.  ( ( A  o.  B )  o.  C
)  <->  E. z ( x C z  /\  z
( A  o.  B
) y ) )
14 exdistr 2040 . . . 4  |-  ( E. z E. w ( x C z  /\  ( z B w  /\  w A y ) )  <->  E. z
( x C z  /\  E. w ( z B w  /\  w A y ) ) )
1511, 13, 143bitr4i 270 . . 3  |-  ( <.
x ,  y >.  e.  ( ( A  o.  B )  o.  C
)  <->  E. z E. w
( x C z  /\  ( z B w  /\  w A y ) ) )
16 vex 2760 . . . . . . 7  |-  w  e. 
_V
1712, 16brco 4826 . . . . . 6  |-  ( x ( B  o.  C
) w  <->  E. z
( x C z  /\  z B w ) )
1817anbi1i 679 . . . . 5  |-  ( ( x ( B  o.  C ) w  /\  w A y )  <->  ( E. z ( x C z  /\  z B w )  /\  w A y ) )
1918exbii 1580 . . . 4  |-  ( E. w ( x ( B  o.  C ) w  /\  w A y )  <->  E. w
( E. z ( x C z  /\  z B w )  /\  w A y ) )
2012, 8opelco 4827 . . . 4  |-  ( <.
x ,  y >.  e.  ( A  o.  ( B  o.  C )
)  <->  E. w ( x ( B  o.  C
) w  /\  w A y ) )
21 19.41v 2035 . . . . 5  |-  ( E. z ( ( x C z  /\  z B w )  /\  w A y )  <->  ( E. z ( x C z  /\  z B w )  /\  w A y ) )
2221exbii 1580 . . . 4  |-  ( E. w E. z ( ( x C z  /\  z B w )  /\  w A y )  <->  E. w
( E. z ( x C z  /\  z B w )  /\  w A y ) )
2319, 20, 223bitr4i 270 . . 3  |-  ( <.
x ,  y >.  e.  ( A  o.  ( B  o.  C )
)  <->  E. w E. z
( ( x C z  /\  z B w )  /\  w A y ) )
246, 15, 233bitr4i 270 . 2  |-  ( <.
x ,  y >.  e.  ( ( A  o.  B )  o.  C
)  <->  <. x ,  y
>.  e.  ( A  o.  ( B  o.  C
) ) )
251, 2, 24eqrelriiv 4755 1  |-  ( ( A  o.  B )  o.  C )  =  ( A  o.  ( B  o.  C )
)
Colors of variables: wff set class
Syntax hints:    /\ wa 360   E.wex 1537    = wceq 1619    e. wcel 1621   <.cop 3603   class class class wbr 3983    o. ccom 4651
This theorem is referenced by:  funcoeqres  5428  fcof1o  5723  tposco  6185  mapen  6979  mapfien  7353  hashfacen  11343  cofuass  13711  setccatid  13864  frmdup3  14436  symggrp  14728  gsumval3  15139  gsumzf1o  15144  gsumzmhm  15158  prds1  15345  psrass1lem  16071  qtophmeo  17456  uniioombllem2  18886  cncombf  18961  pf1mpf  19383  pf1ind  19386  pjsdi2i  22683  pjadj2coi  22730  pj3lem1  22732  pj3i  22734  derangenlem  23060  subfacp1lem5  23073  erdsze2lem2  23093  relexpsucl  23386  relexpadd  23393  pprodcnveq  23785  hmeogrpi  24889  cmpmorass  25319  cocnv  25746  diophrw  26191  eldioph2  26194  f1omvdco2  26744  symggen  26764  psgnunilem1  26769  mendrng  26853  ltrncoidN  29468  trlcoabs2N  30062  trlcoat  30063  trlcone  30068  cdlemg46  30075  cdlemg47  30076  ltrnco4  30079  tgrpgrplem  30089  tendoplass  30123  cdlemi2  30159  cdlemk2  30172  cdlemk4  30174  cdlemk8  30178  cdlemk45  30287  cdlemk54  30298  cdlemk55a  30299  erngdvlem3  30330  erngdvlem3-rN  30338  tendocnv  30362  dvhvaddass  30438  dvhlveclem  30449  cdlemn8  30545  dihopelvalcpre  30589  dih1dimatlem0  30669
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4101  ax-nul 4109  ax-pr 4172
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rex 2522  df-rab 2525  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-op 3609  df-br 3984  df-opab 4038  df-xp 4661  df-rel 4662  df-co 4664
  Copyright terms: Public domain W3C validator