Theorem domentr 8987

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

Syntax hints:   → wi 4   ∧ wa 395   class class class wbr 5110   ≈ cen 8918   ≼ cdom 8919

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-f1o 6521  df-en 8922  df-dom 8923

This theorem is referenced by:  domdifsn  9028  xpdom1g  9043  domunsncan  9046  sdomdomtr  9080  domen2  9090  mapdom2  9118  unxpdom2  9208  sucxpdom  9209  xpfir  9218  fodomfiOLD  9288  cardsdomelir  9933  infxpenlem  9973  xpct  9976  infpwfien  10022  inffien  10023  mappwen  10072  iunfictbso  10074  djuxpdom  10146  cdainflem  10148  djuinf  10149  djulepw  10153  ficardun2  10162  unctb  10164  infdjuabs  10165  infunabs  10166  infdju  10167  infdif  10168  infxpdom  10170  pwdjudom  10175  infmap2  10177  fictb  10204  cfslb  10226  fin1a2lem11  10370  fnct  10497  unirnfdomd  10527  iunctb  10534  alephreg  10542  cfpwsdom  10544  gchdomtri  10589  canthp1lem1  10612  pwfseqlem5  10623  pwxpndom  10626  gchdjuidm  10628  gchxpidm  10629  gchpwdom  10630  gchhar  10639  inttsk  10734  inar1  10735  tskcard  10741  znnen  16187  qnnen  16188  rpnnen  16202  rexpen  16203  aleph1irr  16221  cygctb  19829  1stcfb  23339  2ndcredom  23344  2ndcctbss  23349  hauspwdom  23395  tx2ndc  23545  met1stc  24416  met2ndci  24417  re2ndc  24696  opnreen  24727  ovolctb2  25400  ovolfi  25402  uniiccdif  25486  dyadmbl  25508  opnmblALT  25511  vitali  25521  mbfimaopnlem  25563  mbfsup  25572  aannenlem3  26245  dmvlsiga  34126  sigapildsys  34159  omssubadd  34298  carsgclctunlem3  34318  finminlem  36313  phpreu  37605  lindsdom  37615  mblfinlem1  37658  pellexlem4  42827  pellexlem5  42828  pr2dom  43523  tr3dom  43524  nnfoctb  45049  ioonct  45542  subsaliuncl  46363  caragenunicl  46529  eufunclem  49514  aacllem  49794