arwhoma

Description: An arrow is contained in the hom-set corresponding to its domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	arwrcl.a	$⊢ A = Arrow (C)$
	arwhoma.h	$⊢ H = {Hom}_{a} (C)$
Assertion	arwhoma	$⊢ F \in A \to F \in ({dom}_{a} (F) H {cod}_{a} (F))$

Proof

Step	Hyp	Ref	Expression
1		arwrcl.a	$⊢ A = Arrow (C)$
2		arwhoma.h	$⊢ H = {Hom}_{a} (C)$
3	1 2	arwval	$⊢ A = ⋃ ran H$
4	3	eleq2i	$⊢ F \in A \leftrightarrow F \in ⋃ ran H$
5	4	biimpi	$⊢ F \in A \to F \in ⋃ ran H$
6		eqid	$⊢ {Base}_{C} = {Base}_{C}$
7	1	arwrcl	$⊢ F \in A \to C \in Cat$
8	2 6 7	homaf	$⊢ F \in A \to H : {Base}_{C} \times {Base}_{C} ⟶ 𝒫 (({Base}_{C} \times {Base}_{C}) \times V)$
9		ffn	$⊢ H : {Base}_{C} \times {Base}_{C} ⟶ 𝒫 (({Base}_{C} \times {Base}_{C}) \times V) \to H Fn ({Base}_{C} \times {Base}_{C})$
10		fnunirn	$⊢ H Fn ({Base}_{C} \times {Base}_{C}) \to (F \in ⋃ ran H \leftrightarrow \exists z \in ({Base}_{C} \times {Base}_{C}) F \in H (z))$
11	8 9 10	3syl	$⊢ F \in A \to (F \in ⋃ ran H \leftrightarrow \exists z \in ({Base}_{C} \times {Base}_{C}) F \in H (z))$
12	5 11	mpbid	$⊢ F \in A \to \exists z \in ({Base}_{C} \times {Base}_{C}) F \in H (z)$
13		fveq2	$⊢ z = ⟨x, y⟩ \to H (z) = H (⟨x, y⟩)$
14		df-ov	$⊢ x H y = H (⟨x, y⟩)$
15	13 14	eqtr4di	$⊢ z = ⟨x, y⟩ \to H (z) = x H y$
16	15	eleq2d	$⊢ z = ⟨x, y⟩ \to (F \in H (z) \leftrightarrow F \in (x H y))$
17	16	rexxp	$⊢ \exists z \in ({Base}_{C} \times {Base}_{C}) F \in H (z) \leftrightarrow \exists x \in {Base}_{C} \exists y \in {Base}_{C} F \in (x H y)$
18	12 17	sylib	$⊢ F \in A \to \exists x \in {Base}_{C} \exists y \in {Base}_{C} F \in (x H y)$
19		id	$⊢ F \in (x H y) \to F \in (x H y)$
20	2	homadm	$⊢ F \in (x H y) \to {dom}_{a} (F) = x$
21	2	homacd	$⊢ F \in (x H y) \to {cod}_{a} (F) = y$
22	20 21	oveq12d	$⊢ F \in (x H y) \to {dom}_{a} (F) H {cod}_{a} (F) = x H y$
23	19 22	eleqtrrd	$⊢ F \in (x H y) \to F \in ({dom}_{a} (F) H {cod}_{a} (F))$
24	23	rexlimivw	$⊢ \exists y \in {Base}_{C} F \in (x H y) \to F \in ({dom}_{a} (F) H {cod}_{a} (F))$
25	24	rexlimivw	$⊢ \exists x \in {Base}_{C} \exists y \in {Base}_{C} F \in (x H y) \to F \in ({dom}_{a} (F) H {cod}_{a} (F))$
26	18 25	syl	$⊢ F \in A \to F \in ({dom}_{a} (F) H {cod}_{a} (F))$

Metamath Proof Explorer

Theorem arwhoma

Proof