This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rncoss

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

		Ref	Expression
	Assertion	rncoss	$⊢ ran (A \circ B) \subseteq ran A$

Step	Hyp	Ref	Expression
1		dmcoss	$⊢ dom (B^{-1} \circ A^{-1}) \subseteq dom A^{-1}$
2		df-rn	$⊢ ran (A \circ B) = dom {(A \circ B)}^{-1}$
3		cnvco	$⊢ {(A \circ B)}^{-1} = B^{-1} \circ A^{-1}$
4	3	dmeqi	$⊢ dom {(A \circ B)}^{-1} = dom (B^{-1} \circ A^{-1})$
5	2 4	eqtri	$⊢ ran (A \circ B) = dom (B^{-1} \circ A^{-1})$
6		df-rn	$⊢ ran A = dom A^{-1}$
7	1 5 6	3sstr4i	$⊢ ran (A \circ B) \subseteq ran A$