Theorem domentr 8962

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

Syntax hints:   → wi 4   ∧ wa 395   class class class wbr 5100   ≈ cen 8892   ≼ cdom 8893

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 5243  ax-pow 5312  ax-pr 5379  ax-un 7690

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-f1o 6507  df-en 8896  df-dom 8897

This theorem is referenced by:  domdifsn  9000  xpdom1g  9014  domunsncan  9017  sdomdomtr  9050  domen2  9060  mapdom2  9088  unxpdom2  9172  sucxpdom  9173  xpfir  9180  fodomfiOLD  9242  cardsdomelir  9897  infxpenlem  9935  xpct  9938  infpwfien  9984  inffien  9985  mappwen  10034  iunfictbso  10036  djuxpdom  10108  cdainflem  10110  djuinf  10111  djulepw  10115  ficardun2  10124  unctb  10126  infdjuabs  10127  infunabs  10128  infdju  10129  infdif  10130  infxpdom  10132  pwdjudom  10137  infmap2  10139  fictb  10166  cfslb  10188  fin1a2lem11  10332  fnct  10459  unirnfdomd  10490  iunctb  10497  alephreg  10505  cfpwsdom  10507  gchdomtri  10552  canthp1lem1  10575  pwfseqlem5  10586  pwxpndom  10589  gchdjuidm  10591  gchxpidm  10592  gchpwdom  10593  gchhar  10602  inttsk  10697  inar1  10698  tskcard  10704  znnen  16149  qnnen  16150  rpnnen  16164  rexpen  16165  aleph1irr  16183  cygctb  19833  1stcfb  23401  2ndcredom  23406  2ndcctbss  23411  hauspwdom  23457  tx2ndc  23607  met1stc  24477  met2ndci  24478  re2ndc  24757  opnreen  24788  ovolctb2  25461  ovolfi  25463  uniiccdif  25547  dyadmbl  25569  opnmblALT  25572  vitali  25582  mbfimaopnlem  25624  mbfsup  25633  aannenlem3  26306  dmvlsiga  34306  sigapildsys  34339  omssubadd  34477  carsgclctunlem3  34497  finminlem  36531  phpreu  37852  lindsdom  37862  mblfinlem1  37905  pellexlem4  43186  pellexlem5  43187  pr2dom  43880  tr3dom  43881  nnfoctb  45405  ioonct  45894  subsaliuncl  46713  caragenunicl  46879  eufunclem  49877  aacllem  50157