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

Theorem coass 5191
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 )
)
Dummy variables  x  y  z  w are mutually distinct and distinct from all other variables.

Proof of Theorem coass
StepHypRef Expression
1 relco 5171 . 2  |-  Rel  (
( A  o.  B
)  o.  C )
2 relco 5171 . 2  |-  Rel  ( A  o.  ( B  o.  C ) )
3 excom 1790 . . . 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 632 . . . . 5  |-  ( ( ( x C z  /\  z B w )  /\  w A y )  <->  ( x C z  /\  (
z B w  /\  w A y ) ) )
542exbii 1572 . . . 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 2794 . . . . . . 7  |-  z  e. 
_V
8 vex 2794 . . . . . . 7  |-  y  e. 
_V
97, 8brco 4853 . . . . . 6  |-  ( z ( A  o.  B
) y  <->  E. w
( z B w  /\  w A y ) )
109anbi2i 677 . . . . 5  |-  ( ( x C z  /\  z ( A  o.  B ) y )  <-> 
( x C z  /\  E. w ( z B w  /\  w A y ) ) )
1110exbii 1571 . . . 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 2794 . . . . 5  |-  x  e. 
_V
1312, 8opelco 4854 . . . 4  |-  ( <.
x ,  y >.  e.  ( ( A  o.  B )  o.  C
)  <->  E. z ( x C z  /\  z
( A  o.  B
) y ) )
14 exdistr 1851 . . . 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 2794 . . . . . . 7  |-  w  e. 
_V
1712, 16brco 4853 . . . . . 6  |-  ( x ( B  o.  C
) w  <->  E. z
( x C z  /\  z B w ) )
1817anbi1i 678 . . . . 5  |-  ( ( x ( B  o.  C ) w  /\  w A y )  <->  ( E. z ( x C z  /\  z B w )  /\  w A y ) )
1918exbii 1571 . . . 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 4854 . . . 4  |-  ( <.
x ,  y >.  e.  ( A  o.  ( B  o.  C )
)  <->  E. w ( x ( B  o.  C
) w  /\  w A y ) )
21 19.41v 1846 . . . . 5  |-  ( E. z ( ( x C z  /\  z B w )  /\  w A y )  <->  ( E. z ( x C z  /\  z B w )  /\  w A y ) )
2221exbii 1571 . . . 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 4782 1  |-  ( ( A  o.  B )  o.  C )  =  ( A  o.  ( B  o.  C )
)
Colors of variables: wff set class
Syntax hints:    /\ wa 360   E.wex 1530    = wceq 1625    e. wcel 1687   <.cop 3646   class class class wbr 4026    o. ccom 4694
This theorem is referenced by:  funcoeqres  5471  fcof1o  5766  tposco  6228  mapen  7022  mapfien  7396  hashfacen  11388  cofuass  13759  setccatid  13912  frmdup3  14484  symggrp  14776  gsumval3  15187  gsumzf1o  15192  gsumzmhm  15206  prds1  15393  psrass1lem  16119  qtophmeo  17504  uniioombllem2  18934  cncombf  19009  pf1mpf  19431  pf1ind  19434  pjsdi2i  22731  pjadj2coi  22778  pj3lem1  22780  pj3i  22782  derangenlem  23108  subfacp1lem5  23121  erdsze2lem2  23141  relexpsucl  23434  relexpadd  23441  pprodcnveq  23833  hmeogrpi  24937  cmpmorass  25367  cocnv  25794  diophrw  26239  eldioph2  26242  f1omvdco2  26792  symggen  26812  psgnunilem1  26817  mendrng  26901  ltrncoidN  29586  trlcoabs2N  30180  trlcoat  30181  trlcone  30186  cdlemg46  30193  cdlemg47  30194  ltrnco4  30197  tgrpgrplem  30207  tendoplass  30241  cdlemi2  30277  cdlemk2  30290  cdlemk4  30292  cdlemk8  30296  cdlemk45  30405  cdlemk54  30416  cdlemk55a  30417  erngdvlem3  30448  erngdvlem3-rN  30456  tendocnv  30480  dvhvaddass  30556  dvhlveclem  30567  cdlemn8  30663  dihopelvalcpre  30707  dih1dimatlem0  30787
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-14 1691  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267  ax-sep 4144  ax-nul 4152  ax-pr 4215
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-eu 2150  df-mo 2151  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-ne 2451  df-ral 2551  df-rex 2552  df-rab 2555  df-v 2793  df-dif 3158  df-un 3160  df-in 3162  df-ss 3169  df-nul 3459  df-if 3569  df-sn 3649  df-pr 3650  df-op 3652  df-br 4027  df-opab 4081  df-xp 4696  df-rel 4697  df-co 4699
  Copyright terms: Public domain W3C validator