Theorem domentr 9024

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

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

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 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7740

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 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-f1o 6538  df-en 8958  df-dom 8959

This theorem is used by:  domdifsn  9063  xpdom1g  9077  domunsncan  9080  sdomdomtr  9113  domen2  9123  mapdom2  9151  unxpdom2  9235  sucxpdom  9236  xpfir  9243  cardsdomelir  10035  infxpenlem  10073  xpct  10076  infpwfien  10122  inffien  10123  mappwen  10172  iunfictbso  10174  djuxpdom  10245  cdainflem  10247  djuinf  10248  djulepw  10252  ficardun2  10261  unctb  10263  infdjuabs  10264  infunabs  10265  infdju  10266  infdif  10267  infxpdom  10269  pwdjudom  10274  infmap2  10276  fictb  10303  cfslb  10325  fin1a2lem11  10469  fnct  10601  fnctOLD  10602  unirnfdomd  10633  iunctb  10640  alephreg  10648  cfpwsdom  10650  gchdomtri  10695  canthp1lem1  10718  pwfseqlem5  10729  pwxpndom  10732  gchdjuidm  10734  gchxpidm  10735  gchpwdom  10736  gchhar  10745  inttsk  10840  inar1  10841  tskcard  10847  znnen  16360  qnnen  16361  rpnnen  16375  rexpen  16376  aleph1irr  16394  cygctb  20086  lindsdom  22136  1stcfb  23743  2ndcredom  23748  2ndcctbss  23754  hauspwdom  23800  tx2ndc  23950  met1stc  24820  met2ndci  24821  re2ndc  25100  opnreen  25131  ovolctb2  25793  ovolfi  25795  uniiccdif  25879  dyadmbl  25901  opnmblALT  25904  vitali  25914  mbfimaopnlem  25956  mbfsup  25965  aannenlem3  26639  dmvlsiga  34743  sigapildsys  34777  omssubadd  34915  carsgclctunlem3  34935  karddom  35802  finminlem  37076  phpreu  38495  mblfinlem1  38543  pellexlem4  43792  pellexlem5  43793  pr2dom  44486  tr3dom  44487  nnfoctb  46008  ioonct  46493  caragenunicl  47478  eufunclem  50573  aacllem  50883