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

Theorem coass 5373
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 5352 . 2  |-  Rel  (
( A  o.  B
)  o.  C )
2 relco 5352 . 2  |-  Rel  ( A  o.  ( B  o.  C ) )
3 excom 1938 . . . 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 659 . . . . 5  |-  ( ( ( x C z  /\  z B w )  /\  w A y )  <->  ( x C z  /\  (
z B w  /\  w A y ) ) )
542exbii 1730 . . . 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 260 . . 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 3060 . . . . . . 7  |-  z  e. 
_V
8 vex 3060 . . . . . . 7  |-  y  e. 
_V
97, 8brco 5024 . . . . . 6  |-  ( z ( A  o.  B
) y  <->  E. w
( z B w  /\  w A y ) )
109anbi2i 705 . . . . 5  |-  ( ( x C z  /\  z ( A  o.  B ) y )  <-> 
( x C z  /\  E. w ( z B w  /\  w A y ) ) )
1110exbii 1729 . . . 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 3060 . . . . 5  |-  x  e. 
_V
1312, 8opelco 5025 . . . 4  |-  ( <.
x ,  y >.  e.  ( ( A  o.  B )  o.  C
)  <->  E. z ( x C z  /\  z
( A  o.  B
) y ) )
14 exdistr 1846 . . . 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 285 . . 3  |-  ( <.
x ,  y >.  e.  ( ( A  o.  B )  o.  C
)  <->  E. z E. w
( x C z  /\  ( z B w  /\  w A y ) ) )
16 vex 3060 . . . . . . 7  |-  w  e. 
_V
1712, 16brco 5024 . . . . . 6  |-  ( x ( B  o.  C
) w  <->  E. z
( x C z  /\  z B w ) )
1817anbi1i 706 . . . . 5  |-  ( ( x ( B  o.  C ) w  /\  w A y )  <->  ( E. z ( x C z  /\  z B w )  /\  w A y ) )
1918exbii 1729 . . . 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 5025 . . . 4  |-  ( <.
x ,  y >.  e.  ( A  o.  ( B  o.  C )
)  <->  E. w ( x ( B  o.  C
) w  /\  w A y ) )
21 19.41v 1841 . . . . 5  |-  ( E. z ( ( x C z  /\  z B w )  /\  w A y )  <->  ( E. z ( x C z  /\  z B w )  /\  w A y ) )
2221exbii 1729 . . . 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 285 . . 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 285 . 2  |-  ( <.
x ,  y >.  e.  ( ( A  o.  B )  o.  C
)  <->  <. x ,  y
>.  e.  ( A  o.  ( B  o.  C
) ) )
251, 2, 24eqrelriiv 4948 1  |-  ( ( A  o.  B )  o.  C )  =  ( A  o.  ( B  o.  C )
)
Colors of variables: wff setvar class
Syntax hints:    /\ wa 375    = wceq 1455   E.wex 1674    e. wcel 1898   <.cop 3986   class class class wbr 4416    o. ccom 4857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417  df-opab 4476  df-xp 4859  df-rel 4860  df-co 4862
This theorem is referenced by:  funcoeqres  5867  fcof1oinvd  6216  tposco  7030  mapen  7762  mapfien  7947  hashfacen  12650  relexpsucnnl  13144  relexpaddnn  13163  cofuass  15843  setccatid  16028  estrccatid  16066  frmdup3lem  16699  symggrp  17090  f1omvdco2  17138  symggen  17160  psgnunilem1  17183  gsumval3  17590  gsumzf1o  17595  gsumzmhm  17619  prds1  17891  psrass1lem  18650  pf1mpf  18989  pf1ind  18992  qtophmeo  20881  uniioombllem2  22589  uniioombllem2OLD  22590  cncombf  22663  motgrp  24637  pjsdi2i  27859  pjadj2coi  27906  pj3lem1  27908  pj3i  27910  fcoinver  28263  fcobij  28359  fcobijfs  28360  symgfcoeu  28657  derangenlem  29943  subfacp1lem5  29956  erdsze2lem2  29976  pprodcnveq  30699  cocnv  32097  ltrncoidN  33738  trlcoabs2N  34334  trlcoat  34335  trlcone  34340  cdlemg46  34347  cdlemg47  34348  ltrnco4  34351  tgrpgrplem  34361  tendoplass  34395  cdlemi2  34431  cdlemk2  34444  cdlemk4  34446  cdlemk8  34450  cdlemk45  34559  cdlemk54  34570  cdlemk55a  34571  erngdvlem3  34602  erngdvlem3-rN  34610  tendocnv  34634  dvhvaddass  34710  dvhlveclem  34721  cdlemn8  34817  dihopelvalcpre  34861  dih1dimatlem0  34941  diophrw  35646  eldioph2  35649  mendring  36103  cortrcltrcl  36377  corclrtrcl  36378  cortrclrcl  36380  cotrclrtrcl  36381  cortrclrtrcl  36382  frege131d  36401  rngccatidALTV  40264  ringccatidALTV  40327
  Copyright terms: Public domain W3C validator