Theorem rncoss

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

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

Proof

Step	Hyp	Ref	Expression
1		dmcoss	⊢ dom ( ◡ 𝐵 ∘ ◡ 𝐴 ) ⊆ dom ◡ 𝐴
2		df-rn	⊢ ran ( 𝐴 ∘ 𝐵 ) = dom ◡ ( 𝐴 ∘ 𝐵 )
3		cnvco	⊢ ◡ ( 𝐴 ∘ 𝐵 ) = ( ◡ 𝐵 ∘ ◡ 𝐴 )
4	3	dmeqi	⊢ dom ◡ ( 𝐴 ∘ 𝐵 ) = dom ( ◡ 𝐵 ∘ ◡ 𝐴 )
5	2 4	eqtri	⊢ ran ( 𝐴 ∘ 𝐵 ) = dom ( ◡ 𝐵 ∘ ◡ 𝐴 )
6		df-rn	⊢ ran 𝐴 = dom ◡ 𝐴
7	1 5 6	3sstr4i	⊢ ran ( 𝐴 ∘ 𝐵 ) ⊆ ran 𝐴