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

Theorem coass 5365
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
Dummy variables  x  y  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relco 5344 . 2  |-  Rel  (
( A  o.  B
)  o.  C )
2 relco 5344 . 2  |-  Rel  ( A  o.  ( B  o.  C ) )
3 excom 1898 . . . 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 653 . . . . 5  |-  ( ( ( x C z  /\  z B w )  /\  w A y )  <->  ( x C z  /\  (
z B w  /\  w A y ) ) )
542exbii 1713 . . . 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 255 . . 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 3081 . . . . . . 7  |-  z  e. 
_V
8 vex 3081 . . . . . . 7  |-  y  e. 
_V
97, 8brco 5016 . . . . . 6  |-  ( z ( A  o.  B
) y  <->  E. w
( z B w  /\  w A y ) )
109anbi2i 698 . . . . 5  |-  ( ( x C z  /\  z ( A  o.  B ) y )  <-> 
( x C z  /\  E. w ( z B w  /\  w A y ) ) )
1110exbii 1712 . . . 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 3081 . . . . 5  |-  x  e. 
_V
1312, 8opelco 5017 . . . 4  |-  ( <.
x ,  y >.  e.  ( ( A  o.  B )  o.  C
)  <->  E. z ( x C z  /\  z
( A  o.  B
) y ) )
14 exdistr 1824 . . . 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 280 . . 3  |-  ( <.
x ,  y >.  e.  ( ( A  o.  B )  o.  C
)  <->  E. z E. w
( x C z  /\  ( z B w  /\  w A y ) ) )
16 vex 3081 . . . . . . 7  |-  w  e. 
_V
1712, 16brco 5016 . . . . . 6  |-  ( x ( B  o.  C
) w  <->  E. z
( x C z  /\  z B w ) )
1817anbi1i 699 . . . . 5  |-  ( ( x ( B  o.  C ) w  /\  w A y )  <->  ( E. z ( x C z  /\  z B w )  /\  w A y ) )
1918exbii 1712 . . . 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 5017 . . . 4  |-  ( <.
x ,  y >.  e.  ( A  o.  ( B  o.  C )
)  <->  E. w ( x ( B  o.  C
) w  /\  w A y ) )
21 19.41v 1819 . . . . 5  |-  ( E. z ( ( x C z  /\  z B w )  /\  w A y )  <->  ( E. z ( x C z  /\  z B w )  /\  w A y ) )
2221exbii 1712 . . . 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 280 . . 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 280 . 2  |-  ( <.
x ,  y >.  e.  ( ( A  o.  B )  o.  C
)  <->  <. x ,  y
>.  e.  ( A  o.  ( B  o.  C
) ) )
251, 2, 24eqrelriiv 4940 1  |-  ( ( A  o.  B )  o.  C )  =  ( A  o.  ( B  o.  C )
)
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370    = wceq 1437   E.wex 1659    e. wcel 1867   <.cop 3999   class class class wbr 4417    o. ccom 4849
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-br 4418  df-opab 4476  df-xp 4851  df-rel 4852  df-co 4854
This theorem is referenced by:  funcoeqres  5852  fcof1oinvd  6197  tposco  7003  mapen  7733  mapfien  7918  hashfacen  12601  relexpsucnnl  13063  relexpaddnn  13082  cofuass  15738  setccatid  15923  estrccatid  15961  frmdup3lem  16594  symggrp  16985  f1omvdco2  17033  symggen  17055  psgnunilem1  17078  gsumval3  17469  gsumzf1o  17474  gsumzmhm  17498  prds1  17770  psrass1lem  18529  pf1mpf  18868  pf1ind  18871  qtophmeo  20756  uniioombllem2  22414  uniioombllem2OLD  22415  cncombf  22488  motgrp  24445  pjsdi2i  27642  pjadj2coi  27689  pj3lem1  27691  pj3i  27693  fcoinver  28050  fcobij  28150  fcobijfs  28151  symgfcoeu  28444  derangenlem  29679  subfacp1lem5  29692  erdsze2lem2  29712  pprodcnveq  30432  cocnv  31756  ltrncoidN  33402  trlcoabs2N  33998  trlcoat  33999  trlcone  34004  cdlemg46  34011  cdlemg47  34012  ltrnco4  34015  tgrpgrplem  34025  tendoplass  34059  cdlemi2  34095  cdlemk2  34108  cdlemk4  34110  cdlemk8  34114  cdlemk45  34223  cdlemk54  34234  cdlemk55a  34235  erngdvlem3  34266  erngdvlem3-rN  34274  tendocnv  34298  dvhvaddass  34374  dvhlveclem  34385  cdlemn8  34481  dihopelvalcpre  34525  dih1dimatlem0  34605  diophrw  35310  eldioph2  35313  mendring  35761  cortrcltrcl  35975  corclrtrcl  35976  cortrclrcl  35978  cotrclrtrcl  35979  cortrclrtrcl  35980  frege131d  35999  rngccatidALTV  38762  ringccatidALTV  38825
  Copyright terms: Public domain W3C validator