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

Theorem domtr 7629
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 7583 . 2  |-  Rel  ~<_
2 vex 3090 . . . 4  |-  y  e. 
_V
32brdom 7589 . . 3  |-  ( x  ~<_  y  <->  E. g  g : x -1-1-> y )
4 vex 3090 . . . 4  |-  z  e. 
_V
54brdom 7589 . . 3  |-  ( y  ~<_  z  <->  E. f  f : y -1-1-> z )
6 eeanv 2045 . . . 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 3090 . . . . . . . . 9  |-  f  e. 
_V
10 vex 3090 . . . . . . . . 9  |-  g  e. 
_V
119, 10coex 6759 . . . . . . . 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 3179 . . . . . . 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 7589 . . . . . 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 1770 . . . 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 4899 1  |-  ( ( A  ~<_  B  /\  B  ~<_  C )  ->  A  ~<_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370   E.wex 1659   class class class wbr 4426    o. ccom 4858   -1-1->wf1 5598    ~<_ cdom 7575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-dom 7579
This theorem is referenced by:  endomtr  7634  domentr  7635  undom  7666  sdomdomtr  7711  domsdomtr  7713  xpen  7741  unxpdom2  7786  sucxpdom  7787  fidomdm  7859  hartogs  8059  harword  8080  unxpwdom  8104  harcard  8411  infxpenlem  8443  indcardi  8470  fodomfi2  8489  infpwfien  8491  inffien  8492  cdadom3  8616  cdainf  8620  infcda1  8621  cdalepw  8624  unctb  8633  infcdaabs  8634  infcda  8636  infdif  8637  infdif2  8638  infxp  8643  infmap2  8646  fictb  8673  cfslb2n  8696  isfin32i  8793  fin1a2lem12  8839  hsmexlem1  8854  brdom3  8954  brdom5  8955  brdom4  8956  imadomg  8960  iundomg  8964  uniimadom  8967  ondomon  8986  unirnfdomd  8990  alephval2  8995  iunctb  8997  alephexp1  9002  alephreg  9005  cfpwsdom  9007  gchdomtri  9053  canthnum  9073  canthp1lem1  9076  canthp1  9078  pwfseqlem5  9087  pwxpndom2  9089  pwxpndom  9090  pwcdandom  9091  gchcdaidm  9092  gchxpidm  9093  gchpwdom  9094  gchaclem  9102  gchhar  9103  inar1  9199  rankcf  9201  grudomon  9241  grothac  9254  rpnnen  14257  cctop  19952  1stcfb  20391  2ndcredom  20396  2ndc1stc  20397  1stcrestlem  20398  2ndcctbss  20401  2ndcdisj2  20403  2ndcomap  20404  2ndcsep  20405  dis2ndc  20406  hauspwdom  20447  tx1stc  20596  tx2ndc  20597  met2ndci  21468  opnreen  21760  rectbntr0  21761  uniiccdif  22412  dyadmbl  22435  opnmblALT  22438  mbfimaopnlem  22488  abrexdomjm  27977  ssct  28136  xpct  28137  fnct  28140  dmct  28141  cnvct  28142  fimact  28144  mptct  28145  mptctf  28148  locfinreflem  28506  sigaclci  28793  omsmeas  28984  sibfof  29001  abrexdom  31761  heiborlem3  31849  ttac  35597  idomsubgmo  35771  uzct  37046  omeiunle  37847
  Copyright terms: Public domain W3C validator