Theorem domentr 8770

Description: Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998.)

Assertion

Ref	Expression
domentr	⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶)

Proof of Theorem domentr

Step	Hyp	Ref	Expression
1		endom 8738	. 2 ⊢ (𝐵 ≈ 𝐶 → 𝐵 ≼ 𝐶)
2		domtr 8764	. 2 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
3	1, 2	sylan2 592	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   class class class wbr 5078   ≈ cen 8704   ≼ cdom 8705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-f1o 6437  df-en 8708  df-dom 8709

This theorem is referenced by:  domdifsn  8811  xpdom1g  8825  domunsncan  8828  sdomdomtr  8862  domen2  8872  mapdom2  8900  phpOLD  8970  unxpdom2  8992  sucxpdom  8993  xpfir  9002  fodomfi  9053  cardsdomelir  9715  infxpenlem  9753  xpct  9756  infpwfien  9802  inffien  9803  mappwen  9852  iunfictbso  9854  djuxpdom  9925  cdainflem  9927  djuinf  9928  djulepw  9932  ficardun2  9942  ficardun2OLD  9943  unctb  9945  infdjuabs  9946  infunabs  9947  infdju  9948  infdif  9949  infxpdom  9951  pwdjudom  9956  infmap2  9958  fictb  9985  cfslb  10006  fin1a2lem11  10150  fnct  10277  unirnfdomd  10307  iunctb  10314  alephreg  10322  cfpwsdom  10324  gchdomtri  10369  canthp1lem1  10392  pwfseqlem5  10403  pwxpndom  10406  gchdjuidm  10408  gchxpidm  10409  gchpwdom  10410  gchhar  10419  inttsk  10514  inar1  10515  tskcard  10521  znnen  15902  qnnen  15903  rpnnen  15917  rexpen  15918  aleph1irr  15936  cygctb  19474  1stcfb  22577  2ndcredom  22582  2ndcctbss  22587  hauspwdom  22633  tx2ndc  22783  met1stc  23658  met2ndci  23659  re2ndc  23945  opnreen  23975  ovolctb2  24637  ovolfi  24639  uniiccdif  24723  dyadmbl  24745  opnmblALT  24748  vitali  24758  mbfimaopnlem  24800  mbfsup  24809  aannenlem3  25471  dmvlsiga  32076  sigapildsys  32109  omssubadd  32246  carsgclctunlem3  32266  finminlem  34486  phpreu  35740  lindsdom  35750  mblfinlem1  35793  pellexlem4  40634  pellexlem5  40635  pr2dom  41096  tr3dom  41097  nnfoctb  42548  ioonct  43029  subsaliuncl  43851  caragenunicl  44016  aacllem  46457