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

Theorem domtr 6916
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 6871 . 2  |-  Rel  ~<_
2 vex 2793 . . . 4  |-  y  e. 
_V
32brdom 6876 . . 3  |-  ( x  ~<_  y  <->  E. g  g : x -1-1-> y )
4 vex 2793 . . . 4  |-  z  e. 
_V
54brdom 6876 . . 3  |-  ( y  ~<_  z  <->  E. f  f : y -1-1-> z )
6 eeanv 1856 . . . 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 5448 . . . . . . . 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 2793 . . . . . . . . 9  |-  f  e. 
_V
10 vex 2793 . . . . . . . . 9  |-  g  e. 
_V
119, 10coex 5218 . . . . . . . 8  |-  ( f  o.  g )  e. 
_V
12 f1eq1 5434 . . . . . . . 8  |-  ( h  =  ( f  o.  g )  ->  (
h : x -1-1-> z  <-> 
( f  o.  g
) : x -1-1-> z ) )
1311, 12spcev 2877 . . . . . . 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 6876 . . . . . 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 1669 . . . 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 4735 1  |-  ( ( A  ~<_  B  /\  B  ~<_  C )  ->  A  ~<_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1530   class class class wbr 4025    o. ccom 4695   -1-1->wf1 5254    ~<_ cdom 6863
This theorem is referenced by:  endomtr  6921  domentr  6922  undom  6952  sdomdomtr  6996  domsdomtr  6998  xpen  7026  unxpdom2  7073  sucxpdom  7074  fidomdm  7140  hartogs  7261  harword  7281  unxpwdom  7305  harcard  7613  infxpenlem  7643  indcardi  7670  fodomfi2  7689  infpwfien  7691  inffien  7692  cdadom3  7816  cdainf  7820  infcda1  7821  cdalepw  7824  unctb  7833  infcdaabs  7834  infcda  7836  infdif  7837  infdif2  7838  infxp  7843  infmap2  7846  fictb  7873  cfslb2n  7896  isfin32i  7993  fin1a2lem12  8039  hsmexlem1  8054  brdom3  8155  brdom5  8156  brdom4  8157  imadomg  8161  iundomg  8165  uniimadom  8168  ondomon  8187  unirnfdomd  8191  alephval2  8196  iunctb  8198  alephexp1  8203  alephreg  8206  cfpwsdom  8208  gchdomtri  8253  canthnum  8273  canthp1lem1  8276  canthp1  8278  pwfseqlem5  8287  pwxpndom2  8289  pwxpndom  8290  pwcdandom  8291  gchcdaidm  8292  gchxpidm  8293  gchaclem  8294  gchhar  8295  gchpwdom  8298  inar1  8399  rankcf  8401  grudomon  8441  grothac  8454  rpnnen  12507  cctop  16745  1stcfb  17173  2ndcredom  17178  2ndc1stc  17179  1stcrestlem  17180  2ndcctbss  17183  2ndcdisj2  17185  2ndcomap  17186  2ndcsep  17187  dis2ndc  17188  hauspwdom  17229  tx1stc  17346  tx2ndc  17347  met2ndci  18070  opnreen  18338  rectbntr0  18339  uniiccdif  18935  dyadmbl  18957  opnmblALT  18960  mbfimaopnlem  19012  abrexdomjm  23167  ssct  23339  xpct  23340  fnct  23343  dmct  23344  cnvct  23345  mptct  23347  mptctf  23350  sigaclci  23495  abrexdom  26416  heiborlem3  26548  ttac  27140  idomsubgmo  27525
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-id 4311  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-dom 6867
  Copyright terms: Public domain W3C validator