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

Theorem domtr 7057
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 7012 . 2  |-  Rel  ~<_
2 vex 2876 . . . 4  |-  y  e. 
_V
32brdom 7017 . . 3  |-  ( x  ~<_  y  <->  E. g  g : x -1-1-> y )
4 vex 2876 . . . 4  |-  z  e. 
_V
54brdom 7017 . . 3  |-  ( y  ~<_  z  <->  E. f  f : y -1-1-> z )
6 eeanv 1924 . . . 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 5552 . . . . . . . 8  |-  ( ( f : y -1-1-> z  /\  g : x
-1-1-> y )  ->  (
f  o.  g ) : x -1-1-> z )
87ancoms 439 . . . . . . 7  |-  ( ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  (
f  o.  g ) : x -1-1-> z )
9 vex 2876 . . . . . . . . 9  |-  f  e. 
_V
10 vex 2876 . . . . . . . . 9  |-  g  e. 
_V
119, 10coex 5319 . . . . . . . 8  |-  ( f  o.  g )  e. 
_V
12 f1eq1 5538 . . . . . . . 8  |-  ( h  =  ( f  o.  g )  ->  (
h : x -1-1-> z  <-> 
( f  o.  g
) : x -1-1-> z ) )
1311, 12spcev 2960 . . . . . . 7  |-  ( ( f  o.  g ) : x -1-1-> z  ->  E. h  h :
x -1-1-> z )
148, 13syl 15 . . . . . 6  |-  ( ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  E. h  h : x -1-1-> z )
154brdom 7017 . . . . . 6  |-  ( x  ~<_  z  <->  E. h  h : x -1-1-> z )
1614, 15sylibr 203 . . . . 5  |-  ( ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  x  ~<_  z )
1716exlimivv 1640 . . . 4  |-  ( E. g E. f ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  x  ~<_  z )
186, 17sylbir 204 . . 3  |-  ( ( E. g  g : x -1-1-> y  /\  E. f  f : y
-1-1-> z )  ->  x  ~<_  z )
193, 5, 18syl2anb 465 . 2  |-  ( ( x  ~<_  y  /\  y  ~<_  z )  ->  x  ~<_  z )
201, 19vtoclr 4836 1  |-  ( ( A  ~<_  B  /\  B  ~<_  C )  ->  A  ~<_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1546   class class class wbr 4125    o. ccom 4796   -1-1->wf1 5355    ~<_ cdom 7004
This theorem is referenced by:  endomtr  7062  domentr  7063  undom  7093  sdomdomtr  7137  domsdomtr  7139  xpen  7167  unxpdom2  7214  sucxpdom  7215  fidomdm  7285  hartogs  7406  harword  7426  unxpwdom  7450  harcard  7758  infxpenlem  7788  indcardi  7815  fodomfi2  7834  infpwfien  7836  inffien  7837  cdadom3  7961  cdainf  7965  infcda1  7966  cdalepw  7969  unctb  7978  infcdaabs  7979  infcda  7981  infdif  7982  infdif2  7983  infxp  7988  infmap2  7991  fictb  8018  cfslb2n  8041  isfin32i  8138  fin1a2lem12  8184  hsmexlem1  8199  brdom3  8300  brdom5  8301  brdom4  8302  imadomg  8306  iundomg  8310  uniimadom  8313  ondomon  8332  unirnfdomd  8336  alephval2  8341  iunctb  8343  alephexp1  8348  alephreg  8351  cfpwsdom  8353  gchdomtri  8398  canthnum  8418  canthp1lem1  8421  canthp1  8423  pwfseqlem5  8432  pwxpndom2  8434  pwxpndom  8435  pwcdandom  8436  gchcdaidm  8437  gchxpidm  8438  gchaclem  8439  gchhar  8440  gchpwdom  8443  inar1  8544  rankcf  8546  grudomon  8586  grothac  8599  rpnnen  12713  cctop  16960  1stcfb  17388  2ndcredom  17393  2ndc1stc  17394  1stcrestlem  17395  2ndcctbss  17398  2ndcdisj2  17400  2ndcomap  17401  2ndcsep  17402  dis2ndc  17403  hauspwdom  17444  tx1stc  17561  tx2ndc  17562  met2ndci  18281  opnreen  18550  rectbntr0  18551  uniiccdif  19148  dyadmbl  19170  opnmblALT  19173  mbfimaopnlem  19225  abrexdomjm  23383  ssct  23504  xpct  23505  fnct  23508  dmct  23509  cnvct  23510  mptct  23512  mptctf  23515  sigaclci  23980  abrexdom  25912  heiborlem3  26043  ttac  26635  idomsubgmo  27020
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316  ax-un 4615
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-pw 3716  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-opab 4180  df-id 4412  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-fun 5360  df-fn 5361  df-f 5362  df-f1 5363  df-dom 7008
  Copyright terms: Public domain W3C validator