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

Theorem domtr 6930
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 6885 . 2  |-  Rel  ~<_
2 vex 2804 . . . 4  |-  y  e. 
_V
32brdom 6890 . . 3  |-  ( x  ~<_  y  <->  E. g  g : x -1-1-> y )
4 vex 2804 . . . 4  |-  z  e. 
_V
54brdom 6890 . . 3  |-  ( y  ~<_  z  <->  E. f  f : y -1-1-> z )
6 eeanv 1866 . . . 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 5462 . . . . . . . 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 2804 . . . . . . . . 9  |-  f  e. 
_V
10 vex 2804 . . . . . . . . 9  |-  g  e. 
_V
119, 10coex 5232 . . . . . . . 8  |-  ( f  o.  g )  e. 
_V
12 f1eq1 5448 . . . . . . . 8  |-  ( h  =  ( f  o.  g )  ->  (
h : x -1-1-> z  <-> 
( f  o.  g
) : x -1-1-> z ) )
1311, 12spcev 2888 . . . . . . 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 6890 . . . . . 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 1625 . . . 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 4749 1  |-  ( ( A  ~<_  B  /\  B  ~<_  C )  ->  A  ~<_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1531   class class class wbr 4039    o. ccom 4709   -1-1->wf1 5268    ~<_ cdom 6877
This theorem is referenced by:  endomtr  6935  domentr  6936  undom  6966  sdomdomtr  7010  domsdomtr  7012  xpen  7040  unxpdom2  7087  sucxpdom  7088  fidomdm  7154  hartogs  7275  harword  7295  unxpwdom  7319  harcard  7627  infxpenlem  7657  indcardi  7684  fodomfi2  7703  infpwfien  7705  inffien  7706  cdadom3  7830  cdainf  7834  infcda1  7835  cdalepw  7838  unctb  7847  infcdaabs  7848  infcda  7850  infdif  7851  infdif2  7852  infxp  7857  infmap2  7860  fictb  7887  cfslb2n  7910  isfin32i  8007  fin1a2lem12  8053  hsmexlem1  8068  brdom3  8169  brdom5  8170  brdom4  8171  imadomg  8175  iundomg  8179  uniimadom  8182  ondomon  8201  unirnfdomd  8205  alephval2  8210  iunctb  8212  alephexp1  8217  alephreg  8220  cfpwsdom  8222  gchdomtri  8267  canthnum  8287  canthp1lem1  8290  canthp1  8292  pwfseqlem5  8301  pwxpndom2  8303  pwxpndom  8304  pwcdandom  8305  gchcdaidm  8306  gchxpidm  8307  gchaclem  8308  gchhar  8309  gchpwdom  8312  inar1  8413  rankcf  8415  grudomon  8455  grothac  8468  rpnnen  12521  cctop  16759  1stcfb  17187  2ndcredom  17192  2ndc1stc  17193  1stcrestlem  17194  2ndcctbss  17197  2ndcdisj2  17199  2ndcomap  17200  2ndcsep  17201  dis2ndc  17202  hauspwdom  17243  tx1stc  17360  tx2ndc  17361  met2ndci  18084  opnreen  18352  rectbntr0  18353  uniiccdif  18949  dyadmbl  18971  opnmblALT  18974  mbfimaopnlem  19026  abrexdomjm  23181  ssct  23352  xpct  23353  fnct  23356  dmct  23357  cnvct  23358  mptct  23360  mptctf  23363  sigaclci  23508  abrexdom  26508  heiborlem3  26640  ttac  27232  idomsubgmo  27617
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-dom 6881
  Copyright terms: Public domain W3C validator