Theorem domentr 8687

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

Syntax hints:   → wi 4   ∧ wa 399   class class class wbr 5053   ≈ cen 8623   ≼ cdom 8624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-f1o 6387  df-en 8627  df-dom 8628

This theorem is referenced by:  domdifsn  8728  xpdom1g  8742  domunsncan  8745  sdomdomtr  8779  domen2  8789  mapdom2  8817  php  8830  unxpdom2  8886  sucxpdom  8887  xpfir  8897  fodomfi  8949  cardsdomelir  9589  infxpenlem  9627  xpct  9630  infpwfien  9676  inffien  9677  mappwen  9726  iunfictbso  9728  djuxpdom  9799  cdainflem  9801  djuinf  9802  djulepw  9806  ficardun2  9816  ficardun2OLD  9817  unctb  9819  infdjuabs  9820  infunabs  9821  infdju  9822  infdif  9823  infxpdom  9825  pwdjudom  9830  infmap2  9832  fictb  9859  cfslb  9880  fin1a2lem11  10024  fnct  10151  unirnfdomd  10181  iunctb  10188  alephreg  10196  cfpwsdom  10198  gchdomtri  10243  canthp1lem1  10266  pwfseqlem5  10277  pwxpndom  10280  gchdjuidm  10282  gchxpidm  10283  gchpwdom  10284  gchhar  10293  inttsk  10388  inar1  10389  tskcard  10395  znnen  15773  qnnen  15774  rpnnen  15788  rexpen  15789  aleph1irr  15807  cygctb  19277  1stcfb  22342  2ndcredom  22347  2ndcctbss  22352  hauspwdom  22398  tx2ndc  22548  met1stc  23419  met2ndci  23420  re2ndc  23698  opnreen  23728  ovolctb2  24389  ovolfi  24391  uniiccdif  24475  dyadmbl  24497  opnmblALT  24500  vitali  24510  mbfimaopnlem  24552  mbfsup  24561  aannenlem3  25223  dmvlsiga  31809  sigapildsys  31842  omssubadd  31979  carsgclctunlem3  31999  finminlem  34244  phpreu  35498  lindsdom  35508  mblfinlem1  35551  pellexlem4  40357  pellexlem5  40358  pr2dom  40819  tr3dom  40820  nnfoctb  42268  ioonct  42750  subsaliuncl  43572  caragenunicl  43737  aacllem  46176