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

Metamath Proof Explorer

Theorem cossxp

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

Ref Expression
Assertion cossxp ⊢ A ∘ B ⊆ dom ⁡ B × ran ⁡ A

Proof

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