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	⊢ 𝑀 = ( Hom_F ‘ 𝐶 )
	hofcl.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	hofcl.d	⊢ 𝐷 = ( SetCat ‘ 𝑈 )
	hofcl.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	hofcl.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	hofcl.h	⊢ ( 𝜑 → ran ( Hom_f ‘ 𝐶 ) ⊆ 𝑈 )
Assertion	hofcl	⊢ ( 𝜑 → 𝑀 ∈ ( ( 𝑂 ×_c 𝐶 ) Func 𝐷 ) )

Proof

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

Metamath Proof Explorer

Theorem hofcl

Proof