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

Theorem domtr 8537
 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 8490 . 2 Rel ≼
2 vex 3474 . . . 4 𝑦 ∈ V
32brdom 8496 . . 3 (𝑥𝑦 ↔ ∃𝑔 𝑔:𝑥1-1𝑦)
4 vex 3474 . . . 4 𝑧 ∈ V
54brdom 8496 . . 3 (𝑦𝑧 ↔ ∃𝑓 𝑓:𝑦1-1𝑧)
6 exdistrv 1957 . . . 4 (∃𝑔𝑓(𝑔:𝑥1-1𝑦𝑓:𝑦1-1𝑧) ↔ (∃𝑔 𝑔:𝑥1-1𝑦 ∧ ∃𝑓 𝑓:𝑦1-1𝑧))
7 f1co 6558 . . . . . . . 8 ((𝑓:𝑦1-1𝑧𝑔:𝑥1-1𝑦) → (𝑓𝑔):𝑥1-1𝑧)
87ancoms 462 . . . . . . 7 ((𝑔:𝑥1-1𝑦𝑓:𝑦1-1𝑧) → (𝑓𝑔):𝑥1-1𝑧)
9 vex 3474 . . . . . . . . 9 𝑓 ∈ V
10 vex 3474 . . . . . . . . 9 𝑔 ∈ V
119, 10coex 7610 . . . . . . . 8 (𝑓𝑔) ∈ V
12 f1eq1 6543 . . . . . . . 8 ( = (𝑓𝑔) → (:𝑥1-1𝑧 ↔ (𝑓𝑔):𝑥1-1𝑧))
1311, 12spcev 3584 . . . . . . 7 ((𝑓𝑔):𝑥1-1𝑧 → ∃ :𝑥1-1𝑧)
148, 13syl 17 . . . . . 6 ((𝑔:𝑥1-1𝑦𝑓:𝑦1-1𝑧) → ∃ :𝑥1-1𝑧)
154brdom 8496 . . . . . 6 (𝑥𝑧 ↔ ∃ :𝑥1-1𝑧)
1614, 15sylibr 237 . . . . 5 ((𝑔:𝑥1-1𝑦𝑓:𝑦1-1𝑧) → 𝑥𝑧)
1716exlimivv 1934 . . . 4 (∃𝑔𝑓(𝑔:𝑥1-1𝑦𝑓:𝑦1-1𝑧) → 𝑥𝑧)
186, 17sylbir 238 . . 3 ((∃𝑔 𝑔:𝑥1-1𝑦 ∧ ∃𝑓 𝑓:𝑦1-1𝑧) → 𝑥𝑧)
193, 5, 18syl2anb 600 . 2 ((𝑥𝑦𝑦𝑧) → 𝑥𝑧)
201, 19vtoclr 5588 1 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1781   class class class wbr 5039   ∘ ccom 5532  –1-1→wf1 6325   ≼ cdom 8482 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ral 3131  df-rex 3132  df-rab 3135  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-opab 5102  df-id 5433  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-dom 8486 This theorem is referenced by:  endomtr  8542  domentr  8543  cnvct  8561  ssct  8573  undom  8580  sdomdomtr  8626  domsdomtr  8628  xpen  8656  unxpdom2  8702  sucxpdom  8703  fidomdm  8777  hartogs  8984  harword  9003  unxpwdom  9029  harcard  9383  infxpenlem  9416  xpct  9419  indcardi  9444  fodomfi2  9463  infpwfien  9465  inffien  9466  djudoml  9587  djuinf  9591  infdju1  9592  djulepw  9595  unctb  9604  infdjuabs  9605  infdju  9607  infdif  9608  infdif2  9609  infxp  9614  infmap2  9617  fictb  9644  cfslb2n  9667  isfin32i  9764  fin1a2lem12  9810  hsmexlem1  9825  dmct  9923  brdom3  9927  brdom5  9928  brdom4  9929  imadomg  9933  fimact  9934  fnct  9936  mptct  9937  iundomg  9940  uniimadom  9943  ondomon  9962  unirnfdomd  9966  alephval2  9971  iunctb  9973  alephexp1  9978  alephreg  9981  cfpwsdom  9983  gchdomtri  10028  canthnum  10048  canthp1lem1  10051  canthp1  10053  pwfseqlem5  10062  pwxpndom2  10064  pwxpndom  10065  pwdjundom  10066  gchdjuidm  10067  gchxpidm  10068  gchpwdom  10069  gchaclem  10077  gchhar  10078  inar1  10174  rankcf  10176  grudomon  10216  grothac  10229  rpnnen  15559  cctop  21589  1stcfb  22028  2ndcredom  22033  2ndc1stc  22034  1stcrestlem  22035  2ndcctbss  22038  2ndcdisj2  22040  2ndcomap  22041  2ndcsep  22042  dis2ndc  22043  hauspwdom  22084  tx1stc  22233  tx2ndc  22234  met2ndci  23107  opnreen  23414  rectbntr0  23415  uniiccdif  24160  dyadmbl  24182  opnmblALT  24185  mbfimaopnlem  24237  abrexdomjm  30252  mptctf  30439  locfinreflem  31114  sigaclci  31398  omsmeas  31588  sibfof  31605  abrexdom  35046  heiborlem3  35129  ttac  39772  idomsubgmo  39937  pr2dom  40030  tr3dom  40031  uzct  41480  omeiunle  42947  smfaddlem2  43188  smflimlem6  43200  smfmullem4  43217  smfpimbor1lem1  43221
 Copyright terms: Public domain W3C validator