dmcoass

Description: The domain of composition is a collection of pairs of arrows. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	coafval.o	$⊢ \underset{˙}{\cdot} = {comp}_{a} (C)$
	coafval.a	$⊢ A = Arrow (C)$
Assertion	dmcoass	$⊢ dom \underset{˙}{\cdot} \subseteq A \times A$

Step	Hyp	Ref	Expression
1		coafval.o	$⊢ \underset{˙}{\cdot} = {comp}_{a} (C)$
2		coafval.a	$⊢ A = Arrow (C)$
3		eqid	$⊢ comp (C) = comp (C)$
4	1 2 3	coafval	$⊢ \underset{˙}{\cdot} = (g \in A, f \in \{h \in A \| {cod}_{a} (h) = {dom}_{a} (g)\} ⟼ ⟨{dom}_{a} (f), {cod}_{a} (g), 2^{nd} (g) (⟨{dom}_{a} (f), {dom}_{a} (g)⟩ comp (C) {cod}_{a} (g)) 2^{nd} (f)⟩)$
5	4	dmmpossx	$⊢ dom \underset{˙}{\cdot} \subseteq ⋃_{g \in A} (\{g\} \times \{h \in A \| {cod}_{a} (h) = {dom}_{a} (g)\})$
6		iunss	$⊢ ⋃_{g \in A} (\{g\} \times \{h \in A \| {cod}_{a} (h) = {dom}_{a} (g)\}) \subseteq A \times A \leftrightarrow \forall g \in A \{g\} \times \{h \in A \| {cod}_{a} (h) = {dom}_{a} (g)\} \subseteq A \times A$
7		snssi	$⊢ g \in A \to \{g\} \subseteq A$
8		ssrab2	$⊢ \{h \in A \| {cod}_{a} (h) = {dom}_{a} (g)\} \subseteq A$
9		xpss12	$⊢ (\{g\} \subseteq A \land \{h \in A \| {cod}_{a} (h) = {dom}_{a} (g)\} \subseteq A) \to \{g\} \times \{h \in A \| {cod}_{a} (h) = {dom}_{a} (g)\} \subseteq A \times A$
10	7 8 9	sylancl	$⊢ g \in A \to \{g\} \times \{h \in A \| {cod}_{a} (h) = {dom}_{a} (g)\} \subseteq A \times A$
11	6 10	mprgbir	$⊢ ⋃_{g \in A} (\{g\} \times \{h \in A \| {cod}_{a} (h) = {dom}_{a} (g)\}) \subseteq A \times A$
12	5 11	sstri	$⊢ dom \underset{˙}{\cdot} \subseteq A \times A$

Metamath Proof Explorer