Theorem domentr 9053

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

Syntax hints:   → wi 4   ∧ wa 395   class class class wbr 5143   ≈ cen 8982   ≼ 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-f1o 6568  df-en 8986  df-dom 8987

This theorem is referenced by:  domdifsn  9094  xpdom1g  9109  domunsncan  9112  sdomdomtr  9150  domen2  9160  mapdom2  9188  phpOLD  9259  unxpdom2  9290  sucxpdom  9291  xpfir  9300  fodomfiOLD  9370  cardsdomelir  10013  infxpenlem  10053  xpct  10056  infpwfien  10102  inffien  10103  mappwen  10152  iunfictbso  10154  djuxpdom  10226  cdainflem  10228  djuinf  10229  djulepw  10233  ficardun2  10242  unctb  10244  infdjuabs  10245  infunabs  10246  infdju  10247  infdif  10248  infxpdom  10250  pwdjudom  10255  infmap2  10257  fictb  10284  cfslb  10306  fin1a2lem11  10450  fnct  10577  unirnfdomd  10607  iunctb  10614  alephreg  10622  cfpwsdom  10624  gchdomtri  10669  canthp1lem1  10692  pwfseqlem5  10703  pwxpndom  10706  gchdjuidm  10708  gchxpidm  10709  gchpwdom  10710  gchhar  10719  inttsk  10814  inar1  10815  tskcard  10821  znnen  16248  qnnen  16249  rpnnen  16263  rexpen  16264  aleph1irr  16282  cygctb  19910  1stcfb  23453  2ndcredom  23458  2ndcctbss  23463  hauspwdom  23509  tx2ndc  23659  met1stc  24534  met2ndci  24535  re2ndc  24822  opnreen  24853  ovolctb2  25527  ovolfi  25529  uniiccdif  25613  dyadmbl  25635  opnmblALT  25638  vitali  25648  mbfimaopnlem  25690  mbfsup  25699  aannenlem3  26372  dmvlsiga  34130  sigapildsys  34163  omssubadd  34302  carsgclctunlem3  34322  finminlem  36319  phpreu  37611  lindsdom  37621  mblfinlem1  37664  pellexlem4  42843  pellexlem5  42844  pr2dom  43540  tr3dom  43541  nnfoctb  45053  ioonct  45550  subsaliuncl  46373  caragenunicl  46539  aacllem  49320