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

Theorem domtr 7324
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 7279 . 2
2 vex 3018 . . . 4
32brdom 7284 . . 3
4 vex 3018 . . . 4
54brdom 7284 . . 3
6 eeanv 1941 . . . 4
7 f1co 5632 . . . . . . . 8
87ancoms 441 . . . . . . 7
9 vex 3018 . . . . . . . . 9
10 vex 3018 . . . . . . . . 9
119, 10coex 6536 . . . . . . . 8
12 f1eq1 5618 . . . . . . . 8
1311, 12spcev 3104 . . . . . . 7
148, 13syl 16 . . . . . 6
154brdom 7284 . . . . . 6
1614, 15sylibr 205 . . . . 5
1716exlimivv 1663 . . . 4
186, 17sylbir 206 . . 3
193, 5, 18syl2anb 467 . 2
201, 19vtoclr 4905 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  E.wex 1565   class class class wbr 4318  o.ccom 4866  -1-1->wf1 5435   cdom 7271
This theorem is referenced by:  endomtr  7329  domentr  7330  undom  7361  sdomdomtr  7405  domsdomtr  7407  xpen  7435  unxpdom2  7482  sucxpdom  7483  fidomdm  7554  hartogs  7680  harword  7700  unxpwdom  7724  harcard  8034  infxpenlem  8066  indcardi  8093  fodomfi2  8112  infpwfien  8114  inffien  8115  cdadom3  8239  cdainf  8243  infcda1  8244  cdalepw  8247  unctb  8256  infcdaabs  8257  infcda  8259  infdif  8260  infdif2  8261  infxp  8266  infmap2  8269  fictb  8296  cfslb2n  8319  isfin32i  8416  fin1a2lem12  8462  hsmexlem1  8477  brdom3  8577  brdom5  8578  brdom4  8579  imadomg  8583  iundomg  8587  uniimadom  8590  ondomon  8609  unirnfdomd  8613  alephval2  8618  iunctb  8620  alephexp1  8625  alephreg  8628  cfpwsdom  8630  gchdomtri  8675  canthnum  8695  canthp1lem1  8698  canthp1  8700  pwfseqlem5  8709  pwxpndom2  8711  pwxpndom  8712  pwcdandom  8713  gchcdaidm  8714  gchxpidm  8715  gchpwdom  8716  gchaclem  8724  gchhar  8725  inar1  8821  rankcf  8823  grudomon  8863  grothac  8876  rpnnen  13356  cctop  18084  1stcfb  18523  2ndcredom  18528  2ndc1stc  18529  1stcrestlem  18530  2ndcctbss  18533  2ndcdisj2  18535  2ndcomap  18536  2ndcsep  18537  dis2ndc  18538  hauspwdom  18579  tx1stc  18697  tx2ndc  18698  met2ndci  19567  opnreen  19877  rectbntr0  19878  uniiccdif  20485  dyadmbl  20507  opnmblALT  20510  mbfimaopnlem  20560  abrexdomjm  25016  ssct  25139  xpct  25140  fnct  25143  dmct  25144  cnvct  25145  fimact  25147  mptct  25148  mptctf  25151  sigaclci  25755  sibfof  25900  abrexdom  27804  heiborlem3  27894  ttac  28533  idomsubgmo  28745
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554  ax-un 6382
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-ral 2764  df-rex 2765  df-rab 2768  df-v 3017  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-nul 3674  df-if 3826  df-pw 3895  df-sn 3915  df-pr 3916  df-op 3918  df-uni 4118  df-br 4319  df-opab 4377  df-id 4657  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-fun 5440  df-fn 5441  df-f 5442  df-f1 5443  df-dom 7275
  Copyright terms: Public domain W3C validator