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

Theorem domtr 6882
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
StepHypRef Expression
1 reldom 6837 . 2  |-  Rel  ~<_
2 vex 2766 . . . 4  |-  y  e. 
_V
32brdom 6842 . . 3  |-  ( x  ~<_  y  <->  E. g  g : x -1-1-> y )
4 vex 2766 . . . 4  |-  z  e. 
_V
54brdom 6842 . . 3  |-  ( y  ~<_  z  <->  E. f  f : y -1-1-> z )
6 eeanv 2058 . . . 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 5384 . . . . . . . 8  |-  ( ( f : y -1-1-> z  /\  g : x
-1-1-> y )  ->  (
f  o.  g ) : x -1-1-> z )
87ancoms 441 . . . . . . 7  |-  ( ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  (
f  o.  g ) : x -1-1-> z )
9 vex 2766 . . . . . . . . 9  |-  f  e. 
_V
10 vex 2766 . . . . . . . . 9  |-  g  e. 
_V
119, 10coex 5203 . . . . . . . 8  |-  ( f  o.  g )  e. 
_V
12 f1eq1 5370 . . . . . . . 8  |-  ( h  =  ( f  o.  g )  ->  (
h : x -1-1-> z  <-> 
( f  o.  g
) : x -1-1-> z ) )
1311, 12cla4ev 2850 . . . . . . 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 6842 . . . . . 6  |-  ( x  ~<_  z  <->  E. h  h : x -1-1-> z )
1614, 15sylibr 205 . . . . 5  |-  ( ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  x  ~<_  z )
1716exlimivv 2026 . . . 4  |-  ( E. g E. f ( g : x -1-1-> y  /\  f : y
-1-1-> z )  ->  x  ~<_  z )
186, 17sylbir 206 . . 3  |-  ( ( E. g  g : x -1-1-> y  /\  E. f  f : y
-1-1-> z )  ->  x  ~<_  z )
193, 5, 18syl2anb 467 . 2  |-  ( ( x  ~<_  y  /\  y  ~<_  z )  ->  x  ~<_  z )
201, 19vtoclr 4721 1  |-  ( ( A  ~<_  B  /\  B  ~<_  C )  ->  A  ~<_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360   E.wex 1537   class class class wbr 3997    o. ccom 4665   -1-1->wf1 4670    ~<_ cdom 6829
This theorem is referenced by:  endomtr  6887  domentr  6888  undom  6918  sdomdomtr  6962  domsdomtr  6964  xpen  6992  unxpdom2  7039  sucxpdom  7040  fidomdm  7106  hartogs  7227  harword  7247  unxpwdom  7271  harcard  7579  infxpenlem  7609  indcardi  7636  fodomfi2  7655  infpwfien  7657  inffien  7658  cdadom3  7782  cdainf  7786  infcda1  7787  cdalepw  7790  unctb  7799  infcdaabs  7800  infcda  7802  infdif  7803  infdif2  7804  infxp  7809  infmap2  7812  fictb  7839  cfslb2n  7862  isfin32i  7959  fin1a2lem12  8005  hsmexlem1  8020  brdom3  8121  brdom5  8122  brdom4  8123  imadomg  8127  iundomg  8131  uniimadom  8134  ondomon  8153  unirnfdomd  8157  alephval2  8162  iunctb  8164  alephexp1  8169  alephreg  8172  cfpwsdom  8174  gchdomtri  8219  canthnum  8239  canthp1lem1  8242  canthp1  8244  pwfseqlem5  8253  pwxpndom2  8255  pwxpndom  8256  pwcdandom  8257  gchcdaidm  8258  gchxpidm  8259  gchaclem  8260  gchhar  8261  gchpwdom  8264  inar1  8365  rankcf  8367  grudomon  8407  grothac  8420  rpnnen  12468  cctop  16706  1stcfb  17134  2ndcredom  17139  2ndc1stc  17140  1stcrestlem  17141  2ndcctbss  17144  2ndcdisj2  17146  2ndcomap  17147  2ndcsep  17148  dis2ndc  17149  hauspwdom  17190  tx1stc  17307  tx2ndc  17308  met2ndci  18031  opnreen  18299  rectbntr0  18300  uniiccdif  18896  dyadmbl  18918  opnmblALT  18921  mbfimaopnlem  18973  abrexdom  25773  heiborlem3  25905  ttac  26497  idomsubgmo  26882
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pow 4160  ax-pr 4186  ax-un 4484
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-rab 2527  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-pw 3601  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-br 3998  df-opab 4052  df-id 4281  df-xp 4675  df-rel 4676  df-cnv 4677  df-co 4678  df-dm 4679  df-rn 4680  df-fun 4683  df-fn 4684  df-f 4685  df-f1 4686  df-dom 6833
  Copyright terms: Public domain W3C validator