Theorem domentr 8834

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

Syntax hints:   → wi 4   ∧ wa 397   class class class wbr 5081   ≈ cen 8761   ≼ cdom 8762

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-f1o 6465  df-en 8765  df-dom 8766

This theorem is referenced by:  domdifsn  8879  xpdom1g  8894  domunsncan  8897  sdomdomtr  8935  domen2  8945  mapdom2  8973  phpOLD  9043  unxpdom2  9075  sucxpdom  9076  xpfir  9085  fodomfi  9136  cardsdomelir  9775  infxpenlem  9815  xpct  9818  infpwfien  9864  inffien  9865  mappwen  9914  iunfictbso  9916  djuxpdom  9987  cdainflem  9989  djuinf  9990  djulepw  9994  ficardun2  10004  ficardun2OLD  10005  unctb  10007  infdjuabs  10008  infunabs  10009  infdju  10010  infdif  10011  infxpdom  10013  pwdjudom  10018  infmap2  10020  fictb  10047  cfslb  10068  fin1a2lem11  10212  fnct  10339  unirnfdomd  10369  iunctb  10376  alephreg  10384  cfpwsdom  10386  gchdomtri  10431  canthp1lem1  10454  pwfseqlem5  10465  pwxpndom  10468  gchdjuidm  10470  gchxpidm  10471  gchpwdom  10472  gchhar  10481  inttsk  10576  inar1  10577  tskcard  10583  znnen  15966  qnnen  15967  rpnnen  15981  rexpen  15982  aleph1irr  16000  cygctb  19538  1stcfb  22641  2ndcredom  22646  2ndcctbss  22651  hauspwdom  22697  tx2ndc  22847  met1stc  23722  met2ndci  23723  re2ndc  24009  opnreen  24039  ovolctb2  24701  ovolfi  24703  uniiccdif  24787  dyadmbl  24809  opnmblALT  24812  vitali  24822  mbfimaopnlem  24864  mbfsup  24873  aannenlem3  25535  dmvlsiga  32142  sigapildsys  32175  omssubadd  32312  carsgclctunlem3  32332  finminlem  34552  phpreu  35805  lindsdom  35815  mblfinlem1  35858  pellexlem4  40691  pellexlem5  40692  pr2dom  41172  tr3dom  41173  nnfoctb  42633  ioonct  43124  subsaliuncl  43946  caragenunicl  44112  aacllem  46563