Theorem domentr 8998

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 8964	. 2 ⊢ (𝐵 ≈ 𝐶 → 𝐵 ≼ 𝐶)
2		domtr 8992	. 2 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
3	1, 2	sylan2 604	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   class class class wbr 5104   ≈ cen 8928   ≼ cdom 8929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-pow 5326  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-f1o 6532  df-en 8932  df-dom 8933

This theorem is referenced by:  domdifsn  9036  xpdom1g  9050  domunsncan  9053  sdomdomtr  9086  domen2  9096  mapdom2  9124  unxpdom2  9208  sucxpdom  9209  xpfir  9216  cardsdomelir  9947  infxpenlem  9985  xpct  9988  infpwfien  10034  inffien  10035  mappwen  10084  iunfictbso  10086  djuxpdom  10157  cdainflem  10159  djuinf  10160  djulepw  10164  ficardun2  10173  unctb  10175  infdjuabs  10176  infunabs  10177  infdju  10178  infdif  10179  infxpdom  10181  pwdjudom  10186  infmap2  10188  fictb  10215  cfslb  10238  fin1a2lem11  10382  fnct  10509  unirnfdomd  10540  iunctb  10547  alephreg  10555  cfpwsdom  10557  gchdomtri  10602  canthp1lem1  10625  pwfseqlem5  10636  pwxpndom  10639  gchdjuidm  10641  gchxpidm  10642  gchpwdom  10643  gchhar  10652  inttsk  10747  inar1  10748  tskcard  10754  znnen  16256  qnnen  16257  rpnnen  16271  rexpen  16272  aleph1irr  16290  cygctb  19950  1stcfb  23559  2ndcredom  23564  2ndcctbss  23569  hauspwdom  23615  tx2ndc  23765  met1stc  24635  met2ndci  24636  re2ndc  24915  opnreen  24946  ovolctb2  25608  ovolfi  25610  uniiccdif  25694  dyadmbl  25716  opnmblALT  25719  vitali  25729  mbfimaopnlem  25771  mbfsup  25780  aannenlem3  26448  dmvlsiga  34431  sigapildsys  34464  omssubadd  34602  carsgclctunlem3  34622  finminlem  36686  phpreu  38110  lindsdom  38120  mblfinlem1  38163  pellexlem4  43416  pellexlem5  43417  pr2dom  44110  tr3dom  44111  nnfoctb  45627  ioonct  46112  subsaliuncl  46931  caragenunicl  47097  eufunclem  50151  aacllem  50431