homarel

Description: An arrow is an ordered pair. (Contributed by Mario Carneiro, 11-Jan-2017)

		Ref	Expression
	Hypothesis	homahom.h	$⊢ H = {Hom}_{a} (C)$
	Assertion	homarel	$⊢ Rel (X H Y)$

Step	Hyp	Ref	Expression
1		homahom.h	$⊢ H = {Hom}_{a} (C)$
2		xpss	$⊢ ({Base}_{C} \times {Base}_{C}) \times V \subseteq V \times V$
3		eqid	$⊢ {Base}_{C} = {Base}_{C}$
4	1	homarcl	$⊢ f \in (X H Y) \to C \in Cat$
5	1 3 4	homaf	$⊢ f \in (X H Y) \to H : {Base}_{C} \times {Base}_{C} ⟶ 𝒫 (({Base}_{C} \times {Base}_{C}) \times V)$
6	1 3	homarcl2	$⊢ f \in (X H Y) \to (X \in {Base}_{C} \land Y \in {Base}_{C})$
7	6	simpld	$⊢ f \in (X H Y) \to X \in {Base}_{C}$
8	6	simprd	$⊢ f \in (X H Y) \to Y \in {Base}_{C}$
9	5 7 8	fovcdmd	$⊢ f \in (X H Y) \to X H Y \in 𝒫 (({Base}_{C} \times {Base}_{C}) \times V)$
10		elelpwi	$⊢ (f \in (X H Y) \land X H Y \in 𝒫 (({Base}_{C} \times {Base}_{C}) \times V)) \to f \in (({Base}_{C} \times {Base}_{C}) \times V)$
11	9 10	mpdan	$⊢ f \in (X H Y) \to f \in (({Base}_{C} \times {Base}_{C}) \times V)$
12	2 11	sselid	$⊢ f \in (X H Y) \to f \in (V \times V)$
13	12	ssriv	$⊢ X H Y \subseteq V \times V$
14		df-rel	$⊢ Rel (X H Y) \leftrightarrow X H Y \subseteq V \times V$
15	13 14	mpbir	$⊢ Rel (X H Y)$

Metamath Proof Explorer