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

Theorem domtr 7374
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 7328 . 2  |-  Rel  ~<_
2 vex 2987 . . . 4  |-  y  e. 
_V
32brdom 7334 . . 3  |-  ( x  ~<_  y  <->  E. g  g : x -1-1-> y )
4 vex 2987 . . . 4  |-  z  e. 
_V
54brdom 7334 . . 3  |-  ( y  ~<_  z  <->  E. f  f : y -1-1-> z )
6 eeanv 1932 . . . 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 5627 . . . . . . . 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 2987 . . . . . . . . 9  |-  f  e. 
_V
10 vex 2987 . . . . . . . . 9  |-  g  e. 
_V
119, 10coex 6541 . . . . . . . 8  |-  ( f  o.  g )  e. 
_V
12 f1eq1 5613 . . . . . . . 8  |-  ( h  =  ( f  o.  g )  ->  (
h : x -1-1-> z  <-> 
( f  o.  g
) : x -1-1-> z ) )
1311, 12spcev 3076 . . . . . . 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 7334 . . . . . 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 1689 . . . 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 4895 1  |-  ( ( A  ~<_  B  /\  B  ~<_  C )  ->  A  ~<_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   E.wex 1586   class class class wbr 4304    o. ccom 4856   -1-1->wf1 5427    ~<_ cdom 7320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-opab 4363  df-id 4648  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-fun 5432  df-fn 5433  df-f 5434  df-f1 5435  df-dom 7324
This theorem is referenced by:  endomtr  7379  domentr  7380  undom  7411  sdomdomtr  7456  domsdomtr  7458  xpen  7486  unxpdom2  7533  sucxpdom  7534  fidomdm  7605  hartogs  7770  harword  7792  unxpwdom  7816  harcard  8160  infxpenlem  8192  indcardi  8223  fodomfi2  8242  infpwfien  8244  inffien  8245  cdadom3  8369  cdainf  8373  infcda1  8374  cdalepw  8377  unctb  8386  infcdaabs  8387  infcda  8389  infdif  8390  infdif2  8391  infxp  8396  infmap2  8399  fictb  8426  cfslb2n  8449  isfin32i  8546  fin1a2lem12  8592  hsmexlem1  8607  brdom3  8707  brdom5  8708  brdom4  8709  imadomg  8713  iundomg  8717  uniimadom  8720  ondomon  8739  unirnfdomd  8743  alephval2  8748  iunctb  8750  alephexp1  8755  alephreg  8758  cfpwsdom  8760  gchdomtri  8808  canthnum  8828  canthp1lem1  8831  canthp1  8833  pwfseqlem5  8842  pwxpndom2  8844  pwxpndom  8845  pwcdandom  8846  gchcdaidm  8847  gchxpidm  8848  gchpwdom  8849  gchaclem  8857  gchhar  8858  inar1  8954  rankcf  8956  grudomon  8996  grothac  9009  rpnnen  13521  cctop  18622  1stcfb  19061  2ndcredom  19066  2ndc1stc  19067  1stcrestlem  19068  2ndcctbss  19071  2ndcdisj2  19073  2ndcomap  19074  2ndcsep  19075  dis2ndc  19076  hauspwdom  19117  tx1stc  19235  tx2ndc  19236  met2ndci  20109  opnreen  20420  rectbntr0  20421  uniiccdif  21070  dyadmbl  21092  opnmblALT  21095  mbfimaopnlem  21145  abrexdomjm  25900  ssct  26021  xpct  26022  fnct  26025  dmct  26026  cnvct  26027  fimact  26029  mptct  26030  mptctf  26033  sigaclci  26587  sibfof  26738  abrexdom  28636  heiborlem3  28724  ttac  29397  idomsubgmo  29575
  Copyright terms: Public domain W3C validator