Theorem domentr 8953

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

Syntax hints:   → wi 4   ∧ wa 395   class class class wbr 5086   ≈ cen 8883   ≼ cdom 8884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-f1o 6499  df-en 8887  df-dom 8888

This theorem is referenced by:  domdifsn  8991  xpdom1g  9005  domunsncan  9008  sdomdomtr  9041  domen2  9051  mapdom2  9079  unxpdom2  9163  sucxpdom  9164  xpfir  9171  fodomfiOLD  9233  cardsdomelir  9888  infxpenlem  9926  xpct  9929  infpwfien  9975  inffien  9976  mappwen  10025  iunfictbso  10027  djuxpdom  10099  cdainflem  10101  djuinf  10102  djulepw  10106  ficardun2  10115  unctb  10117  infdjuabs  10118  infunabs  10119  infdju  10120  infdif  10121  infxpdom  10123  pwdjudom  10128  infmap2  10130  fictb  10157  cfslb  10179  fin1a2lem11  10323  fnct  10450  unirnfdomd  10481  iunctb  10488  alephreg  10496  cfpwsdom  10498  gchdomtri  10543  canthp1lem1  10566  pwfseqlem5  10577  pwxpndom  10580  gchdjuidm  10582  gchxpidm  10583  gchpwdom  10584  gchhar  10593  inttsk  10688  inar1  10689  tskcard  10695  znnen  16170  qnnen  16171  rpnnen  16185  rexpen  16186  aleph1irr  16204  cygctb  19858  1stcfb  23420  2ndcredom  23425  2ndcctbss  23430  hauspwdom  23476  tx2ndc  23626  met1stc  24496  met2ndci  24497  re2ndc  24776  opnreen  24807  ovolctb2  25469  ovolfi  25471  uniiccdif  25555  dyadmbl  25577  opnmblALT  25580  vitali  25590  mbfimaopnlem  25632  mbfsup  25641  aannenlem3  26307  dmvlsiga  34289  sigapildsys  34322  omssubadd  34460  carsgclctunlem3  34480  finminlem  36516  phpreu  37939  lindsdom  37949  mblfinlem1  37992  pellexlem4  43278  pellexlem5  43279  pr2dom  43972  tr3dom  43973  nnfoctb  45497  ioonct  45985  subsaliuncl  46804  caragenunicl  46970  eufunclem  50008  aacllem  50288