Theorem domentr 8935

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

Syntax hints:   → wi 4   ∧ wa 395   class class class wbr 5091   ≈ cen 8866   ≼ cdom 8867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-f1o 6488  df-en 8870  df-dom 8871

This theorem is referenced by:  domdifsn  8973  xpdom1g  8987  domunsncan  8990  sdomdomtr  9023  domen2  9033  mapdom2  9061  unxpdom2  9144  sucxpdom  9145  xpfir  9152  fodomfiOLD  9214  cardsdomelir  9866  infxpenlem  9904  xpct  9907  infpwfien  9953  inffien  9954  mappwen  10003  iunfictbso  10005  djuxpdom  10077  cdainflem  10079  djuinf  10080  djulepw  10084  ficardun2  10093  unctb  10095  infdjuabs  10096  infunabs  10097  infdju  10098  infdif  10099  infxpdom  10101  pwdjudom  10106  infmap2  10108  fictb  10135  cfslb  10157  fin1a2lem11  10301  fnct  10428  unirnfdomd  10458  iunctb  10465  alephreg  10473  cfpwsdom  10475  gchdomtri  10520  canthp1lem1  10543  pwfseqlem5  10554  pwxpndom  10557  gchdjuidm  10559  gchxpidm  10560  gchpwdom  10561  gchhar  10570  inttsk  10665  inar1  10666  tskcard  10672  znnen  16121  qnnen  16122  rpnnen  16136  rexpen  16137  aleph1irr  16155  cygctb  19805  1stcfb  23361  2ndcredom  23366  2ndcctbss  23371  hauspwdom  23417  tx2ndc  23567  met1stc  24437  met2ndci  24438  re2ndc  24717  opnreen  24748  ovolctb2  25421  ovolfi  25423  uniiccdif  25507  dyadmbl  25529  opnmblALT  25532  vitali  25542  mbfimaopnlem  25584  mbfsup  25593  aannenlem3  26266  dmvlsiga  34140  sigapildsys  34173  omssubadd  34311  carsgclctunlem3  34331  finminlem  36358  phpreu  37650  lindsdom  37660  mblfinlem1  37703  pellexlem4  42871  pellexlem5  42872  pr2dom  43566  tr3dom  43567  nnfoctb  45091  ioonct  45583  subsaliuncl  46402  caragenunicl  46568  eufunclem  49559  aacllem  49839