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

Theorem domtr 7653
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 7606 . 2  |-  Rel  ~<_
2 vex 3060 . . . 4  |-  y  e. 
_V
32brdom 7612 . . 3  |-  ( x  ~<_  y  <->  E. g  g : x -1-1-> y )
4 vex 3060 . . . 4  |-  z  e. 
_V
54brdom 7612 . . 3  |-  ( y  ~<_  z  <->  E. f  f : y -1-1-> z )
6 eeanv 2089 . . . 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 5815 . . . . . . . 8  |-  ( ( f : y -1-1-> z  /\  g : x
-1-1-> y )  ->  (
f  o.  g ) : x -1-1-> z )
87ancoms 459 . . . . . . 7  |-  ( ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  (
f  o.  g ) : x -1-1-> z )
9 vex 3060 . . . . . . . . 9  |-  f  e. 
_V
10 vex 3060 . . . . . . . . 9  |-  g  e. 
_V
119, 10coex 6777 . . . . . . . 8  |-  ( f  o.  g )  e. 
_V
12 f1eq1 5801 . . . . . . . 8  |-  ( h  =  ( f  o.  g )  ->  (
h : x -1-1-> z  <-> 
( f  o.  g
) : x -1-1-> z ) )
1311, 12spcev 3153 . . . . . . 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 7612 . . . . . 6  |-  ( x  ~<_  z  <->  E. h  h : x -1-1-> z )
1614, 15sylibr 217 . . . . 5  |-  ( ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  x  ~<_  z )
1716exlimivv 1789 . . . 4  |-  ( E. g E. f ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  x  ~<_  z )
186, 17sylbir 218 . . 3  |-  ( ( E. g  g : x -1-1-> y  /\  E. f  f : y
-1-1-> z )  ->  x  ~<_  z )
193, 5, 18syl2anb 486 . 2  |-  ( ( x  ~<_  y  /\  y  ~<_  z )  ->  x  ~<_  z )
201, 19vtoclr 4901 1  |-  ( ( A  ~<_  B  /\  B  ~<_  C )  ->  A  ~<_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375   E.wex 1674   class class class wbr 4418    o. ccom 4860   -1-1->wf1 5602    ~<_ cdom 7598
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-dom 7602
This theorem is referenced by:  endomtr  7658  domentr  7659  ssct  7684  undom  7691  sdomdomtr  7736  domsdomtr  7738  xpen  7766  unxpdom2  7811  sucxpdom  7812  fidomdm  7884  hartogs  8090  harword  8111  unxpwdom  8135  harcard  8443  infxpenlem  8475  xpct  8478  indcardi  8503  fodomfi2  8522  infpwfien  8524  inffien  8525  cdadom3  8649  cdainf  8653  infcda1  8654  cdalepw  8657  unctb  8666  infcdaabs  8667  infcda  8669  infdif  8670  infdif2  8671  infxp  8676  infmap2  8679  fictb  8706  cfslb2n  8729  isfin32i  8826  fin1a2lem12  8872  hsmexlem1  8887  brdom3  8987  brdom5  8988  brdom4  8989  imadomg  8993  iundomg  8997  uniimadom  9000  ondomon  9019  unirnfdomd  9023  alephval2  9028  iunctb  9030  alephexp1  9035  alephreg  9038  cfpwsdom  9040  gchdomtri  9085  canthnum  9105  canthp1lem1  9108  canthp1  9110  pwfseqlem5  9119  pwxpndom2  9121  pwxpndom  9122  pwcdandom  9123  gchcdaidm  9124  gchxpidm  9125  gchpwdom  9126  gchaclem  9134  gchhar  9135  inar1  9231  rankcf  9233  grudomon  9273  grothac  9286  rpnnen  14334  cctop  20076  1stcfb  20515  2ndcredom  20520  2ndc1stc  20521  1stcrestlem  20522  2ndcctbss  20525  2ndcdisj2  20527  2ndcomap  20528  2ndcsep  20529  dis2ndc  20530  hauspwdom  20571  tx1stc  20720  tx2ndc  20721  met2ndci  21592  opnreen  21904  rectbntr0  21905  uniiccdif  22591  dyadmbl  22614  opnmblALT  22617  mbfimaopnlem  22667  abrexdomjm  28197  fnct  28349  dmct  28350  cnvct  28351  fimact  28353  mptct  28354  mptctf  28357  locfinreflem  28718  sigaclci  29005  omsmeas  29205  omsmeasOLD  29206  sibfof  29223  abrexdom  32103  heiborlem3  32191  ttac  35937  idomsubgmo  36118  uzct  37443  omeiunle  38446
  Copyright terms: Public domain W3C validator