Theorem domentr 9011

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

Syntax hints:   → wi 4   ∧ wa 400   class class class wbr 5110   ≈ cen 8941   ≼ cdom 8942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-f1o 6545  df-en 8945  df-dom 8946

This theorem is referenced by:  domdifsn  9049  xpdom1g  9063  domunsncan  9066  sdomdomtr  9099  domen2  9109  mapdom2  9137  unxpdom2  9221  sucxpdom  9222  xpfir  9229  cardsdomelir  9960  infxpenlem  9998  xpct  10001  infpwfien  10047  inffien  10048  mappwen  10097  iunfictbso  10099  djuxpdom  10170  cdainflem  10172  djuinf  10173  djulepw  10177  ficardun2  10186  unctb  10188  infdjuabs  10189  infunabs  10190  infdju  10191  infdif  10192  infxpdom  10194  pwdjudom  10199  infmap2  10201  fictb  10228  cfslb  10251  fin1a2lem11  10395  fnct  10522  unirnfdomd  10553  iunctb  10560  alephreg  10568  cfpwsdom  10570  gchdomtri  10615  canthp1lem1  10638  pwfseqlem5  10649  pwxpndom  10652  gchdjuidm  10654  gchxpidm  10655  gchpwdom  10656  gchhar  10665  inttsk  10760  inar1  10761  tskcard  10767  znnen  16269  qnnen  16270  rpnnen  16284  rexpen  16285  aleph1irr  16303  cygctb  19963  1stcfb  23583  2ndcredom  23588  2ndcctbss  23593  hauspwdom  23639  tx2ndc  23789  met1stc  24659  met2ndci  24660  re2ndc  24939  opnreen  24970  ovolctb2  25632  ovolfi  25634  uniiccdif  25718  dyadmbl  25740  opnmblALT  25743  vitali  25753  mbfimaopnlem  25795  mbfsup  25804  aannenlem3  26474  dmvlsiga  34500  sigapildsys  34533  omssubadd  34671  carsgclctunlem3  34691  karddom  35555  finminlem  36810  phpreu  38236  lindsdom  38246  mblfinlem1  38289  pellexlem4  43542  pellexlem5  43543  pr2dom  44236  tr3dom  44237  nnfoctb  45751  ioonct  46236  subsaliuncl  47055  caragenunicl  47221  eufunclem  50282  aacllem  50584