Theorem domentr 8562

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

Syntax hints:   → wi 4   ∧ wa 398   class class class wbr 5059   ≈ cen 8500   ≼ cdom 8501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-id 5455  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-f1o 6357  df-en 8504  df-dom 8505

This theorem is referenced by:  domdifsn  8594  xpdom1g  8608  domunsncan  8611  sdomdomtr  8644  domen2  8654  mapdom2  8682  php  8695  unxpdom2  8720  sucxpdom  8721  xpfir  8734  fodomfi  8791  cardsdomelir  9396  infxpenlem  9433  xpct  9436  infpwfien  9482  inffien  9483  mappwen  9532  iunfictbso  9534  djuxpdom  9605  cdainflem  9607  djuinf  9608  djulepw  9612  ficardun2  9619  unctb  9621  infdjuabs  9622  infunabs  9623  infdju  9624  infdif  9625  infxpdom  9627  pwdjudom  9632  infmap2  9634  fictb  9661  cfslb  9682  fin1a2lem11  9826  fnct  9953  unirnfdomd  9983  iunctb  9990  alephreg  9998  cfpwsdom  10000  gchdomtri  10045  canthp1lem1  10068  pwfseqlem5  10079  pwxpndom  10082  gchdjuidm  10084  gchxpidm  10085  gchpwdom  10086  gchhar  10095  inttsk  10190  inar1  10191  tskcard  10197  znnen  15559  qnnen  15560  rpnnen  15574  rexpen  15575  aleph1irr  15593  cygctb  19006  1stcfb  22047  2ndcredom  22052  2ndcctbss  22057  hauspwdom  22103  tx2ndc  22253  met1stc  23125  met2ndci  23126  re2ndc  23403  opnreen  23433  ovolctb2  24087  ovolfi  24089  uniiccdif  24173  dyadmbl  24195  opnmblALT  24198  vitali  24208  mbfimaopnlem  24250  mbfsup  24259  aannenlem3  24913  dmvlsiga  31383  sigapildsys  31416  omssubadd  31553  carsgclctunlem3  31573  finminlem  33661  phpreu  34870  lindsdom  34880  mblfinlem1  34923  pellexlem4  39422  pellexlem5  39423  pr2dom  39886  tr3dom  39887  nnfoctb  41302  ioonct  41805  subsaliuncl  42634  caragenunicl  42799  aacllem  44895