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

Theorem domtr 7588
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

Proof of Theorem domtr
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reldom 7542 . 2
2 vex 3112 . . . 4
32brdom 7548 . . 3
4 vex 3112 . . . 4
54brdom 7548 . . 3
6 eeanv 1988 . . . 4
7 f1co 5795 . . . . . . . 8
87ancoms 453 . . . . . . 7
9 vex 3112 . . . . . . . . 9
10 vex 3112 . . . . . . . . 9
119, 10coex 6752 . . . . . . . 8
12 f1eq1 5781 . . . . . . . 8
1311, 12spcev 3201 . . . . . . 7
148, 13syl 16 . . . . . 6
154brdom 7548 . . . . . 6
1614, 15sylibr 212 . . . . 5
1716exlimivv 1723 . . . 4
186, 17sylbir 213 . . 3
193, 5, 18syl2anb 479 . 2
201, 19vtoclr 5049 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  E.wex 1612   class class class wbr 4452  o.ccom 5008  -1-1->wf1 5590   cdom 7534
This theorem is referenced by:  endomtr  7593  domentr  7594  undom  7625  sdomdomtr  7670  domsdomtr  7672  xpen  7700  unxpdom2  7748  sucxpdom  7749  fidomdm  7822  hartogs  7990  harword  8012  unxpwdom  8036  harcard  8380  infxpenlem  8412  indcardi  8443  fodomfi2  8462  infpwfien  8464  inffien  8465  cdadom3  8589  cdainf  8593  infcda1  8594  cdalepw  8597  unctb  8606  infcdaabs  8607  infcda  8609  infdif  8610  infdif2  8611  infxp  8616  infmap2  8619  fictb  8646  cfslb2n  8669  isfin32i  8766  fin1a2lem12  8812  hsmexlem1  8827  brdom3  8927  brdom5  8928  brdom4  8929  imadomg  8933  iundomg  8937  uniimadom  8940  ondomon  8959  unirnfdomd  8963  alephval2  8968  iunctb  8970  alephexp1  8975  alephreg  8978  cfpwsdom  8980  gchdomtri  9028  canthnum  9048  canthp1lem1  9051  canthp1  9053  pwfseqlem5  9062  pwxpndom2  9064  pwxpndom  9065  pwcdandom  9066  gchcdaidm  9067  gchxpidm  9068  gchpwdom  9069  gchaclem  9077  gchhar  9078  inar1  9174  rankcf  9176  grudomon  9216  grothac  9229  rpnnen  13960  cctop  19507  1stcfb  19946  2ndcredom  19951  2ndc1stc  19952  1stcrestlem  19953  2ndcctbss  19956  2ndcdisj2  19958  2ndcomap  19959  2ndcsep  19960  dis2ndc  19961  hauspwdom  20002  tx1stc  20151  tx2ndc  20152  met2ndci  21025  opnreen  21336  rectbntr0  21337  uniiccdif  21987  dyadmbl  22009  opnmblALT  22012  mbfimaopnlem  22062  abrexdomjm  27405  ssct  27532  xpct  27533  fnct  27536  dmct  27537  cnvct  27538  fimact  27540  mptct  27541  mptctf  27544  locfinreflem  27843  sigaclci  28132  sibfof  28282  abrexdom  30221  heiborlem3  30309  ttac  30978  idomsubgmo  31155
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  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 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-dom 7538
  Copyright terms: Public domain W3C validator