eldmcoa

Description: A pair <. G , F >. is in the domain of the arrow composition, if the domain of G equals the codomain of F . (In this case we say G and F are composable.) (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	coafval.o	$⊢ \underset{˙}{\cdot} = {comp}_{a} (C)$
	coafval.a	$⊢ A = Arrow (C)$
Assertion	eldmcoa	$⊢ G dom \underset{˙}{\cdot} F \leftrightarrow (F \in A \land G \in A \land {cod}_{a} (F) = {dom}_{a} (G))$

Proof

Step	Hyp	Ref	Expression
1		coafval.o	$⊢ \underset{˙}{\cdot} = {comp}_{a} (C)$
2		coafval.a	$⊢ A = Arrow (C)$
3		df-br	$⊢ G dom \underset{˙}{\cdot} F \leftrightarrow ⟨G, F⟩ \in dom \underset{˙}{\cdot}$
4		otex	$⊢ ⟨{dom}_{a} (f), {cod}_{a} (g), 2^{nd} (g) (⟨{dom}_{a} (f), {dom}_{a} (g)⟩ comp (C) {cod}_{a} (g)) 2^{nd} (f)⟩ \in V$
5	4	rgen2w	$⊢ \forall g \in A \forall 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)⟩ \in V$
6		eqid	$⊢ comp (C) = comp (C)$
7	1 2 6	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)⟩)$
8	7	fmpox	$⊢ \forall g \in A \forall 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)⟩ \in V \leftrightarrow \underset{˙}{\cdot} : ⋃_{g \in A} (\{g\} \times \{h \in A \| {cod}_{a} (h) = {dom}_{a} (g)\}) ⟶ V$
9	5 8	mpbi	$⊢ \underset{˙}{\cdot} : ⋃_{g \in A} (\{g\} \times \{h \in A \| {cod}_{a} (h) = {dom}_{a} (g)\}) ⟶ V$
10	9	fdmi	$⊢ dom \underset{˙}{\cdot} = ⋃_{g \in A} (\{g\} \times \{h \in A \| {cod}_{a} (h) = {dom}_{a} (g)\})$
11	10	eleq2i	$⊢ ⟨G, F⟩ \in dom \underset{˙}{\cdot} \leftrightarrow ⟨G, F⟩ \in ⋃_{g \in A} (\{g\} \times \{h \in A \| {cod}_{a} (h) = {dom}_{a} (g)\})$
12		fveq2	$⊢ g = G \to {dom}_{a} (g) = {dom}_{a} (G)$
13	12	eqeq2d	$⊢ g = G \to ({cod}_{a} (h) = {dom}_{a} (g) \leftrightarrow {cod}_{a} (h) = {dom}_{a} (G))$
14	13	rabbidv	$⊢ g = G \to \{h \in A \| {cod}_{a} (h) = {dom}_{a} (g)\} = \{h \in A \| {cod}_{a} (h) = {dom}_{a} (G)\}$
15	14	opeliunxp2	$⊢ ⟨G, F⟩ \in ⋃_{g \in A} (\{g\} \times \{h \in A \| {cod}_{a} (h) = {dom}_{a} (g)\}) \leftrightarrow (G \in A \land F \in \{h \in A \| {cod}_{a} (h) = {dom}_{a} (G)\})$
16		fveqeq2	$⊢ h = F \to ({cod}_{a} (h) = {dom}_{a} (G) \leftrightarrow {cod}_{a} (F) = {dom}_{a} (G))$
17	16	elrab	$⊢ F \in \{h \in A \| {cod}_{a} (h) = {dom}_{a} (G)\} \leftrightarrow (F \in A \land {cod}_{a} (F) = {dom}_{a} (G))$
18	17	anbi2i	$⊢ (G \in A \land F \in \{h \in A \| {cod}_{a} (h) = {dom}_{a} (G)\}) \leftrightarrow (G \in A \land (F \in A \land {cod}_{a} (F) = {dom}_{a} (G)))$
19		an12	$⊢ (G \in A \land (F \in A \land {cod}_{a} (F) = {dom}_{a} (G))) \leftrightarrow (F \in A \land (G \in A \land {cod}_{a} (F) = {dom}_{a} (G)))$
20		3anass	$⊢ (F \in A \land G \in A \land {cod}_{a} (F) = {dom}_{a} (G)) \leftrightarrow (F \in A \land (G \in A \land {cod}_{a} (F) = {dom}_{a} (G)))$
21	19 20	bitr4i	$⊢ (G \in A \land (F \in A \land {cod}_{a} (F) = {dom}_{a} (G))) \leftrightarrow (F \in A \land G \in A \land {cod}_{a} (F) = {dom}_{a} (G))$
22	15 18 21	3bitri	$⊢ ⟨G, F⟩ \in ⋃_{g \in A} (\{g\} \times \{h \in A \| {cod}_{a} (h) = {dom}_{a} (g)\}) \leftrightarrow (F \in A \land G \in A \land {cod}_{a} (F) = {dom}_{a} (G))$
23	3 11 22	3bitri	$⊢ G dom \underset{˙}{\cdot} F \leftrightarrow (F \in A \land G \in A \land {cod}_{a} (F) = {dom}_{a} (G))$

Metamath Proof Explorer

Theorem eldmcoa

Proof