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

Theorem rncoss 5193
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 5192 . 2  |-  dom  ( `' B  o.  `' A )  C_  dom  `' A
2 df-rn 4941 . . 3  |-  ran  ( A  o.  B )  =  dom  `' ( A  o.  B )
3 cnvco 5118 . . . 4  |-  `' ( A  o.  B )  =  ( `' B  o.  `' A )
43dmeqi 5134 . . 3  |-  dom  `' ( A  o.  B
)  =  dom  ( `' B  o.  `' A )
52, 4eqtri 2425 . 2  |-  ran  ( A  o.  B )  =  dom  ( `' B  o.  `' A )
6 df-rn 4941 . 2  |-  ran  A  =  dom  `' A
71, 5, 63sstr4i 3473 1  |-  ran  ( A  o.  B )  C_ 
ran  A
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3406   `'ccnv 4929   dom cdm 4930   ran crn 4931    o. ccom 4934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pr 4618
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-rab 2755  df-v 3053  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3729  df-if 3875  df-sn 3962  df-pr 3964  df-op 3968  df-br 4385  df-opab 4443  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941
This theorem is referenced by:  cossxp  5455  fco  5666  fin23lem29  8656  fin23lem30  8657  wunco  9044  imasless  14970  gsumzf1o  17057  gsumzf1oOLD  17060  znleval  18707  pi1xfrcnvlem  21664  pjss1coi  27223  pj3i  27268  mblfinlem3  30258  mblfinlem4  30259  ismblfin  30260  stoweidlem27  32014  fourierdlem42  32136  relexp0a  38280
  Copyright terms: Public domain W3C validator