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

Theorem domtr 7096
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 7051 . 2  |-  Rel  ~<_
2 vex 2902 . . . 4  |-  y  e. 
_V
32brdom 7056 . . 3  |-  ( x  ~<_  y  <->  E. g  g : x -1-1-> y )
4 vex 2902 . . . 4  |-  z  e. 
_V
54brdom 7056 . . 3  |-  ( y  ~<_  z  <->  E. f  f : y -1-1-> z )
6 eeanv 1926 . . . 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 5588 . . . . . . . 8  |-  ( ( f : y -1-1-> z  /\  g : x
-1-1-> y )  ->  (
f  o.  g ) : x -1-1-> z )
87ancoms 440 . . . . . . 7  |-  ( ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  (
f  o.  g ) : x -1-1-> z )
9 vex 2902 . . . . . . . . 9  |-  f  e. 
_V
10 vex 2902 . . . . . . . . 9  |-  g  e. 
_V
119, 10coex 5353 . . . . . . . 8  |-  ( f  o.  g )  e. 
_V
12 f1eq1 5574 . . . . . . . 8  |-  ( h  =  ( f  o.  g )  ->  (
h : x -1-1-> z  <-> 
( f  o.  g
) : x -1-1-> z ) )
1311, 12spcev 2986 . . . . . . 7  |-  ( ( f  o.  g ) : x -1-1-> z  ->  E. h  h :
x -1-1-> z )
148, 13syl 16 . . . . . 6  |-  ( ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  E. h  h : x -1-1-> z )
154brdom 7056 . . . . . 6  |-  ( x  ~<_  z  <->  E. h  h : x -1-1-> z )
1614, 15sylibr 204 . . . . 5  |-  ( ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  x  ~<_  z )
1716exlimivv 1642 . . . 4  |-  ( E. g E. f ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  x  ~<_  z )
186, 17sylbir 205 . . 3  |-  ( ( E. g  g : x -1-1-> y  /\  E. f  f : y
-1-1-> z )  ->  x  ~<_  z )
193, 5, 18syl2anb 466 . 2  |-  ( ( x  ~<_  y  /\  y  ~<_  z )  ->  x  ~<_  z )
201, 19vtoclr 4862 1  |-  ( ( A  ~<_  B  /\  B  ~<_  C )  ->  A  ~<_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   E.wex 1547   class class class wbr 4153    o. ccom 4822   -1-1->wf1 5391    ~<_ cdom 7043
This theorem is referenced by:  endomtr  7101  domentr  7102  undom  7132  sdomdomtr  7176  domsdomtr  7178  xpen  7206  unxpdom2  7253  sucxpdom  7254  fidomdm  7324  hartogs  7446  harword  7466  unxpwdom  7490  harcard  7798  infxpenlem  7828  indcardi  7855  fodomfi2  7874  infpwfien  7876  inffien  7877  cdadom3  8001  cdainf  8005  infcda1  8006  cdalepw  8009  unctb  8018  infcdaabs  8019  infcda  8021  infdif  8022  infdif2  8023  infxp  8028  infmap2  8031  fictb  8058  cfslb2n  8081  isfin32i  8178  fin1a2lem12  8224  hsmexlem1  8239  brdom3  8339  brdom5  8340  brdom4  8341  imadomg  8345  iundomg  8349  uniimadom  8352  ondomon  8371  unirnfdomd  8375  alephval2  8380  iunctb  8382  alephexp1  8387  alephreg  8390  cfpwsdom  8392  gchdomtri  8437  canthnum  8457  canthp1lem1  8460  canthp1  8462  pwfseqlem5  8471  pwxpndom2  8473  pwxpndom  8474  pwcdandom  8475  gchcdaidm  8476  gchxpidm  8477  gchaclem  8478  gchhar  8479  gchpwdom  8482  inar1  8583  rankcf  8585  grudomon  8625  grothac  8638  rpnnen  12753  cctop  16993  1stcfb  17429  2ndcredom  17434  2ndc1stc  17435  1stcrestlem  17436  2ndcctbss  17439  2ndcdisj2  17441  2ndcomap  17442  2ndcsep  17443  dis2ndc  17444  hauspwdom  17485  tx1stc  17603  tx2ndc  17604  met2ndci  18442  opnreen  18733  rectbntr0  18734  uniiccdif  19337  dyadmbl  19359  opnmblALT  19362  mbfimaopnlem  19414  abrexdomjm  23832  ssct  23942  xpct  23943  fnct  23946  dmct  23947  cnvct  23948  mptct  23950  mptctf  23953  sigaclci  24311  abrexdom  26123  heiborlem3  26213  ttac  26798  idomsubgmo  27183
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-opab 4208  df-id 4439  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-dom 7047
  Copyright terms: Public domain W3C validator