Theorem domentr 8957

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

Syntax hints:   → wi 4   ∧ wa 396   class class class wbr 5079   ≈ cen 8887   ≼ cdom 8888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-f1o 6499  df-en 8891  df-dom 8892

This theorem is referenced by:  domdifsn  8995  xpdom1g  9009  domunsncan  9012  sdomdomtr  9045  domen2  9055  mapdom2  9083  unxpdom2  9167  sucxpdom  9168  xpfir  9175  fodomfiOLD  9237  cardsdomelir  9895  infxpenlem  9933  xpct  9936  infpwfien  9982  inffien  9983  mappwen  10032  iunfictbso  10034  djuxpdom  10106  cdainflem  10108  djuinf  10109  djulepw  10113  ficardun2  10122  unctb  10124  infdjuabs  10125  infunabs  10126  infdju  10127  infdif  10128  infxpdom  10130  pwdjudom  10135  infmap2  10137  fictb  10164  cfslb  10186  fin1a2lem11  10330  fnct  10457  unirnfdomd  10488  iunctb  10495  alephreg  10503  cfpwsdom  10505  gchdomtri  10550  canthp1lem1  10573  pwfseqlem5  10584  pwxpndom  10587  gchdjuidm  10589  gchxpidm  10590  gchpwdom  10591  gchhar  10600  inttsk  10695  inar1  10696  tskcard  10702  znnen  16177  qnnen  16178  rpnnen  16192  rexpen  16193  aleph1irr  16211  cygctb  19865  1stcfb  23435  2ndcredom  23440  2ndcctbss  23445  hauspwdom  23491  tx2ndc  23641  met1stc  24511  met2ndci  24512  re2ndc  24791  opnreen  24822  ovolctb2  25484  ovolfi  25486  uniiccdif  25570  dyadmbl  25592  opnmblALT  25595  vitali  25605  mbfimaopnlem  25647  mbfsup  25656  aannenlem3  26321  dmvlsiga  34320  sigapildsys  34353  omssubadd  34491  carsgclctunlem3  34511  finminlem  36553  phpreu  37978  lindsdom  37988  mblfinlem1  38031  pellexlem4  43284  pellexlem5  43285  pr2dom  43978  tr3dom  43979  nnfoctb  45503  ioonct  45989  subsaliuncl  46808  caragenunicl  46974  eufunclem  50018  aacllem  50298