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

Theorem domtr 7123
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 7078 . 2  |-  Rel  ~<_
2 vex 2923 . . . 4  |-  y  e. 
_V
32brdom 7083 . . 3  |-  ( x  ~<_  y  <->  E. g  g : x -1-1-> y )
4 vex 2923 . . . 4  |-  z  e. 
_V
54brdom 7083 . . 3  |-  ( y  ~<_  z  <->  E. f  f : y -1-1-> z )
6 eeanv 1933 . . . 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 5611 . . . . . . . 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 2923 . . . . . . . . 9  |-  f  e. 
_V
10 vex 2923 . . . . . . . . 9  |-  g  e. 
_V
119, 10coex 5376 . . . . . . . 8  |-  ( f  o.  g )  e. 
_V
12 f1eq1 5597 . . . . . . . 8  |-  ( h  =  ( f  o.  g )  ->  (
h : x -1-1-> z  <-> 
( f  o.  g
) : x -1-1-> z ) )
1311, 12spcev 3007 . . . . . . 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 7083 . . . . . 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 4885 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 4176    o. ccom 4845   -1-1->wf1 5414    ~<_ cdom 7070
This theorem is referenced by:  endomtr  7128  domentr  7129  undom  7159  sdomdomtr  7203  domsdomtr  7205  xpen  7233  unxpdom2  7280  sucxpdom  7281  fidomdm  7351  hartogs  7473  harword  7493  unxpwdom  7517  harcard  7825  infxpenlem  7855  indcardi  7882  fodomfi2  7901  infpwfien  7903  inffien  7904  cdadom3  8028  cdainf  8032  infcda1  8033  cdalepw  8036  unctb  8045  infcdaabs  8046  infcda  8048  infdif  8049  infdif2  8050  infxp  8055  infmap2  8058  fictb  8085  cfslb2n  8108  isfin32i  8205  fin1a2lem12  8251  hsmexlem1  8266  brdom3  8366  brdom5  8367  brdom4  8368  imadomg  8372  iundomg  8376  uniimadom  8379  ondomon  8398  unirnfdomd  8402  alephval2  8407  iunctb  8409  alephexp1  8414  alephreg  8417  cfpwsdom  8419  gchdomtri  8464  canthnum  8484  canthp1lem1  8487  canthp1  8489  pwfseqlem5  8498  pwxpndom2  8500  pwxpndom  8501  pwcdandom  8502  gchcdaidm  8503  gchxpidm  8504  gchaclem  8505  gchhar  8506  gchpwdom  8509  inar1  8610  rankcf  8612  grudomon  8652  grothac  8665  rpnnen  12785  cctop  17029  1stcfb  17465  2ndcredom  17470  2ndc1stc  17471  1stcrestlem  17472  2ndcctbss  17475  2ndcdisj2  17477  2ndcomap  17478  2ndcsep  17479  dis2ndc  17480  hauspwdom  17521  tx1stc  17639  tx2ndc  17640  met2ndci  18509  opnreen  18819  rectbntr0  18820  uniiccdif  19427  dyadmbl  19449  opnmblALT  19452  mbfimaopnlem  19504  abrexdomjm  23945  ssct  24058  xpct  24059  fnct  24062  dmct  24063  cnvct  24064  mptct  24066  mptctf  24069  sigaclci  24472  sibfof  24611  abrexdom  26326  heiborlem3  26416  ttac  27001  idomsubgmo  27386
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 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664
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 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-id 4462  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-dom 7074
  Copyright terms: Public domain W3C validator