MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rncoss Structured version   Unicode version

Theorem rncoss 5184
Description: Range of a composition. (Contributed by NM, 19-Mar-1998.)
Assertion
Ref Expression
rncoss  |-  ran  ( A  o.  B )  C_ 
ran  A

Proof of Theorem rncoss
StepHypRef Expression
1 dmcoss 5183 . 2  |-  dom  ( `' B  o.  `' A )  C_  dom  `' A
2 df-rn 4935 . . 3  |-  ran  ( A  o.  B )  =  dom  `' ( A  o.  B )
3 cnvco 5109 . . . 4  |-  `' ( A  o.  B )  =  ( `' B  o.  `' A )
43dmeqi 5125 . . 3  |-  dom  `' ( A  o.  B
)  =  dom  ( `' B  o.  `' A )
52, 4eqtri 2478 . 2  |-  ran  ( A  o.  B )  =  dom  ( `' B  o.  `' A )
6 df-rn 4935 . 2  |-  ran  A  =  dom  `' A
71, 5, 63sstr4i 3479 1  |-  ran  ( A  o.  B )  C_ 
ran  A
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3412   `'ccnv 4923   dom cdm 4924   ran crn 4925    o. ccom 4928
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4497  ax-nul 4505  ax-pr 4615
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-rab 2801  df-v 3056  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-nul 3722  df-if 3876  df-sn 3962  df-pr 3964  df-op 3968  df-br 4377  df-opab 4435  df-cnv 4932  df-co 4933  df-dm 4934  df-rn 4935
This theorem is referenced by:  cossxp  5444  fco  5652  fin23lem29  8597  fin23lem30  8598  wunco  8987  imasless  14566  gsumzf1o  16481  gsumzf1oOLD  16484  znleval  18082  pi1xfrcnvlem  20730  pjss1coi  25688  pj3i  25733  relexprn  27458  mblfinlem3  28554  mblfinlem4  28555  ismblfin  28556  stoweidlem27  29946
  Copyright terms: Public domain W3C validator