hofpropd

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

	Ref	Expression
Hypotheses	hofpropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
	hofpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
	hofpropd.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	hofpropd.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
Assertion	hofpropd	⊢ ( 𝜑 → ( Hom_F ‘ 𝐶 ) = ( Hom_F ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		hofpropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
2		hofpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
3		hofpropd.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		hofpropd.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
5	1	homfeqbas	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
6	5	sqxpeqd	⊢ ( 𝜑 → ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) = ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
7	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) → ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) = ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
8		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
10		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
11	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
12		xp1st	⊢ ( 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
13	12	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) → ( 1^st ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
14		xp1st	⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
15	14	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) → ( 1^st ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
16	8 9 10 11 13 15	homfeqval	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) → ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( 1^st ‘ 𝑥 ) ) )
17		xp2nd	⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) → ( 2^nd ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
18	17	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) → ( 2^nd ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
19		xp2nd	⊢ ( 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) → ( 2^nd ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
20	19	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) → ( 2^nd ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
21	8 9 10 11 18 20	homfeqval	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) → ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) = ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑦 ) ) )
22	21	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ) → ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) = ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑦 ) ) )
23	8 9 10 11 15 18	homfeqval	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) → ( ( 1^st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑥 ) ) )
24		df-ov	⊢ ( ( 1^st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑥 ) ) = ( ( Hom ‘ 𝐶 ) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
25		df-ov	⊢ ( ( 1^st ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑥 ) ) = ( ( Hom ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
26	23 24 25	3eqtr3g	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) → ( ( Hom ‘ 𝐶 ) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) = ( ( Hom ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) )
27		1st2nd2	⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
28	27	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
29	28	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) → ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) = ( ( Hom ‘ 𝐶 ) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) )
30	28	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) → ( ( Hom ‘ 𝐷 ) ‘ 𝑥 ) = ( ( Hom ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) )
31	26 29 30	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) → ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) = ( ( Hom ‘ 𝐷 ) ‘ 𝑥 ) )
32	31	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) → ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) = ( ( Hom ‘ 𝐷 ) ‘ 𝑥 ) )
33		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
34		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
35	11	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) ∧ ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
36	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) ∧ ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
37	13	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) ∧ ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) → ( 1^st ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
38	15	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) ∧ ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) → ( 1^st ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
39	20	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) ∧ ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) → ( 2^nd ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
40		simplrl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) ∧ ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) → 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) )
41	28	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) ∧ ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
42	41	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 ‘ 𝑦 ) ) )
43	42	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 ‘ 𝑦 ) ) ℎ ) )
44	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) ∧ ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) → 𝐶 ∈ Cat )
45	18	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) ∧ ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) → ( 2^nd ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
46	29	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) → ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) = ( ( Hom ‘ 𝐶 ) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) )
47	46 24	eqtr4di	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) → ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑥 ) ) )
48	47	eleq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) → ( ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ↔ ℎ ∈ ( ( 1^st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑥 ) ) ) )
49	48	biimpa	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) ∧ ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) → ℎ ∈ ( ( 1^st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑥 ) ) )
50		simplrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) ∧ ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) → 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) )
51	8 9 33 44 38 45 39 49 50	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 ‘ 𝑦 ) ) )
52	43 51	eqeltrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) ∧ ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) → ( 𝑔 ( 𝑥 ( comp ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ∈ ( ( 1^st ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) )
53	8 9 33 34 35 36 37 38 39 40 52	comfeqval	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 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 ‘ 𝑦 ) ) 𝑓 ) = ( ( 𝑔 ( 𝑥 ( comp ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) )
54	8 9 33 34 35 36 38 45 39 49 50	comfeqval	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) ∧ ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) → ( 𝑔 ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) = ( 𝑔 ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) )
55	41	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 ‘ 𝑦 ) ) )
56	55	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 ‘ 𝑦 ) ) ℎ ) )
57	54 43 56	3eqtr4d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑥 ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) ) ∧ ℎ ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) → ( 𝑔 ( 𝑥 ( comp ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) = ( 𝑔 ( 𝑥 ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) )
58	57	oveq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 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 ‘ 𝑦 ) ) 𝑓 ) = ( ( 𝑔 ( 𝑥 ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) )
59	53 58	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 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 ‘ 𝑦 ) ) 𝑓 ) = ( ( 𝑔 ( 𝑥 ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) )
60	32 59	mpteq12dva	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 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 ‘ 𝐷 ) ‘ 𝑥 ) ↦ ( ( 𝑔 ( 𝑥 ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑦 ) ) ℎ ) ( ⟨ ( 1^st ‘ 𝑦 ) , ( 1^st ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑦 ) ) 𝑓 ) ) )
61	16 22 60	mpoeq123dva	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 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 ‘ 𝑦 ) ) 𝑓 ) ) ) )
62	6 7 61	mpoeq123dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 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 ‘ 𝑦 ) ) 𝑓 ) ) ) ) )
63	1 62	opeq12d	⊢ ( 𝜑 → ⟨ ( 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 ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ = ⟨ ( 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 ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ )
64		eqid	⊢ ( Hom_F ‘ 𝐶 ) = ( Hom_F ‘ 𝐶 )
65	64 3 8 9 33	hofval	⊢ ( 𝜑 → ( Hom_F ‘ 𝐶 ) = ⟨ ( 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 ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ )
66		eqid	⊢ ( Hom_F ‘ 𝐷 ) = ( Hom_F ‘ 𝐷 )
67		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
68	66 4 67 10 34	hofval	⊢ ( 𝜑 → ( Hom_F ‘ 𝐷 ) = ⟨ ( 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 ‘ 𝑦 ) ) 𝑓 ) ) ) ) ⟩ )
69	63 65 68	3eqtr4d	⊢ ( 𝜑 → ( Hom_F ‘ 𝐶 ) = ( Hom_F ‘ 𝐷 ) )

Metamath Proof Explorer

Theorem hofpropd

Proof