Theorem domentr 9020

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   class class class wbr 5103   ≈ cen 8950   ≼ cdom 8951

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pow 5330  ax-pr 5398  ax-un 7737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-f1o 6540  df-en 8954  df-dom 8955

This theorem is used by:  domdifsn  9059  xpdom1g  9073  domunsncan  9076  sdomdomtr  9109  domen2  9119  mapdom2  9147  unxpdom2  9231  sucxpdom  9232  xpfir  9239  cardsdomelir  9979  infxpenlem  10017  xpct  10020  infpwfien  10066  inffien  10067  mappwen  10116  iunfictbso  10118  djuxpdom  10189  cdainflem  10191  djuinf  10192  djulepw  10196  ficardun2  10205  unctb  10207  infdjuabs  10208  infunabs  10209  infdju  10210  infdif  10211  infxpdom  10213  pwdjudom  10218  infmap2  10220  fictb  10247  cfslb  10269  fin1a2lem11  10413  fnct  10545  fnctOLD  10546  unirnfdomd  10577  iunctb  10584  alephreg  10592  cfpwsdom  10594  gchdomtri  10639  canthp1lem1  10662  pwfseqlem5  10673  pwxpndom  10676  gchdjuidm  10678  gchxpidm  10679  gchpwdom  10680  gchhar  10689  inttsk  10784  inar1  10785  tskcard  10791  znnen  16301  qnnen  16302  rpnnen  16316  rexpen  16317  aleph1irr  16335  cygctb  20020  lindsdom  22064  1stcfb  23671  2ndcredom  23676  2ndcctbss  23682  hauspwdom  23728  tx2ndc  23878  met1stc  24748  met2ndci  24749  re2ndc  25028  opnreen  25059  ovolctb2  25721  ovolfi  25723  uniiccdif  25807  dyadmbl  25829  opnmblALT  25832  vitali  25842  mbfimaopnlem  25884  mbfsup  25893  aannenlem3  26567  dmvlsiga  34640  sigapildsys  34674  omssubadd  34812  carsgclctunlem3  34832  karddom  35688  finminlem  36938  phpreu  38359  mblfinlem1  38407  pellexlem4  43674  pellexlem5  43675  pr2dom  44368  tr3dom  44369  nnfoctb  45883  ioonct  46368  caragenunicl  47353  eufunclem  50448  aacllem  50773