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

Theorem domtr 7633
Description: Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94. (Contributed by NM, 4-Jun-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
Assertion
Ref Expression
domtr  |-  ( ( A  ~<_  B  /\  B  ~<_  C )  ->  A  ~<_  C )

Proof of Theorem domtr
Dummy variables  x  y  z  f  g  h are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reldom 7587 . 2  |-  Rel  ~<_
2 vex 3083 . . . 4  |-  y  e. 
_V
32brdom 7593 . . 3  |-  ( x  ~<_  y  <->  E. g  g : x -1-1-> y )
4 vex 3083 . . . 4  |-  z  e. 
_V
54brdom 7593 . . 3  |-  ( y  ~<_  z  <->  E. f  f : y -1-1-> z )
6 eeanv 2047 . . . 4  |-  ( E. g E. f ( g : x -1-1-> y  /\  f : y
-1-1-> z )  <->  ( E. g  g : x
-1-1-> y  /\  E. f 
f : y -1-1-> z ) )
7 f1co 5805 . . . . . . . 8  |-  ( ( f : y -1-1-> z  /\  g : x
-1-1-> y )  ->  (
f  o.  g ) : x -1-1-> z )
87ancoms 454 . . . . . . 7  |-  ( ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  (
f  o.  g ) : x -1-1-> z )
9 vex 3083 . . . . . . . . 9  |-  f  e. 
_V
10 vex 3083 . . . . . . . . 9  |-  g  e. 
_V
119, 10coex 6760 . . . . . . . 8  |-  ( f  o.  g )  e. 
_V
12 f1eq1 5791 . . . . . . . 8  |-  ( h  =  ( f  o.  g )  ->  (
h : x -1-1-> z  <-> 
( f  o.  g
) : x -1-1-> z ) )
1311, 12spcev 3173 . . . . . . 7  |-  ( ( f  o.  g ) : x -1-1-> z  ->  E. h  h :
x -1-1-> z )
148, 13syl 17 . . . . . 6  |-  ( ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  E. h  h : x -1-1-> z )
154brdom 7593 . . . . . 6  |-  ( x  ~<_  z  <->  E. h  h : x -1-1-> z )
1614, 15sylibr 215 . . . . 5  |-  ( ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  x  ~<_  z )
1716exlimivv 1771 . . . 4  |-  ( E. g E. f ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  x  ~<_  z )
186, 17sylbir 216 . . 3  |-  ( ( E. g  g : x -1-1-> y  /\  E. f  f : y
-1-1-> z )  ->  x  ~<_  z )
193, 5, 18syl2anb 481 . 2  |-  ( ( x  ~<_  y  /\  y  ~<_  z )  ->  x  ~<_  z )
201, 19vtoclr 4898 1  |-  ( ( A  ~<_  B  /\  B  ~<_  C )  ->  A  ~<_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370   E.wex 1657   class class class wbr 4423    o. ccom 4857   -1-1->wf1 5598    ~<_ cdom 7579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-dom 7583
This theorem is referenced by:  endomtr  7638  domentr  7639  undom  7670  sdomdomtr  7715  domsdomtr  7717  xpen  7745  unxpdom2  7790  sucxpdom  7791  fidomdm  7863  hartogs  8069  harword  8090  unxpwdom  8114  harcard  8421  infxpenlem  8453  indcardi  8480  fodomfi2  8499  infpwfien  8501  inffien  8502  cdadom3  8626  cdainf  8630  infcda1  8631  cdalepw  8634  unctb  8643  infcdaabs  8644  infcda  8646  infdif  8647  infdif2  8648  infxp  8653  infmap2  8656  fictb  8683  cfslb2n  8706  isfin32i  8803  fin1a2lem12  8849  hsmexlem1  8864  brdom3  8964  brdom5  8965  brdom4  8966  imadomg  8970  iundomg  8974  uniimadom  8977  ondomon  8996  unirnfdomd  9000  alephval2  9005  iunctb  9007  alephexp1  9012  alephreg  9015  cfpwsdom  9017  gchdomtri  9062  canthnum  9082  canthp1lem1  9085  canthp1  9087  pwfseqlem5  9096  pwxpndom2  9098  pwxpndom  9099  pwcdandom  9100  gchcdaidm  9101  gchxpidm  9102  gchpwdom  9103  gchaclem  9111  gchhar  9112  inar1  9208  rankcf  9210  grudomon  9250  grothac  9263  rpnnen  14279  cctop  20020  1stcfb  20459  2ndcredom  20464  2ndc1stc  20465  1stcrestlem  20466  2ndcctbss  20469  2ndcdisj2  20471  2ndcomap  20472  2ndcsep  20473  dis2ndc  20474  hauspwdom  20515  tx1stc  20664  tx2ndc  20665  met2ndci  21536  opnreen  21848  rectbntr0  21849  uniiccdif  22534  dyadmbl  22557  opnmblALT  22560  mbfimaopnlem  22610  abrexdomjm  28141  ssct  28300  xpct  28301  fnct  28304  dmct  28305  cnvct  28306  fimact  28308  mptct  28309  mptctf  28312  locfinreflem  28676  sigaclci  28963  omsmeas  29164  omsmeasOLD  29165  sibfof  29182  abrexdom  32022  heiborlem3  32110  ttac  35862  idomsubgmo  36043  uzct  37378  omeiunle  38247
  Copyright terms: Public domain W3C validator