hofcl

Description: Closure of the Hom functor. Note that the codomain is the category SetCatU for any universe U which contains each Hom-set. This corresponds to the assertion that C be locally small (with respect to U ). (Contributed by Mario Carneiro, 15-Jan-2017)

	Ref	Expression
Hypotheses	hofcl.m	$⊢ M = {Hom}_{F} (C)$
	hofcl.o	$⊢ O = oppCat (C)$
	hofcl.d	$⊢ D = SetCat (U)$
	hofcl.c	$⊢ φ \to C \in Cat$
	hofcl.u	$⊢ φ \to U \in V$
	hofcl.h	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
Assertion	hofcl	$⊢ φ \to M \in ((O \times_{c} C) Func D)$

Proof

Step	Hyp	Ref	Expression
1		hofcl.m	$⊢ M = {Hom}_{F} (C)$
2		hofcl.o	$⊢ O = oppCat (C)$
3		hofcl.d	$⊢ D = SetCat (U)$
4		hofcl.c	$⊢ φ \to C \in Cat$
5		hofcl.u	$⊢ φ \to U \in V$
6		hofcl.h	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
7		eqid	$⊢ {Base}_{C} = {Base}_{C}$
8		eqid	$⊢ Hom (C) = Hom (C)$
9		eqid	$⊢ comp (C) = comp (C)$
10	1 4 7 8 9	hofval	$⊢ φ \to M = ⟨{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)))⟩$
11		fvex	$⊢ {Hom}_{𝑓} (C) \in V$
12		fvex	$⊢ {Base}_{C} \in V$
13	12 12	xpex	$⊢ {Base}_{C} \times {Base}_{C} \in V$
14	13 13	mpoex	$⊢ (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))) \in V$
15	11 14	op2ndd	$⊢ M = ⟨{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)))⟩ \to 2^{nd} (M) = (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)))$
16	10 15	syl	$⊢ φ \to 2^{nd} (M) = (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)))$
17	16	opeq2d	$⊢ φ \to ⟨{Hom}_{𝑓} (C), 2^{nd} (M)⟩ = ⟨{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)))⟩$
18	10 17	eqtr4d	$⊢ φ \to M = ⟨{Hom}_{𝑓} (C), 2^{nd} (M)⟩$
19		eqid	$⊢ O \times_{c} C = O \times_{c} C$
20	2 7	oppcbas	$⊢ {Base}_{C} = {Base}_{O}$
21	19 20 7	xpcbas	$⊢ {Base}_{C} \times {Base}_{C} = {Base}_{(O \times_{c} C)}$
22		eqid	$⊢ {Base}_{D} = {Base}_{D}$
23		eqid	$⊢ Hom (O \times_{c} C) = Hom (O \times_{c} C)$
24		eqid	$⊢ Hom (D) = Hom (D)$
25		eqid	$⊢ Id (O \times_{c} C) = Id (O \times_{c} C)$
26		eqid	$⊢ Id (D) = Id (D)$
27		eqid	$⊢ comp (O \times_{c} C) = comp (O \times_{c} C)$
28		eqid	$⊢ comp (D) = comp (D)$
29	2	oppccat	$⊢ C \in Cat \to O \in Cat$
30	4 29	syl	$⊢ φ \to O \in Cat$
31	19 30 4	xpccat	$⊢ φ \to O \times_{c} C \in Cat$
32	3	setccat	$⊢ U \in V \to D \in Cat$
33	5 32	syl	$⊢ φ \to D \in Cat$
34		eqid	$⊢ {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C)$
35	34 7	homffn	$⊢ {Hom}_{𝑓} (C) Fn ({Base}_{C} \times {Base}_{C})$
36	35	a1i	$⊢ φ \to {Hom}_{𝑓} (C) Fn ({Base}_{C} \times {Base}_{C})$
37		df-f	$⊢ {Hom}_{𝑓} (C) : {Base}_{C} \times {Base}_{C} ⟶ U \leftrightarrow ({Hom}_{𝑓} (C) Fn ({Base}_{C} \times {Base}_{C}) \land ran {Hom}_{𝑓} (C) \subseteq U)$
38	36 6 37	sylanbrc	$⊢ φ \to {Hom}_{𝑓} (C) : {Base}_{C} \times {Base}_{C} ⟶ U$
39	3 5	setcbas	$⊢ φ \to U = {Base}_{D}$
40	39	feq3d	$⊢ φ \to ({Hom}_{𝑓} (C) : {Base}_{C} \times {Base}_{C} ⟶ U \leftrightarrow {Hom}_{𝑓} (C) : {Base}_{C} \times {Base}_{C} ⟶ {Base}_{D})$
41	38 40	mpbid	$⊢ φ \to {Hom}_{𝑓} (C) : {Base}_{C} \times {Base}_{C} ⟶ {Base}_{D}$
42		eqid	$⊢ (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}_{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)))$
43		ovex	$⊢ 1^{st} (y) Hom (C) 1^{st} (x) \in V$
44		ovex	$⊢ 2^{nd} (x) Hom (C) 2^{nd} (y) \in V$
45	43 44	mpoex	$⊢ (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)) \in V$
46	42 45	fnmpoi	$⊢ (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))) Fn (({Base}_{C} \times {Base}_{C}) \times ({Base}_{C} \times {Base}_{C}))$
47	16	fneq1d	$⊢ φ \to (2^{nd} (M) Fn (({Base}_{C} \times {Base}_{C}) \times ({Base}_{C} \times {Base}_{C})) \leftrightarrow (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))) Fn (({Base}_{C} \times {Base}_{C}) \times ({Base}_{C} \times {Base}_{C})))$
48	46 47	mpbiri	$⊢ φ \to 2^{nd} (M) Fn (({Base}_{C} \times {Base}_{C}) \times ({Base}_{C} \times {Base}_{C}))$
49	4	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$
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)))) \to y \in ({Base}_{C} \times {Base}_{C})$
51		xp1st	$⊢ y \in ({Base}_{C} \times {Base}_{C}) \to 1^{st} (y) \in {Base}_{C}$
52	50 51	syl	$⊢ ((φ \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 1^{st} (y) \in {Base}_{C}$
53	52	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)))) \land h \in Hom (C) (x)) \to 1^{st} (y) \in {Base}_{C}$
54		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)))) \to x \in ({Base}_{C} \times {Base}_{C})$
55		xp1st	$⊢ x \in ({Base}_{C} \times {Base}_{C}) \to 1^{st} (x) \in {Base}_{C}$
56	54 55	syl	$⊢ ((φ \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 1^{st} (x) \in {Base}_{C}$
57	56	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)))) \land h \in Hom (C) (x)) \to 1^{st} (x) \in {Base}_{C}$
58		xp2nd	$⊢ y \in ({Base}_{C} \times {Base}_{C}) \to 2^{nd} (y) \in {Base}_{C}$
59	50 58	syl	$⊢ ((φ \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 2^{nd} (y) \in {Base}_{C}$
60	59	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)))) \land h \in Hom (C) (x)) \to 2^{nd} (y) \in {Base}_{C}$
61		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))$
62		1st2nd2	$⊢ x \in ({Base}_{C} \times {Base}_{C}) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
63	54 62	syl	$⊢ ((φ \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 x = ⟨1^{st} (x), 2^{nd} (x)⟩$
64	63	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)))) \land h \in Hom (C) (x)) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
65	64	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)$
66	65	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$
67		xp2nd	$⊢ x \in ({Base}_{C} \times {Base}_{C}) \to 2^{nd} (x) \in {Base}_{C}$
68	54 67	syl	$⊢ ((φ \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 2^{nd} (x) \in {Base}_{C}$
69	68	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)))) \land h \in Hom (C) (x)) \to 2^{nd} (x) \in {Base}_{C}$
70	63	fveq2d	$⊢ ((φ \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)⟩)$
71		df-ov	$⊢ 1^{st} (x) Hom (C) 2^{nd} (x) = Hom (C) (⟨1^{st} (x), 2^{nd} (x)⟩)$
72	70 71	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)$
73	72	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)))$
74	73	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))$
75		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))$
76	7 8 9 49 57 69 60 74 75	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))$
77	66 76	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))$
78	7 8 9 49 53 57 60 61 77	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 (x comp (C) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (C) 2^{nd} (y)) f \in (1^{st} (y) Hom (C) 2^{nd} (y))$
79		1st2nd2	$⊢ y \in ({Base}_{C} \times {Base}_{C}) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
80	50 79	syl	$⊢ ((φ \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 y = ⟨1^{st} (y), 2^{nd} (y)⟩$
81	80	fveq2d	$⊢ ((φ \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) (y) = Hom (C) (⟨1^{st} (y), 2^{nd} (y)⟩)$
82		df-ov	$⊢ 1^{st} (y) Hom (C) 2^{nd} (y) = Hom (C) (⟨1^{st} (y), 2^{nd} (y)⟩)$
83	81 82	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) (y) = 1^{st} (y) Hom (C) 2^{nd} (y)$
84	83	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)))) \land h \in Hom (C) (x)) \to Hom (C) (y) = 1^{st} (y) Hom (C) 2^{nd} (y)$
85	78 84	eleqtrrd	$⊢ (((φ \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 \in Hom (C) (y)$
86	85	fmpttd	$⊢ ((φ \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) : Hom (C) (x) ⟶ Hom (C) (y)$
87	5	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)))) \to U \in V$
88	34 7 8 56 68	homfval	$⊢ ((φ \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 1^{st} (x) {Hom}_{𝑓} (C) 2^{nd} (x) = 1^{st} (x) Hom (C) 2^{nd} (x)$
89	63	fveq2d	$⊢ ((φ \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)⟩)$
90		df-ov	$⊢ 1^{st} (x) {Hom}_{𝑓} (C) 2^{nd} (x) = {Hom}_{𝑓} (C) (⟨1^{st} (x), 2^{nd} (x)⟩)$
91	89 90	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)$
92	88 91 72	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)))) \to {Hom}_{𝑓} (C) (x) = Hom (C) (x)$
93	38	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)))) \to {Hom}_{𝑓} (C) : {Base}_{C} \times {Base}_{C} ⟶ U$
94	93 54	ffvelrnd	$⊢ ((φ \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) \in U$
95	92 94	eqeltrrd	$⊢ ((φ \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) \in U$
96	34 7 8 52 59	homfval	$⊢ ((φ \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 1^{st} (y) {Hom}_{𝑓} (C) 2^{nd} (y) = 1^{st} (y) Hom (C) 2^{nd} (y)$
97	80	fveq2d	$⊢ ((φ \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) (y) = {Hom}_{𝑓} (C) (⟨1^{st} (y), 2^{nd} (y)⟩)$
98		df-ov	$⊢ 1^{st} (y) {Hom}_{𝑓} (C) 2^{nd} (y) = {Hom}_{𝑓} (C) (⟨1^{st} (y), 2^{nd} (y)⟩)$
99	97 98	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) (y) = 1^{st} (y) {Hom}_{𝑓} (C) 2^{nd} (y)$
100	96 99 83	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)))) \to {Hom}_{𝑓} (C) (y) = Hom (C) (y)$
101	93 50	ffvelrnd	$⊢ ((φ \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) (y) \in U$
102	100 101	eqeltrrd	$⊢ ((φ \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) (y) \in U$
103	3 87 24 95 102	elsetchom	$⊢ ((φ \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) \in (Hom (C) (x) Hom (D) Hom (C) (y)) \leftrightarrow (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 (C) (x) ⟶ Hom (C) (y))$
104	86 103	mpbird	$⊢ ((φ \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) \in (Hom (C) (x) Hom (D) Hom (C) (y))$
105	92 100	oveq12d	$⊢ ((φ \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) {Hom}_{𝑓} (C) (y) = Hom (C) (x) Hom (D) Hom (C) (y)$
106	104 105	eleqtrrd	$⊢ ((φ \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) \in ({Hom}_{𝑓} (C) (x) Hom (D) {Hom}_{𝑓} (C) (y))$
107	106	ralrimivva	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to \forall f \in (1^{st} (y) Hom (C) 1^{st} (x)) \forall 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) \in ({Hom}_{𝑓} (C) (x) Hom (D) {Hom}_{𝑓} (C) (y))$
108		eqid	$⊢ (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 (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))$
109	108	fmpo	$⊢ \forall f \in (1^{st} (y) Hom (C) 1^{st} (x)) \forall 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) \in ({Hom}_{𝑓} (C) (x) Hom (D) {Hom}_{𝑓} (C) (y)) \leftrightarrow (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)) : (1^{st} (y) Hom (C) 1^{st} (x)) \times (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟶ {Hom}_{𝑓} (C) (x) Hom (D) {Hom}_{𝑓} (C) (y)$
110	107 109	sylib	$⊢ (φ \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)) : (1^{st} (y) Hom (C) 1^{st} (x)) \times (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟶ {Hom}_{𝑓} (C) (x) Hom (D) {Hom}_{𝑓} (C) (y)$
111	16	oveqd	$⊢ φ \to x 2^{nd} (M) y = x (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))) y$
112	42	ovmpt4g	$⊢ (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)), 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)) \in V) \to x (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))) y = (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))$
113	45 112	mp3an3	$⊢ (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C})) \to x (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))) y = (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))$
114	111 113	sylan9eq	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to x 2^{nd} (M) y = (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))$
115		eqid	$⊢ Hom (O) = Hom (O)$
116		simprl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to x \in ({Base}_{C} \times {Base}_{C})$
117		simprr	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to y \in ({Base}_{C} \times {Base}_{C})$
118	19 21 115 8 23 116 117	xpchom	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to x Hom (O \times_{c} C) y = (1^{st} (x) Hom (O) 1^{st} (y)) \times (2^{nd} (x) Hom (C) 2^{nd} (y))$
119	8 2	oppchom	$⊢ 1^{st} (x) Hom (O) 1^{st} (y) = 1^{st} (y) Hom (C) 1^{st} (x)$
120	119	xpeq1i	$⊢ (1^{st} (x) Hom (O) 1^{st} (y)) \times (2^{nd} (x) Hom (C) 2^{nd} (y)) = (1^{st} (y) Hom (C) 1^{st} (x)) \times (2^{nd} (x) Hom (C) 2^{nd} (y))$
121	118 120	eqtrdi	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to x Hom (O \times_{c} C) y = (1^{st} (y) Hom (C) 1^{st} (x)) \times (2^{nd} (x) Hom (C) 2^{nd} (y))$
122	114 121	feq12d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to ((x 2^{nd} (M) y) : x Hom (O \times_{c} C) y ⟶ {Hom}_{𝑓} (C) (x) Hom (D) {Hom}_{𝑓} (C) (y) \leftrightarrow (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)) : (1^{st} (y) Hom (C) 1^{st} (x)) \times (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟶ {Hom}_{𝑓} (C) (x) Hom (D) {Hom}_{𝑓} (C) (y))$
123	110 122	mpbird	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}))) \to (x 2^{nd} (M) y) : x Hom (O \times_{c} C) y ⟶ {Hom}_{𝑓} (C) (x) Hom (D) {Hom}_{𝑓} (C) (y)$
124		eqid	$⊢ Id (C) = Id (C)$
125	4	ad2antrr	$⊢ ((φ \land x \in ({Base}_{C} \times {Base}_{C})) \land f \in (1^{st} (x) Hom (C) 2^{nd} (x))) \to C \in Cat$
126	55	adantl	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to 1^{st} (x) \in {Base}_{C}$
127	126	adantr	$⊢ ((φ \land x \in ({Base}_{C} \times {Base}_{C})) \land f \in (1^{st} (x) Hom (C) 2^{nd} (x))) \to 1^{st} (x) \in {Base}_{C}$
128	67	adantl	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to 2^{nd} (x) \in {Base}_{C}$
129	128	adantr	$⊢ ((φ \land x \in ({Base}_{C} \times {Base}_{C})) \land f \in (1^{st} (x) Hom (C) 2^{nd} (x))) \to 2^{nd} (x) \in {Base}_{C}$
130		simpr	$⊢ ((φ \land x \in ({Base}_{C} \times {Base}_{C})) \land f \in (1^{st} (x) Hom (C) 2^{nd} (x))) \to f \in (1^{st} (x) Hom (C) 2^{nd} (x))$
131	7 8 124 125 127 9 129 130	catlid	$⊢ ((φ \land x \in ({Base}_{C} \times {Base}_{C})) \land f \in (1^{st} (x) Hom (C) 2^{nd} (x))) \to Id (C) (2^{nd} (x)) (⟨1^{st} (x), 2^{nd} (x)⟩ comp (C) 2^{nd} (x)) f = f$
132	131	oveq1d	$⊢ ((φ \land x \in ({Base}_{C} \times {Base}_{C})) \land f \in (1^{st} (x) Hom (C) 2^{nd} (x))) \to (Id (C) (2^{nd} (x)) (⟨1^{st} (x), 2^{nd} (x)⟩ comp (C) 2^{nd} (x)) f) (⟨1^{st} (x), 1^{st} (x)⟩ comp (C) 2^{nd} (x)) Id (C) (1^{st} (x)) = f (⟨1^{st} (x), 1^{st} (x)⟩ comp (C) 2^{nd} (x)) Id (C) (1^{st} (x))$
133	7 8 124 125 127 9 129 130	catrid	$⊢ ((φ \land x \in ({Base}_{C} \times {Base}_{C})) \land f \in (1^{st} (x) Hom (C) 2^{nd} (x))) \to f (⟨1^{st} (x), 1^{st} (x)⟩ comp (C) 2^{nd} (x)) Id (C) (1^{st} (x)) = f$
134	132 133	eqtrd	$⊢ ((φ \land x \in ({Base}_{C} \times {Base}_{C})) \land f \in (1^{st} (x) Hom (C) 2^{nd} (x))) \to (Id (C) (2^{nd} (x)) (⟨1^{st} (x), 2^{nd} (x)⟩ comp (C) 2^{nd} (x)) f) (⟨1^{st} (x), 1^{st} (x)⟩ comp (C) 2^{nd} (x)) Id (C) (1^{st} (x)) = f$
135	134	mpteq2dva	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to (f \in (1^{st} (x) Hom (C) 2^{nd} (x)) ⟼ (Id (C) (2^{nd} (x)) (⟨1^{st} (x), 2^{nd} (x)⟩ comp (C) 2^{nd} (x)) f) (⟨1^{st} (x), 1^{st} (x)⟩ comp (C) 2^{nd} (x)) Id (C) (1^{st} (x))) = (f \in (1^{st} (x) Hom (C) 2^{nd} (x)) ⟼ f)$
136		df-ov	$⊢ Id (C) (1^{st} (x)) (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (x), 2^{nd} (x)⟩) Id (C) (2^{nd} (x)) = (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (x), 2^{nd} (x)⟩) (⟨Id (C) (1^{st} (x)), Id (C) (2^{nd} (x))⟩)$
137	4	adantr	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to C \in Cat$
138	7 8 124 137 126	catidcl	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to Id (C) (1^{st} (x)) \in (1^{st} (x) Hom (C) 1^{st} (x))$
139	7 8 124 137 128	catidcl	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to Id (C) (2^{nd} (x)) \in (2^{nd} (x) Hom (C) 2^{nd} (x))$
140	1 137 7 8 126 128 126 128 9 138 139	hof2val	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to Id (C) (1^{st} (x)) (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (x), 2^{nd} (x)⟩) Id (C) (2^{nd} (x)) = (f \in (1^{st} (x) Hom (C) 2^{nd} (x)) ⟼ (Id (C) (2^{nd} (x)) (⟨1^{st} (x), 2^{nd} (x)⟩ comp (C) 2^{nd} (x)) f) (⟨1^{st} (x), 1^{st} (x)⟩ comp (C) 2^{nd} (x)) Id (C) (1^{st} (x)))$
141	136 140	syl5eqr	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (x), 2^{nd} (x)⟩) (⟨Id (C) (1^{st} (x)), Id (C) (2^{nd} (x))⟩) = (f \in (1^{st} (x) Hom (C) 2^{nd} (x)) ⟼ (Id (C) (2^{nd} (x)) (⟨1^{st} (x), 2^{nd} (x)⟩ comp (C) 2^{nd} (x)) f) (⟨1^{st} (x), 1^{st} (x)⟩ comp (C) 2^{nd} (x)) Id (C) (1^{st} (x)))$
142	62	adantl	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
143	142	fveq2d	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to {Hom}_{𝑓} (C) (x) = {Hom}_{𝑓} (C) (⟨1^{st} (x), 2^{nd} (x)⟩)$
144	143 90	eqtr4di	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to {Hom}_{𝑓} (C) (x) = 1^{st} (x) {Hom}_{𝑓} (C) 2^{nd} (x)$
145	34 7 8 126 128	homfval	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to 1^{st} (x) {Hom}_{𝑓} (C) 2^{nd} (x) = 1^{st} (x) Hom (C) 2^{nd} (x)$
146	144 145	eqtrd	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to {Hom}_{𝑓} (C) (x) = 1^{st} (x) Hom (C) 2^{nd} (x)$
147	146	reseq2d	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to {I ↾}_{{Hom}_{𝑓} (C) (x)} = {I ↾}_{(1^{st} (x) Hom (C) 2^{nd} (x))}$
148		mptresid	$⊢ {I ↾}_{(1^{st} (x) Hom (C) 2^{nd} (x))} = (f \in (1^{st} (x) Hom (C) 2^{nd} (x)) ⟼ f)$
149	147 148	eqtrdi	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to {I ↾}_{{Hom}_{𝑓} (C) (x)} = (f \in (1^{st} (x) Hom (C) 2^{nd} (x)) ⟼ f)$
150	135 141 149	3eqtr4d	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (x), 2^{nd} (x)⟩) (⟨Id (C) (1^{st} (x)), Id (C) (2^{nd} (x))⟩) = {I ↾}_{{Hom}_{𝑓} (C) (x)}$
151	142 142	oveq12d	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to x 2^{nd} (M) x = ⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (x), 2^{nd} (x)⟩$
152	142	fveq2d	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to Id (O \times_{c} C) (x) = Id (O \times_{c} C) (⟨1^{st} (x), 2^{nd} (x)⟩)$
153	30	adantr	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to O \in Cat$
154		eqid	$⊢ Id (O) = Id (O)$
155	19 153 137 20 7 154 124 25 126 128	xpcid	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to Id (O \times_{c} C) (⟨1^{st} (x), 2^{nd} (x)⟩) = ⟨Id (O) (1^{st} (x)), Id (C) (2^{nd} (x))⟩$
156	2 124	oppcid	$⊢ C \in Cat \to Id (O) = Id (C)$
157	137 156	syl	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to Id (O) = Id (C)$
158	157	fveq1d	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to Id (O) (1^{st} (x)) = Id (C) (1^{st} (x))$
159	158	opeq1d	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to ⟨Id (O) (1^{st} (x)), Id (C) (2^{nd} (x))⟩ = ⟨Id (C) (1^{st} (x)), Id (C) (2^{nd} (x))⟩$
160	152 155 159	3eqtrd	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to Id (O \times_{c} C) (x) = ⟨Id (C) (1^{st} (x)), Id (C) (2^{nd} (x))⟩$
161	151 160	fveq12d	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to (x 2^{nd} (M) x) (Id (O \times_{c} C) (x)) = (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (x), 2^{nd} (x)⟩) (⟨Id (C) (1^{st} (x)), Id (C) (2^{nd} (x))⟩)$
162	5	adantr	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to U \in V$
163	38	ffvelrnda	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to {Hom}_{𝑓} (C) (x) \in U$
164	3 26 162 163	setcid	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to Id (D) ({Hom}_{𝑓} (C) (x)) = {I ↾}_{{Hom}_{𝑓} (C) (x)}$
165	150 161 164	3eqtr4d	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{C})) \to (x 2^{nd} (M) x) (Id (O \times_{c} C) (x)) = Id (D) ({Hom}_{𝑓} (C) (x))$
166	4	3ad2ant1	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to C \in Cat$
167	5	3ad2ant1	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to U \in V$
168	6	3ad2ant1	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to ran {Hom}_{𝑓} (C) \subseteq U$
169		simp21	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to x \in ({Base}_{C} \times {Base}_{C})$
170	169 55	syl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to 1^{st} (x) \in {Base}_{C}$
171	169 67	syl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to 2^{nd} (x) \in {Base}_{C}$
172		simp22	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to y \in ({Base}_{C} \times {Base}_{C})$
173	172 51	syl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to 1^{st} (y) \in {Base}_{C}$
174	172 58	syl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to 2^{nd} (y) \in {Base}_{C}$
175		simp23	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to z \in ({Base}_{C} \times {Base}_{C})$
176		xp1st	$⊢ z \in ({Base}_{C} \times {Base}_{C}) \to 1^{st} (z) \in {Base}_{C}$
177	175 176	syl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to 1^{st} (z) \in {Base}_{C}$
178		xp2nd	$⊢ z \in ({Base}_{C} \times {Base}_{C}) \to 2^{nd} (z) \in {Base}_{C}$
179	175 178	syl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to 2^{nd} (z) \in {Base}_{C}$
180		simp3l	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to f \in (x Hom (O \times_{c} C) y)$
181	19 21 115 8 23 169 172	xpchom	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to x Hom (O \times_{c} C) y = (1^{st} (x) Hom (O) 1^{st} (y)) \times (2^{nd} (x) Hom (C) 2^{nd} (y))$
182	180 181	eleqtrd	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to f \in ((1^{st} (x) Hom (O) 1^{st} (y)) \times (2^{nd} (x) Hom (C) 2^{nd} (y)))$
183		xp1st	$⊢ f \in ((1^{st} (x) Hom (O) 1^{st} (y)) \times (2^{nd} (x) Hom (C) 2^{nd} (y))) \to 1^{st} (f) \in (1^{st} (x) Hom (O) 1^{st} (y))$
184	182 183	syl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to 1^{st} (f) \in (1^{st} (x) Hom (O) 1^{st} (y))$
185	184 119	eleqtrdi	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to 1^{st} (f) \in (1^{st} (y) Hom (C) 1^{st} (x))$
186		xp2nd	$⊢ f \in ((1^{st} (x) Hom (O) 1^{st} (y)) \times (2^{nd} (x) Hom (C) 2^{nd} (y))) \to 2^{nd} (f) \in (2^{nd} (x) Hom (C) 2^{nd} (y))$
187	182 186	syl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to 2^{nd} (f) \in (2^{nd} (x) Hom (C) 2^{nd} (y))$
188		simp3r	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to g \in (y Hom (O \times_{c} C) z)$
189	19 21 115 8 23 172 175	xpchom	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to y Hom (O \times_{c} C) z = (1^{st} (y) Hom (O) 1^{st} (z)) \times (2^{nd} (y) Hom (C) 2^{nd} (z))$
190	188 189	eleqtrd	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to g \in ((1^{st} (y) Hom (O) 1^{st} (z)) \times (2^{nd} (y) Hom (C) 2^{nd} (z)))$
191		xp1st	$⊢ g \in ((1^{st} (y) Hom (O) 1^{st} (z)) \times (2^{nd} (y) Hom (C) 2^{nd} (z))) \to 1^{st} (g) \in (1^{st} (y) Hom (O) 1^{st} (z))$
192	190 191	syl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to 1^{st} (g) \in (1^{st} (y) Hom (O) 1^{st} (z))$
193	8 2	oppchom	$⊢ 1^{st} (y) Hom (O) 1^{st} (z) = 1^{st} (z) Hom (C) 1^{st} (y)$
194	192 193	eleqtrdi	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to 1^{st} (g) \in (1^{st} (z) Hom (C) 1^{st} (y))$
195		xp2nd	$⊢ g \in ((1^{st} (y) Hom (O) 1^{st} (z)) \times (2^{nd} (y) Hom (C) 2^{nd} (z))) \to 2^{nd} (g) \in (2^{nd} (y) Hom (C) 2^{nd} (z))$
196	190 195	syl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to 2^{nd} (g) \in (2^{nd} (y) Hom (C) 2^{nd} (z))$
197	1 2 3 166 167 168 7 8 170 171 173 174 177 179 185 187 194 196	hofcllem	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to (1^{st} (f) (⟨1^{st} (z), 1^{st} (y)⟩ comp (C) 1^{st} (x)) 1^{st} (g)) (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (z), 2^{nd} (z)⟩) (2^{nd} (g) (⟨2^{nd} (x), 2^{nd} (y)⟩ comp (C) 2^{nd} (z)) 2^{nd} (f)) = (1^{st} (g) (⟨1^{st} (y), 2^{nd} (y)⟩ 2^{nd} (M) ⟨1^{st} (z), 2^{nd} (z)⟩) 2^{nd} (g)) (⟨1^{st} (x) Hom (C) 2^{nd} (x), 1^{st} (y) Hom (C) 2^{nd} (y)⟩ comp (D) (1^{st} (z) Hom (C) 2^{nd} (z))) (1^{st} (f) (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (y), 2^{nd} (y)⟩) 2^{nd} (f))$
198	169 62	syl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
199		1st2nd2	$⊢ z \in ({Base}_{C} \times {Base}_{C}) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
200	175 199	syl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
201	198 200	oveq12d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to x 2^{nd} (M) z = ⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (z), 2^{nd} (z)⟩$
202	172 79	syl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
203	198 202	opeq12d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to ⟨x, y⟩ = ⟨⟨1^{st} (x), 2^{nd} (x)⟩, ⟨1^{st} (y), 2^{nd} (y)⟩⟩$
204	203 200	oveq12d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to ⟨x, y⟩ comp (O \times_{c} C) z = ⟨⟨1^{st} (x), 2^{nd} (x)⟩, ⟨1^{st} (y), 2^{nd} (y)⟩⟩ comp (O \times_{c} C) ⟨1^{st} (z), 2^{nd} (z)⟩$
205		1st2nd2	$⊢ g \in ((1^{st} (y) Hom (O) 1^{st} (z)) \times (2^{nd} (y) Hom (C) 2^{nd} (z))) \to g = ⟨1^{st} (g), 2^{nd} (g)⟩$
206	190 205	syl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to g = ⟨1^{st} (g), 2^{nd} (g)⟩$
207		1st2nd2	$⊢ f \in ((1^{st} (x) Hom (O) 1^{st} (y)) \times (2^{nd} (x) Hom (C) 2^{nd} (y))) \to f = ⟨1^{st} (f), 2^{nd} (f)⟩$
208	182 207	syl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to f = ⟨1^{st} (f), 2^{nd} (f)⟩$
209	204 206 208	oveq123d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to g (⟨x, y⟩ comp (O \times_{c} C) z) f = ⟨1^{st} (g), 2^{nd} (g)⟩ (⟨⟨1^{st} (x), 2^{nd} (x)⟩, ⟨1^{st} (y), 2^{nd} (y)⟩⟩ comp (O \times_{c} C) ⟨1^{st} (z), 2^{nd} (z)⟩) ⟨1^{st} (f), 2^{nd} (f)⟩$
210		eqid	$⊢ comp (O) = comp (O)$
211	19 20 7 115 8 170 171 173 174 210 9 27 177 179 184 187 192 196	xpcco2	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to ⟨1^{st} (g), 2^{nd} (g)⟩ (⟨⟨1^{st} (x), 2^{nd} (x)⟩, ⟨1^{st} (y), 2^{nd} (y)⟩⟩ comp (O \times_{c} C) ⟨1^{st} (z), 2^{nd} (z)⟩) ⟨1^{st} (f), 2^{nd} (f)⟩ = ⟨1^{st} (g) (⟨1^{st} (x), 1^{st} (y)⟩ comp (O) 1^{st} (z)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (x), 2^{nd} (y)⟩ comp (C) 2^{nd} (z)) 2^{nd} (f)⟩$
212	7 9 2 170 173 177	oppcco	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to 1^{st} (g) (⟨1^{st} (x), 1^{st} (y)⟩ comp (O) 1^{st} (z)) 1^{st} (f) = 1^{st} (f) (⟨1^{st} (z), 1^{st} (y)⟩ comp (C) 1^{st} (x)) 1^{st} (g)$
213	212	opeq1d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to ⟨1^{st} (g) (⟨1^{st} (x), 1^{st} (y)⟩ comp (O) 1^{st} (z)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (x), 2^{nd} (y)⟩ comp (C) 2^{nd} (z)) 2^{nd} (f)⟩ = ⟨1^{st} (f) (⟨1^{st} (z), 1^{st} (y)⟩ comp (C) 1^{st} (x)) 1^{st} (g), 2^{nd} (g) (⟨2^{nd} (x), 2^{nd} (y)⟩ comp (C) 2^{nd} (z)) 2^{nd} (f)⟩$
214	209 211 213	3eqtrd	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to g (⟨x, y⟩ comp (O \times_{c} C) z) f = ⟨1^{st} (f) (⟨1^{st} (z), 1^{st} (y)⟩ comp (C) 1^{st} (x)) 1^{st} (g), 2^{nd} (g) (⟨2^{nd} (x), 2^{nd} (y)⟩ comp (C) 2^{nd} (z)) 2^{nd} (f)⟩$
215	201 214	fveq12d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to (x 2^{nd} (M) z) (g (⟨x, y⟩ comp (O \times_{c} C) z) f) = (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (z), 2^{nd} (z)⟩) (⟨1^{st} (f) (⟨1^{st} (z), 1^{st} (y)⟩ comp (C) 1^{st} (x)) 1^{st} (g), 2^{nd} (g) (⟨2^{nd} (x), 2^{nd} (y)⟩ comp (C) 2^{nd} (z)) 2^{nd} (f)⟩)$
216		df-ov	$⊢ (1^{st} (f) (⟨1^{st} (z), 1^{st} (y)⟩ comp (C) 1^{st} (x)) 1^{st} (g)) (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (z), 2^{nd} (z)⟩) (2^{nd} (g) (⟨2^{nd} (x), 2^{nd} (y)⟩ comp (C) 2^{nd} (z)) 2^{nd} (f)) = (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (z), 2^{nd} (z)⟩) (⟨1^{st} (f) (⟨1^{st} (z), 1^{st} (y)⟩ comp (C) 1^{st} (x)) 1^{st} (g), 2^{nd} (g) (⟨2^{nd} (x), 2^{nd} (y)⟩ comp (C) 2^{nd} (z)) 2^{nd} (f)⟩)$
217	215 216	eqtr4di	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to (x 2^{nd} (M) z) (g (⟨x, y⟩ comp (O \times_{c} C) z) f) = (1^{st} (f) (⟨1^{st} (z), 1^{st} (y)⟩ comp (C) 1^{st} (x)) 1^{st} (g)) (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (z), 2^{nd} (z)⟩) (2^{nd} (g) (⟨2^{nd} (x), 2^{nd} (y)⟩ comp (C) 2^{nd} (z)) 2^{nd} (f))$
218	198	fveq2d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to {Hom}_{𝑓} (C) (x) = {Hom}_{𝑓} (C) (⟨1^{st} (x), 2^{nd} (x)⟩)$
219	218 90	eqtr4di	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to {Hom}_{𝑓} (C) (x) = 1^{st} (x) {Hom}_{𝑓} (C) 2^{nd} (x)$
220	34 7 8 170 171	homfval	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to 1^{st} (x) {Hom}_{𝑓} (C) 2^{nd} (x) = 1^{st} (x) Hom (C) 2^{nd} (x)$
221	219 220	eqtrd	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to {Hom}_{𝑓} (C) (x) = 1^{st} (x) Hom (C) 2^{nd} (x)$
222	202	fveq2d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to {Hom}_{𝑓} (C) (y) = {Hom}_{𝑓} (C) (⟨1^{st} (y), 2^{nd} (y)⟩)$
223	222 98	eqtr4di	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to {Hom}_{𝑓} (C) (y) = 1^{st} (y) {Hom}_{𝑓} (C) 2^{nd} (y)$
224	34 7 8 173 174	homfval	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to 1^{st} (y) {Hom}_{𝑓} (C) 2^{nd} (y) = 1^{st} (y) Hom (C) 2^{nd} (y)$
225	223 224	eqtrd	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to {Hom}_{𝑓} (C) (y) = 1^{st} (y) Hom (C) 2^{nd} (y)$
226	221 225	opeq12d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to ⟨{Hom}_{𝑓} (C) (x), {Hom}_{𝑓} (C) (y)⟩ = ⟨1^{st} (x) Hom (C) 2^{nd} (x), 1^{st} (y) Hom (C) 2^{nd} (y)⟩$
227	200	fveq2d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to {Hom}_{𝑓} (C) (z) = {Hom}_{𝑓} (C) (⟨1^{st} (z), 2^{nd} (z)⟩)$
228		df-ov	$⊢ 1^{st} (z) {Hom}_{𝑓} (C) 2^{nd} (z) = {Hom}_{𝑓} (C) (⟨1^{st} (z), 2^{nd} (z)⟩)$
229	227 228	eqtr4di	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to {Hom}_{𝑓} (C) (z) = 1^{st} (z) {Hom}_{𝑓} (C) 2^{nd} (z)$
230	34 7 8 177 179	homfval	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to 1^{st} (z) {Hom}_{𝑓} (C) 2^{nd} (z) = 1^{st} (z) Hom (C) 2^{nd} (z)$
231	229 230	eqtrd	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to {Hom}_{𝑓} (C) (z) = 1^{st} (z) Hom (C) 2^{nd} (z)$
232	226 231	oveq12d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to ⟨{Hom}_{𝑓} (C) (x), {Hom}_{𝑓} (C) (y)⟩ comp (D) {Hom}_{𝑓} (C) (z) = ⟨1^{st} (x) Hom (C) 2^{nd} (x), 1^{st} (y) Hom (C) 2^{nd} (y)⟩ comp (D) (1^{st} (z) Hom (C) 2^{nd} (z))$
233	202 200	oveq12d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to y 2^{nd} (M) z = ⟨1^{st} (y), 2^{nd} (y)⟩ 2^{nd} (M) ⟨1^{st} (z), 2^{nd} (z)⟩$
234	233 206	fveq12d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to (y 2^{nd} (M) z) (g) = (⟨1^{st} (y), 2^{nd} (y)⟩ 2^{nd} (M) ⟨1^{st} (z), 2^{nd} (z)⟩) (⟨1^{st} (g), 2^{nd} (g)⟩)$
235		df-ov	$⊢ 1^{st} (g) (⟨1^{st} (y), 2^{nd} (y)⟩ 2^{nd} (M) ⟨1^{st} (z), 2^{nd} (z)⟩) 2^{nd} (g) = (⟨1^{st} (y), 2^{nd} (y)⟩ 2^{nd} (M) ⟨1^{st} (z), 2^{nd} (z)⟩) (⟨1^{st} (g), 2^{nd} (g)⟩)$
236	234 235	eqtr4di	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to (y 2^{nd} (M) z) (g) = 1^{st} (g) (⟨1^{st} (y), 2^{nd} (y)⟩ 2^{nd} (M) ⟨1^{st} (z), 2^{nd} (z)⟩) 2^{nd} (g)$
237	198 202	oveq12d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to x 2^{nd} (M) y = ⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (y), 2^{nd} (y)⟩$
238	237 208	fveq12d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to (x 2^{nd} (M) y) (f) = (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (y), 2^{nd} (y)⟩) (⟨1^{st} (f), 2^{nd} (f)⟩)$
239		df-ov	$⊢ 1^{st} (f) (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (y), 2^{nd} (y)⟩) 2^{nd} (f) = (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (y), 2^{nd} (y)⟩) (⟨1^{st} (f), 2^{nd} (f)⟩)$
240	238 239	eqtr4di	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to (x 2^{nd} (M) y) (f) = 1^{st} (f) (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (y), 2^{nd} (y)⟩) 2^{nd} (f)$
241	232 236 240	oveq123d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to (y 2^{nd} (M) z) (g) (⟨{Hom}_{𝑓} (C) (x), {Hom}_{𝑓} (C) (y)⟩ comp (D) {Hom}_{𝑓} (C) (z)) (x 2^{nd} (M) y) (f) = (1^{st} (g) (⟨1^{st} (y), 2^{nd} (y)⟩ 2^{nd} (M) ⟨1^{st} (z), 2^{nd} (z)⟩) 2^{nd} (g)) (⟨1^{st} (x) Hom (C) 2^{nd} (x), 1^{st} (y) Hom (C) 2^{nd} (y)⟩ comp (D) (1^{st} (z) Hom (C) 2^{nd} (z))) (1^{st} (f) (⟨1^{st} (x), 2^{nd} (x)⟩ 2^{nd} (M) ⟨1^{st} (y), 2^{nd} (y)⟩) 2^{nd} (f))$
242	197 217 241	3eqtr4d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{C}) \land y \in ({Base}_{C} \times {Base}_{C}) \land z \in ({Base}_{C} \times {Base}_{C})) \land (f \in (x Hom (O \times_{c} C) y) \land g \in (y Hom (O \times_{c} C) z))) \to (x 2^{nd} (M) z) (g (⟨x, y⟩ comp (O \times_{c} C) z) f) = (y 2^{nd} (M) z) (g) (⟨{Hom}_{𝑓} (C) (x), {Hom}_{𝑓} (C) (y)⟩ comp (D) {Hom}_{𝑓} (C) (z)) (x 2^{nd} (M) y) (f)$
243	21 22 23 24 25 26 27 28 31 33 41 48 123 165 242	isfuncd	$⊢ φ \to {Hom}_{𝑓} (C) ((O \times_{c} C) Func D) 2^{nd} (M)$
244		df-br	$⊢ {Hom}_{𝑓} (C) ((O \times_{c} C) Func D) 2^{nd} (M) \leftrightarrow ⟨{Hom}_{𝑓} (C), 2^{nd} (M)⟩ \in ((O \times_{c} C) Func D)$
245	243 244	sylib	$⊢ φ \to ⟨{Hom}_{𝑓} (C), 2^{nd} (M)⟩ \in ((O \times_{c} C) Func D)$
246	18 245	eqeltrd	$⊢ φ \to M \in ((O \times_{c} C) Func D)$

Metamath Proof Explorer

Theorem hofcl

Proof