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

Theorem domtr 9047
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 8991 . 2 Rel ≼
2 vex 3484 . . . 4 𝑦 ∈ V
32brdom 9001 . . 3 (𝑥𝑦 ↔ ∃𝑔 𝑔:𝑥1-1𝑦)
4 vex 3484 . . . 4 𝑧 ∈ V
54brdom 9001 . . 3 (𝑦𝑧 ↔ ∃𝑓 𝑓:𝑦1-1𝑧)
6 exdistrv 1955 . . . 4 (∃𝑔𝑓(𝑔:𝑥1-1𝑦𝑓:𝑦1-1𝑧) ↔ (∃𝑔 𝑔:𝑥1-1𝑦 ∧ ∃𝑓 𝑓:𝑦1-1𝑧))
7 f1co 6815 . . . . . . . 8 ((𝑓:𝑦1-1𝑧𝑔:𝑥1-1𝑦) → (𝑓𝑔):𝑥1-1𝑧)
87ancoms 458 . . . . . . 7 ((𝑔:𝑥1-1𝑦𝑓:𝑦1-1𝑧) → (𝑓𝑔):𝑥1-1𝑧)
9 vex 3484 . . . . . . . . 9 𝑓 ∈ V
10 vex 3484 . . . . . . . . 9 𝑔 ∈ V
119, 10coex 7952 . . . . . . . 8 (𝑓𝑔) ∈ V
12 f1eq1 6799 . . . . . . . 8 ( = (𝑓𝑔) → (:𝑥1-1𝑧 ↔ (𝑓𝑔):𝑥1-1𝑧))
1311, 12spcev 3606 . . . . . . 7 ((𝑓𝑔):𝑥1-1𝑧 → ∃ :𝑥1-1𝑧)
148, 13syl 17 . . . . . 6 ((𝑔:𝑥1-1𝑦𝑓:𝑦1-1𝑧) → ∃ :𝑥1-1𝑧)
154brdom 9001 . . . . . 6 (𝑥𝑧 ↔ ∃ :𝑥1-1𝑧)
1614, 15sylibr 234 . . . . 5 ((𝑔:𝑥1-1𝑦𝑓:𝑦1-1𝑧) → 𝑥𝑧)
1716exlimivv 1932 . . . 4 (∃𝑔𝑓(𝑔:𝑥1-1𝑦𝑓:𝑦1-1𝑧) → 𝑥𝑧)
186, 17sylbir 235 . . 3 ((∃𝑔 𝑔:𝑥1-1𝑦 ∧ ∃𝑓 𝑓:𝑦1-1𝑧) → 𝑥𝑧)
193, 5, 18syl2anb 598 . 2 ((𝑥𝑦𝑦𝑧) → 𝑥𝑧)
201, 19vtoclr 5748 1 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wex 1779   class class class wbr 5143  ccom 5689  1-1wf1 6558  cdom 8983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-dom 8987
This theorem is referenced by:  endomtr  9052  domentr  9053  cnvct  9074  ssctOLD  9092  undomOLD  9100  sdomdomtr  9150  domsdomtr  9152  xpen  9180  unxpdom2  9290  sucxpdom  9291  fidomdm  9374  hartogs  9584  harword  9603  unxpwdom  9629  harcard  10018  infxpenlem  10053  xpct  10056  indcardi  10081  fodomfi2  10100  infpwfien  10102  inffien  10103  djudoml  10225  djuinf  10229  infdju1  10230  djulepw  10233  unctb  10244  infdjuabs  10245  infdju  10247  infdif  10248  infdif2  10249  infxp  10254  infmap2  10257  fictb  10284  cfslb2n  10308  isfin32i  10405  fin1a2lem12  10451  hsmexlem1  10466  dmct  10564  brdom3  10568  brdom5  10569  brdom4  10570  imadomg  10574  fimact  10575  fnct  10577  mptct  10578  iundomg  10581  uniimadom  10584  ondomon  10603  unirnfdomd  10607  alephval2  10612  iunctb  10614  alephexp1  10619  alephreg  10622  cfpwsdom  10624  gchdomtri  10669  canthnum  10689  canthp1lem1  10692  canthp1  10694  pwfseqlem5  10703  pwxpndom2  10705  pwxpndom  10706  pwdjundom  10707  gchdjuidm  10708  gchxpidm  10709  gchpwdom  10710  gchaclem  10718  gchhar  10719  inar1  10815  rankcf  10817  grudomon  10857  grothac  10870  rpnnen  16263  cctop  23013  1stcfb  23453  2ndcredom  23458  2ndc1stc  23459  1stcrestlem  23460  2ndcctbss  23463  2ndcdisj2  23465  2ndcomap  23466  2ndcsep  23467  dis2ndc  23468  hauspwdom  23509  tx1stc  23658  tx2ndc  23659  met2ndci  24535  opnreen  24853  rectbntr0  24854  uniiccdif  25613  dyadmbl  25635  opnmblALT  25638  mbfimaopnlem  25690  abrexdomjm  32526  mptctf  32729  locfinreflem  33839  sigaclci  34133  omsmeas  34325  sibfof  34342  abrexdom  37737  heiborlem3  37820  imadomfi  42003  ttac  43048  idomsubgmo  43205  safesnsupfidom1o  43430  pr2dom  43540  tr3dom  43541  uzct  45068  rn1st  45280  omeiunle  46532  smfaddlem2  46779  smflimlem6  46791  smfmullem4  46809  smfpimbor1lem1  46813
  Copyright terms: Public domain W3C validator