Theorem rncoss 5959

Description: Range of a composition. (Contributed by NM, 19-Mar-1998.)

Assertion

Ref	Expression
rncoss	⊢ ran (𝐴 ∘ 𝐵) ⊆ ran 𝐴

Proof of Theorem rncoss

Step	Hyp	Ref	Expression
1		dmcoss 5957	. 2 ⊢ dom (◡𝐵 ∘ ◡𝐴) ⊆ dom ◡𝐴
2		df-rn 5662	. . 3 ⊢ ran (𝐴 ∘ 𝐵) = dom ◡(𝐴 ∘ 𝐵)
3		cnvco 5867	. . . 4 ⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴)
4	3	dmeqi 5886	. . 3 ⊢ dom ◡(𝐴 ∘ 𝐵) = dom (◡𝐵 ∘ ◡𝐴)
5	2, 4	eqtri 2784	. 2 ⊢ ran (𝐴 ∘ 𝐵) = dom (◡𝐵 ∘ ◡𝐴)
6		df-rn 5662	. 2 ⊢ ran 𝐴 = dom ◡𝐴
7	1, 5, 6	3sstr4i 3982	1 ⊢ ran (𝐴 ∘ 𝐵) ⊆ ran 𝐴

This proof depends on syntax axioms:   ⊆ wss 3899  ^◡ccnv 5650  dom cdm 5651  ran crn 5652   ∘ ccom 5655

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-ext 2733  ax-sep 5249  ax-pr 5391

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-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  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-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662

This theorem is used by:  cossxp  6273  fcof  6731  fin23lem29  10412  fin23lem30  10413  wunco  10811  imasless  17705  gsumzf1o  20119  znleval  21853  pi1xfrcnvlem  25370  pjss1coi  32758  pj3i  32803  smatrcl  34421  mblfinlem3  38557  mblfinlem4  38558  ismblfin  38559  relexp0a  44701  rntrclfv  44717  stoweidlem27  47006  fourierdlem42  47128  hoicvr  47527