hofpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same Hom functor. (Contributed by Mario Carneiro, 26-Jan-2017)

	Ref	Expression
Hypotheses	hofpropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
	hofpropd.2	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
	hofpropd.c	$⊢ φ \to C \in Cat$
	hofpropd.d	$⊢ φ \to D \in Cat$
Assertion	hofpropd	$⊢ φ \to {Hom}_{F} (C) = {Hom}_{F} (D)$

Proof

Step	Hyp	Ref	Expression
1		hofpropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
2		hofpropd.2	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
3		hofpropd.c	$⊢ φ \to C \in Cat$
4		hofpropd.d	$⊢ φ \to D \in Cat$
5	1	homfeqbas	$⊢ φ \to {Base}_{C} = {Base}_{D}$
6	5	sqxpeqd	$⊢ φ \to {Base}_{C} \times {Base}_{C} = {Base}_{D} \times {Base}_{D}$
7	6	adantr	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to {Base}_{C} \times {Base}_{C} = {Base}_{D} \times {Base}_{D}$
8		eqid	$⊢ {Base}_{C} = {Base}_{C}$
9		eqid	$⊢ Hom (C) = Hom (C)$
10		eqid	$⊢ Hom (D) = Hom (D)$
11	1	adantr	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
12		xp1st	$⊢ y \in ({Base}_{C} \times {Base}_{C}) \to 1^{st} (y) \in {Base}_{C}$
13	12	ad2antll	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to 1^{st} (y) \in {Base}_{C}$
14		xp1st	$⊢ x \in ({Base}_{C} \times {Base}_{C}) \to 1^{st} (x) \in {Base}_{C}$
15	14	ad2antrl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to 1^{st} (x) \in {Base}_{C}$
16	8 9 10 11 13 15	homfeqval	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to 1^{st} (y) Hom (C) 1^{st} (x) = 1^{st} (y) Hom (D) 1^{st} (x)$
17		xp2nd	$⊢ x \in ({Base}_{C} \times {Base}_{C}) \to 2^{nd} (x) \in {Base}_{C}$
18	17	ad2antrl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to 2^{nd} (x) \in {Base}_{C}$
19		xp2nd	$⊢ y \in ({Base}_{C} \times {Base}_{C}) \to 2^{nd} (y) \in {Base}_{C}$
20	19	ad2antll	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to 2^{nd} (y) \in {Base}_{C}$
21	8 9 10 11 18 20	homfeqval	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to 2^{nd} (x) Hom (C) 2^{nd} (y) = 2^{nd} (x) Hom (D) 2^{nd} (y)$
22	21	adantr	$⊢ ((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land f \in (1^{st} (y) Hom (C) 1^{st} (x))) \to 2^{nd} (x) Hom (C) 2^{nd} (y) = 2^{nd} (x) Hom (D) 2^{nd} (y)$
23	8 9 10 11 15 18	homfeqval	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to 1^{st} (x) Hom (C) 2^{nd} (x) = 1^{st} (x) Hom (D) 2^{nd} (x)$
24		df-ov	$⊢ 1^{st} (x) Hom (C) 2^{nd} (x) = Hom (C) (⟨1^{st} (x), 2^{nd} (x)⟩)$
25		df-ov	$⊢ 1^{st} (x) Hom (D) 2^{nd} (x) = Hom (D) (⟨1^{st} (x), 2^{nd} (x)⟩)$
26	23 24 25	3eqtr3g	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to Hom (C) (⟨1^{st} (x), 2^{nd} (x)⟩) = Hom (D) (⟨1^{st} (x), 2^{nd} (x)⟩)$
27		1st2nd2	$⊢ x \in ({Base}_{C} \times {Base}_{C}) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
28	27	ad2antrl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
29	28	fveq2d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to Hom (C) (x) = Hom (C) (⟨1^{st} (x), 2^{nd} (x)⟩)$
30	28	fveq2d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to Hom (D) (x) = Hom (D) (⟨1^{st} (x), 2^{nd} (x)⟩)$
31	26 29 30	3eqtr4d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to Hom (C) (x) = Hom (D) (x)$
32	31	adantr	$⊢ ((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \to Hom (C) (x) = Hom (D) (x)$
33		eqid	$⊢ comp (C) = comp (C)$
34		eqid	$⊢ comp (D) = comp (D)$
35	11	ad2antrr	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
36	2	ad3antrrr	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
37	13	ad2antrr	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to 1^{st} (y) \in {Base}_{C}$
38	15	ad2antrr	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to 1^{st} (x) \in {Base}_{C}$
39	20	ad2antrr	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to 2^{nd} (y) \in {Base}_{C}$
40		simplrl	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to f \in (1^{st} (y) Hom (C) 1^{st} (x))$
41	28	ad2antrr	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
42	41	oveq1d	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to x comp (C) 2^{nd} (y) = ⟨1^{st} (x), 2^{nd} (x)⟩ comp (C) 2^{nd} (y)$
43	42	oveqd	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to g (x comp (C) 2^{nd} (y)) h = g (⟨1^{st} (x), 2^{nd} (x)⟩ comp (C) 2^{nd} (y)) h$
44	3	ad3antrrr	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to C \in Cat$
45	18	ad2antrr	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to 2^{nd} (x) \in {Base}_{C}$
46	29	adantr	$⊢ ((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \to Hom (C) (x) = Hom (C) (⟨1^{st} (x), 2^{nd} (x)⟩)$
47	46 24	eqtr4di	$⊢ ((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \to Hom (C) (x) = 1^{st} (x) Hom (C) 2^{nd} (x)$
48	47	eleq2d	$⊢ ((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \to (h \in Hom (C) (x) \leftrightarrow h \in (1^{st} (x) Hom (C) 2^{nd} (x)))$
49	48	biimpa	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to h \in (1^{st} (x) Hom (C) 2^{nd} (x))$
50		simplrr	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to g \in (2^{nd} (x) Hom (C) 2^{nd} (y))$
51	8 9 33 44 38 45 39 49 50	catcocl	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to g (⟨1^{st} (x), 2^{nd} (x)⟩ comp (C) 2^{nd} (y)) h \in (1^{st} (x) Hom (C) 2^{nd} (y))$
52	43 51	eqeltrd	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to g (x comp (C) 2^{nd} (y)) h \in (1^{st} (x) Hom (C) 2^{nd} (y))$
53	8 9 33 34 35 36 37 38 39 40 52	comfeqval	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to (g (x comp (C) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (C) 2^{nd} (y)) f = (g (x comp (C) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (D) 2^{nd} (y)) f$
54	8 9 33 34 35 36 38 45 39 49 50	comfeqval	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to g (⟨1^{st} (x), 2^{nd} (x)⟩ comp (C) 2^{nd} (y)) h = g (⟨1^{st} (x), 2^{nd} (x)⟩ comp (D) 2^{nd} (y)) h$
55	41	oveq1d	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to x comp (D) 2^{nd} (y) = ⟨1^{st} (x), 2^{nd} (x)⟩ comp (D) 2^{nd} (y)$
56	55	oveqd	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to g (x comp (D) 2^{nd} (y)) h = g (⟨1^{st} (x), 2^{nd} (x)⟩ comp (D) 2^{nd} (y)) h$
57	54 43 56	3eqtr4d	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to g (x comp (C) 2^{nd} (y)) h = g (x comp (D) 2^{nd} (y)) h$
58	57	oveq1d	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to (g (x comp (C) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (D) 2^{nd} (y)) f = (g (x comp (D) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (D) 2^{nd} (y)) f$
59	53 58	eqtrd	$⊢ (((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \land h \in Hom (C) (x)) \to (g (x comp (C) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (C) 2^{nd} (y)) f = (g (x comp (D) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (D) 2^{nd} (y)) f$
60	32 59	mpteq12dva	$⊢ ((φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \land (f \in (1^{st} (y) Hom (C) 1^{st} (x)) \land g \in (2^{nd} (x) Hom (C) 2^{nd} (y)))) \to (h \in Hom (C) (x) ⟼ (g (x comp (C) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (C) 2^{nd} (y)) f) = (h \in Hom (D) (x) ⟼ (g (x comp (D) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (D) 2^{nd} (y)) f)$
61	16 22 60	mpoeq123dva	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to (f \in (1^{st} (y) Hom (C) 1^{st} (x)), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ (h \in Hom (C) (x) ⟼ (g (x comp (C) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (C) 2^{nd} (y)) f)) = (f \in (1^{st} (y) Hom (D) 1^{st} (x)), g \in (2^{nd} (x) Hom (D) 2^{nd} (y)) ⟼ (h \in Hom (D) (x) ⟼ (g (x comp (D) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (D) 2^{nd} (y)) f))$
62	6 7 61	mpoeq123dva	$⊢ φ \to (x \in ({Base}_{C} \times {Base}_{C}), y \in ({Base}_{C} \times {Base}_{C}) ⟼ (f \in (1^{st} (y) Hom (C) 1^{st} (x)), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ (h \in Hom (C) (x) ⟼ (g (x comp (C) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (C) 2^{nd} (y)) f))) = (x \in ({Base}_{D} \times {Base}_{D}), y \in ({Base}_{D} \times {Base}_{D}) ⟼ (f \in (1^{st} (y) Hom (D) 1^{st} (x)), g \in (2^{nd} (x) Hom (D) 2^{nd} (y)) ⟼ (h \in Hom (D) (x) ⟼ (g (x comp (D) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (D) 2^{nd} (y)) f)))$
63	1 62	opeq12d	$⊢ φ \to ⟨{Hom}_{𝑓} (C), (x \in ({Base}_{C} \times {Base}_{C}), y \in ({Base}_{C} \times {Base}_{C}) ⟼ (f \in (1^{st} (y) Hom (C) 1^{st} (x)), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ (h \in Hom (C) (x) ⟼ (g (x comp (C) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (C) 2^{nd} (y)) f)))⟩ = ⟨{Hom}_{𝑓} (D), (x \in ({Base}_{D} \times {Base}_{D}), y \in ({Base}_{D} \times {Base}_{D}) ⟼ (f \in (1^{st} (y) Hom (D) 1^{st} (x)), g \in (2^{nd} (x) Hom (D) 2^{nd} (y)) ⟼ (h \in Hom (D) (x) ⟼ (g (x comp (D) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (D) 2^{nd} (y)) f)))⟩$
64		eqid	$⊢ {Hom}_{F} (C) = {Hom}_{F} (C)$
65	64 3 8 9 33	hofval	$⊢ φ \to {Hom}_{F} (C) = ⟨{Hom}_{𝑓} (C), (x \in ({Base}_{C} \times {Base}_{C}), y \in ({Base}_{C} \times {Base}_{C}) ⟼ (f \in (1^{st} (y) Hom (C) 1^{st} (x)), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ (h \in Hom (C) (x) ⟼ (g (x comp (C) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (C) 2^{nd} (y)) f)))⟩$
66		eqid	$⊢ {Hom}_{F} (D) = {Hom}_{F} (D)$
67		eqid	$⊢ {Base}_{D} = {Base}_{D}$
68	66 4 67 10 34	hofval	$⊢ φ \to {Hom}_{F} (D) = ⟨{Hom}_{𝑓} (D), (x \in ({Base}_{D} \times {Base}_{D}), y \in ({Base}_{D} \times {Base}_{D}) ⟼ (f \in (1^{st} (y) Hom (D) 1^{st} (x)), g \in (2^{nd} (x) Hom (D) 2^{nd} (y)) ⟼ (h \in Hom (D) (x) ⟼ (g (x comp (D) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (D) 2^{nd} (y)) f)))⟩$
69	63 65 68	3eqtr4d	$⊢ φ \to {Hom}_{F} (C) = {Hom}_{F} (D)$

Metamath Proof Explorer

Theorem hofpropd

Proof