Theorem cossxp

Description: Composition as a subset of the Cartesian product of factors. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Assertion	cossxp	⊢ ( 𝐴 ∘ 𝐵 ) ⊆ ( dom 𝐵 × ran 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		relco	⊢ Rel ( 𝐴 ∘ 𝐵 )
2		relssdmrn	⊢ ( Rel ( 𝐴 ∘ 𝐵 ) → ( 𝐴 ∘ 𝐵 ) ⊆ ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) )
3	1 2	ax-mp	⊢ ( 𝐴 ∘ 𝐵 ) ⊆ ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) )
4		dmcoss	⊢ dom ( 𝐴 ∘ 𝐵 ) ⊆ dom 𝐵
5		rncoss	⊢ ran ( 𝐴 ∘ 𝐵 ) ⊆ ran 𝐴
6		xpss12	⊢ ( ( dom ( 𝐴 ∘ 𝐵 ) ⊆ dom 𝐵 ∧ ran ( 𝐴 ∘ 𝐵 ) ⊆ ran 𝐴 ) → ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) ⊆ ( dom 𝐵 × ran 𝐴 ) )
7	4 5 6	mp2an	⊢ ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) ⊆ ( dom 𝐵 × ran 𝐴 )
8	3 7	sstri	⊢ ( 𝐴 ∘ 𝐵 ) ⊆ ( dom 𝐵 × ran 𝐴 )