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

Theorem domtr 7587
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 7541 . 2  |-  Rel  ~<_
2 vex 3112 . . . 4  |-  y  e. 
_V
32brdom 7547 . . 3  |-  ( x  ~<_  y  <->  E. g  g : x -1-1-> y )
4 vex 3112 . . . 4  |-  z  e. 
_V
54brdom 7547 . . 3  |-  ( y  ~<_  z  <->  E. f  f : y -1-1-> z )
6 eeanv 1989 . . . 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 5796 . . . . . . . 8  |-  ( ( f : y -1-1-> z  /\  g : x
-1-1-> y )  ->  (
f  o.  g ) : x -1-1-> z )
87ancoms 453 . . . . . . 7  |-  ( ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  (
f  o.  g ) : x -1-1-> z )
9 vex 3112 . . . . . . . . 9  |-  f  e. 
_V
10 vex 3112 . . . . . . . . 9  |-  g  e. 
_V
119, 10coex 6751 . . . . . . . 8  |-  ( f  o.  g )  e. 
_V
12 f1eq1 5782 . . . . . . . 8  |-  ( h  =  ( f  o.  g )  ->  (
h : x -1-1-> z  <-> 
( f  o.  g
) : x -1-1-> z ) )
1311, 12spcev 3201 . . . . . . 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 7547 . . . . . 6  |-  ( x  ~<_  z  <->  E. h  h : x -1-1-> z )
1614, 15sylibr 212 . . . . 5  |-  ( ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  x  ~<_  z )
1716exlimivv 1724 . . . 4  |-  ( E. g E. f ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  x  ~<_  z )
186, 17sylbir 213 . . 3  |-  ( ( E. g  g : x -1-1-> y  /\  E. f  f : y
-1-1-> z )  ->  x  ~<_  z )
193, 5, 18syl2anb 479 . 2  |-  ( ( x  ~<_  y  /\  y  ~<_  z )  ->  x  ~<_  z )
201, 19vtoclr 5053 1  |-  ( ( A  ~<_  B  /\  B  ~<_  C )  ->  A  ~<_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   E.wex 1613   class class class wbr 4456    o. ccom 5012   -1-1->wf1 5591    ~<_ cdom 7533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-dom 7537
This theorem is referenced by:  endomtr  7592  domentr  7593  undom  7624  sdomdomtr  7669  domsdomtr  7671  xpen  7699  unxpdom2  7747  sucxpdom  7748  fidomdm  7820  hartogs  7987  harword  8009  unxpwdom  8033  harcard  8376  infxpenlem  8408  indcardi  8439  fodomfi2  8458  infpwfien  8460  inffien  8461  cdadom3  8585  cdainf  8589  infcda1  8590  cdalepw  8593  unctb  8602  infcdaabs  8603  infcda  8605  infdif  8606  infdif2  8607  infxp  8612  infmap2  8615  fictb  8642  cfslb2n  8665  isfin32i  8762  fin1a2lem12  8808  hsmexlem1  8823  brdom3  8923  brdom5  8924  brdom4  8925  imadomg  8929  iundomg  8933  uniimadom  8936  ondomon  8955  unirnfdomd  8959  alephval2  8964  iunctb  8966  alephexp1  8971  alephreg  8974  cfpwsdom  8976  gchdomtri  9024  canthnum  9044  canthp1lem1  9047  canthp1  9049  pwfseqlem5  9058  pwxpndom2  9060  pwxpndom  9061  pwcdandom  9062  gchcdaidm  9063  gchxpidm  9064  gchpwdom  9065  gchaclem  9073  gchhar  9074  inar1  9170  rankcf  9172  grudomon  9212  grothac  9225  rpnnen  13971  cctop  19633  1stcfb  20071  2ndcredom  20076  2ndc1stc  20077  1stcrestlem  20078  2ndcctbss  20081  2ndcdisj2  20083  2ndcomap  20084  2ndcsep  20085  dis2ndc  20086  hauspwdom  20127  tx1stc  20276  tx2ndc  20277  met2ndci  21150  opnreen  21461  rectbntr0  21462  uniiccdif  22112  dyadmbl  22134  opnmblALT  22137  mbfimaopnlem  22187  abrexdomjm  27532  ssct  27682  xpct  27683  fnct  27686  dmct  27687  cnvct  27688  fimact  27690  mptct  27691  mptctf  27694  locfinreflem  27996  sigaclci  28293  sibfof  28457  abrexdom  30383  heiborlem3  30471  ttac  31140  idomsubgmo  31317
  Copyright terms: Public domain W3C validator