funcpropd

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

	Ref	Expression
Hypotheses	funcpropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
	funcpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐴 ) = ( comp_f ‘ 𝐵 ) )
	funcpropd.3	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
	funcpropd.4	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
	funcpropd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	funcpropd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	funcpropd.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	funcpropd.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
Assertion	funcpropd	⊢ ( 𝜑 → ( 𝐴 Func 𝐶 ) = ( 𝐵 Func 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		funcpropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
2		funcpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐴 ) = ( comp_f ‘ 𝐵 ) )
3		funcpropd.3	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
4		funcpropd.4	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
5		funcpropd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		funcpropd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
7		funcpropd.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
8		funcpropd.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
9		relfunc	⊢ Rel ( 𝐴 Func 𝐶 )
10		relfunc	⊢ Rel ( 𝐵 Func 𝐷 )
11	1 2 5 6	catpropd	⊢ ( 𝜑 → ( 𝐴 ∈ Cat ↔ 𝐵 ∈ Cat ) )
12	3 4 7 8	catpropd	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ↔ 𝐷 ∈ Cat ) )
13	11 12	anbi12d	⊢ ( 𝜑 → ( ( 𝐴 ∈ Cat ∧ 𝐶 ∈ Cat ) ↔ ( 𝐵 ∈ Cat ∧ 𝐷 ∈ Cat ) ) )
14		2fveq3	⊢ ( 𝑧 = 𝑤 → ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) = ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) )
15		2fveq3	⊢ ( 𝑧 = 𝑤 → ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) = ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) )
16	14 15	oveq12d	⊢ ( 𝑧 = 𝑤 → ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) = ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) )
17		fveq2	⊢ ( 𝑧 = 𝑤 → ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) = ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) )
18	16 17	oveq12d	⊢ ( 𝑧 = 𝑤 → ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) = ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) )
19	18	cbvixpv	⊢ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) = X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) )
20	19	eleq2i	⊢ ( 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) ↔ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) )
21	20	anbi2i	⊢ ( ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) )
22	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
23	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( comp_f ‘ 𝐴 ) = ( comp_f ‘ 𝐵 ) )
24	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → 𝐴 ∈ 𝑉 )
25	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → 𝐵 ∈ 𝑉 )
26	22 23 24 25	cidpropd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( Id ‘ 𝐴 ) = ( Id ‘ 𝐵 ) )
27	26	fveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) = ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) )
28	27	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ) = ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) )
29	3 4 7 8	cidpropd	⊢ ( 𝜑 → ( Id ‘ 𝐶 ) = ( Id ‘ 𝐷 ) )
30	29	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( Id ‘ 𝐶 ) = ( Id ‘ 𝐷 ) )
31	30	fveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) )
32	28 31	eqeq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ↔ ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
33		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
34		eqid	⊢ ( Hom ‘ 𝐴 ) = ( Hom ‘ 𝐴 )
35		eqid	⊢ ( comp ‘ 𝐴 ) = ( comp ‘ 𝐴 )
36		eqid	⊢ ( comp ‘ 𝐵 ) = ( comp ‘ 𝐵 )
37	1	ad6antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
38	2	ad6antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → ( comp_f ‘ 𝐴 ) = ( comp_f ‘ 𝐵 ) )
39		simp-5r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
40		simp-4r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
41		simpllr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → 𝑧 ∈ ( Base ‘ 𝐴 ) )
42		simplr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) )
43		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) )
44	33 34 35 36 37 38 39 40 41 42 43	comfeqval	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) = ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) )
45	44	fveq2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) )
46		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
47		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
48		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
49		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
50	3	ad6antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
51	4	ad6antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
52		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) → 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) )
53	52	ad5antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) )
54	53 39	ffvelcdmd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
55	53 40	ffvelcdmd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → ( 𝑓 ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
56	53 41	ffvelcdmd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → ( 𝑓 ‘ 𝑧 ) ∈ ( Base ‘ 𝐶 ) )
57		df-ov	⊢ ( 𝑥 𝑔 𝑦 ) = ( 𝑔 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
58		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) → 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) )
59	58	ad3antrrr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) )
60	59	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) )
61		opelxpi	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) )
62	61	ad5ant23	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) )
63		vex	⊢ 𝑥 ∈ V
64		vex	⊢ 𝑦 ∈ V
65	63 64	op1std	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1^st ‘ 𝑤 ) = 𝑥 )
66	65	fveq2d	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) = ( 𝑓 ‘ 𝑥 ) )
67	63 64	op2ndd	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2^nd ‘ 𝑤 ) = 𝑦 )
68	67	fveq2d	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) = ( 𝑓 ‘ 𝑦 ) )
69	66 68	oveq12d	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) )
70		fveq2	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) = ( ( Hom ‘ 𝐴 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
71		df-ov	⊢ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) = ( ( Hom ‘ 𝐴 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
72	70 71	eqtr4di	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) = ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) )
73	69 72	oveq12d	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) = ( ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) ↑_m ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) )
74	73	fvixp	⊢ ( ( 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → ( 𝑔 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) ↑_m ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) )
75	60 62 74	syl2anc	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( 𝑔 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) ↑_m ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) )
76	57 75	eqeltrid	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( 𝑥 𝑔 𝑦 ) ∈ ( ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) ↑_m ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) )
77		elmapi	⊢ ( ( 𝑥 𝑔 𝑦 ) ∈ ( ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) ↑_m ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( 𝑥 𝑔 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ⟶ ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) )
78	76 77	syl	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( 𝑥 𝑔 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ⟶ ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) )
79	78	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → ( 𝑥 𝑔 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ⟶ ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) )
80	79 42	ffvelcdmd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ∈ ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) )
81		df-ov	⊢ ( 𝑦 𝑔 𝑧 ) = ( 𝑔 ‘ ⟨ 𝑦 , 𝑧 ⟩ )
82		opelxpi	⊢ ( ( 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) )
83	82	adantll	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) )
84		vex	⊢ 𝑧 ∈ V
85	64 84	op1std	⊢ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( 1^st ‘ 𝑤 ) = 𝑦 )
86	85	fveq2d	⊢ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) = ( 𝑓 ‘ 𝑦 ) )
87	64 84	op2ndd	⊢ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( 2^nd ‘ 𝑤 ) = 𝑧 )
88	87	fveq2d	⊢ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) = ( 𝑓 ‘ 𝑧 ) )
89	86 88	oveq12d	⊢ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) = ( ( 𝑓 ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) )
90		fveq2	⊢ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) = ( ( Hom ‘ 𝐴 ) ‘ ⟨ 𝑦 , 𝑧 ⟩ ) )
91		df-ov	⊢ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) = ( ( Hom ‘ 𝐴 ) ‘ ⟨ 𝑦 , 𝑧 ⟩ )
92	90 91	eqtr4di	⊢ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) = ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) )
93	89 92	oveq12d	⊢ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) = ( ( ( 𝑓 ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ↑_m ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) )
94	93	fvixp	⊢ ( ( 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → ( 𝑔 ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ∈ ( ( ( 𝑓 ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ↑_m ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) )
95	59 83 94	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑔 ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ∈ ( ( ( 𝑓 ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ↑_m ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) )
96	81 95	eqeltrid	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑦 𝑔 𝑧 ) ∈ ( ( ( 𝑓 ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ↑_m ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) )
97		elmapi	⊢ ( ( 𝑦 𝑔 𝑧 ) ∈ ( ( ( 𝑓 ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ↑_m ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → ( 𝑦 𝑔 𝑧 ) : ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ⟶ ( ( 𝑓 ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) )
98	96 97	syl	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑦 𝑔 𝑧 ) : ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ⟶ ( ( 𝑓 ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) )
99	98	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( 𝑦 𝑔 𝑧 ) : ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ⟶ ( ( 𝑓 ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) )
100	99	ffvelcdmda	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ∈ ( ( 𝑓 ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) )
101	46 47 48 49 50 51 54 55 56 80 100	comfeqval	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) )
102	45 101	eqeq12d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) → ( ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
103	102	ralbidva	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
104	103	ralbidva	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → ( ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
105		eqid	⊢ ( Hom ‘ 𝐵 ) = ( Hom ‘ 𝐵 )
106	22	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
107		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
108		simplr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
109	33 34 105 106 107 108	homfeqval	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) )
110		simpr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → 𝑧 ∈ ( Base ‘ 𝐴 ) )
111	33 34 105 106 108 110	homfeqval	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) = ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) )
112	111	raleqdv	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → ( ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
113	109 112	raleqbidv	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → ( ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
114	104 113	bitrd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → ( ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
115	114	ralbidva	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
116	115	ralbidva	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
117	32 116	anbi12d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ↔ ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) )
118	117	ralbidva	⊢ ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑤 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑤 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑤 ) ) ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) )
119	21 118	sylan2b	⊢ ( ( 𝜑 ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) )
120	119	pm5.32da	⊢ ( 𝜑 → ( ( ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
121		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
122	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
123		simplr	⊢ ( ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) )
124		xp1st	⊢ ( 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) → ( 1^st ‘ 𝑧 ) ∈ ( Base ‘ 𝐴 ) )
125	124	adantl	⊢ ( ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → ( 1^st ‘ 𝑧 ) ∈ ( Base ‘ 𝐴 ) )
126	123 125	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ∈ ( Base ‘ 𝐶 ) )
127		xp2nd	⊢ ( 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) → ( 2^nd ‘ 𝑧 ) ∈ ( Base ‘ 𝐴 ) )
128	127	adantl	⊢ ( ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → ( 2^nd ‘ 𝑧 ) ∈ ( Base ‘ 𝐴 ) )
129	123 128	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ∈ ( Base ‘ 𝐶 ) )
130	46 47 121 122 126 129	homfeqval	⊢ ( ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) = ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) )
131	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
132	33 34 105 131 125 128	homfeqval	⊢ ( ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → ( ( 1^st ‘ 𝑧 ) ( Hom ‘ 𝐴 ) ( 2^nd ‘ 𝑧 ) ) = ( ( 1^st ‘ 𝑧 ) ( Hom ‘ 𝐵 ) ( 2^nd ‘ 𝑧 ) ) )
133		df-ov	⊢ ( ( 1^st ‘ 𝑧 ) ( Hom ‘ 𝐴 ) ( 2^nd ‘ 𝑧 ) ) = ( ( Hom ‘ 𝐴 ) ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
134		df-ov	⊢ ( ( 1^st ‘ 𝑧 ) ( Hom ‘ 𝐵 ) ( 2^nd ‘ 𝑧 ) ) = ( ( Hom ‘ 𝐵 ) ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
135	132 133 134	3eqtr3g	⊢ ( ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → ( ( Hom ‘ 𝐴 ) ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) = ( ( Hom ‘ 𝐵 ) ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) )
136		1st2nd2	⊢ ( 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
137	136	adantl	⊢ ( ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
138	137	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) = ( ( Hom ‘ 𝐴 ) ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) )
139	137	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) = ( ( Hom ‘ 𝐵 ) ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) )
140	135 138 139	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) = ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) )
141	130 140	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ) → ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) = ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) )
142	141	ixpeq2dva	⊢ ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) → X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) = X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) )
143	1	homfeqbas	⊢ ( 𝜑 → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
144	143	sqxpeqd	⊢ ( 𝜑 → ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) = ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) )
145	144	adantr	⊢ ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) → ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) = ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) )
146	145	ixpeq1d	⊢ ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) → X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) = X 𝑧 ∈ ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) )
147	142 146	eqtrd	⊢ ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) → X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) = X 𝑧 ∈ ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) )
148	147	eleq2d	⊢ ( ( 𝜑 ∧ 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ) → ( 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) ↔ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) ) )
149	148	pm5.32da	⊢ ( 𝜑 → ( ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) ) ) )
150	3	homfeqbas	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
151	143 150	feq23d	⊢ ( 𝜑 → ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ↔ 𝑓 : ( Base ‘ 𝐵 ) ⟶ ( Base ‘ 𝐷 ) ) )
152	151	anbi1d	⊢ ( 𝜑 → ( ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝐵 ) ⟶ ( Base ‘ 𝐷 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) ) ) )
153	149 152	bitrd	⊢ ( 𝜑 → ( ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝐵 ) ⟶ ( Base ‘ 𝐷 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) ) ) )
154	143	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
155	154	raleqdv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐵 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
156	154 155	raleqbidv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑧 ∈ ( Base ‘ 𝐵 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
157	156	anbi2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ↔ ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑧 ∈ ( Base ‘ 𝐵 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) )
158	143 157	raleqbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑧 ∈ ( Base ‘ 𝐵 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) )
159	153 158	anbi12d	⊢ ( 𝜑 → ( ( ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( ( 𝑓 : ( Base ‘ 𝐵 ) ⟶ ( Base ‘ 𝐷 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑧 ∈ ( Base ‘ 𝐵 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
160	120 159	bitrd	⊢ ( 𝜑 → ( ( ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( ( 𝑓 : ( Base ‘ 𝐵 ) ⟶ ( Base ‘ 𝐷 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑧 ∈ ( Base ‘ 𝐵 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
161		df-3an	⊢ ( ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) )
162		df-3an	⊢ ( ( 𝑓 : ( Base ‘ 𝐵 ) ⟶ ( Base ‘ 𝐷 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑧 ∈ ( Base ‘ 𝐵 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( ( 𝑓 : ( Base ‘ 𝐵 ) ⟶ ( Base ‘ 𝐷 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑧 ∈ ( Base ‘ 𝐵 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) )
163	160 161 162	3bitr4g	⊢ ( 𝜑 → ( ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝐵 ) ⟶ ( Base ‘ 𝐷 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑧 ∈ ( Base ‘ 𝐵 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
164	13 163	anbi12d	⊢ ( 𝜑 → ( ( ( 𝐴 ∈ Cat ∧ 𝐶 ∈ Cat ) ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) ↔ ( ( 𝐵 ∈ Cat ∧ 𝐷 ∈ Cat ) ∧ ( 𝑓 : ( Base ‘ 𝐵 ) ⟶ ( Base ‘ 𝐷 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑧 ∈ ( Base ‘ 𝐵 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) ) )
165		df-br	⊢ ( 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ↔ ⟨ 𝑓 , 𝑔 ⟩ ∈ ( 𝐴 Func 𝐶 ) )
166		funcrcl	⊢ ( ⟨ 𝑓 , 𝑔 ⟩ ∈ ( 𝐴 Func 𝐶 ) → ( 𝐴 ∈ Cat ∧ 𝐶 ∈ Cat ) )
167	165 166	sylbi	⊢ ( 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 → ( 𝐴 ∈ Cat ∧ 𝐶 ∈ Cat ) )
168		eqid	⊢ ( Id ‘ 𝐴 ) = ( Id ‘ 𝐴 )
169		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
170		simpl	⊢ ( ( 𝐴 ∈ Cat ∧ 𝐶 ∈ Cat ) → 𝐴 ∈ Cat )
171		simpr	⊢ ( ( 𝐴 ∈ Cat ∧ 𝐶 ∈ Cat ) → 𝐶 ∈ Cat )
172	33 46 34 47 168 169 35 48 170 171	isfunc	⊢ ( ( 𝐴 ∈ Cat ∧ 𝐶 ∈ Cat ) → ( 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ↔ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
173	167 172	biadanii	⊢ ( 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ↔ ( ( 𝐴 ∈ Cat ∧ 𝐶 ∈ Cat ) ∧ ( 𝑓 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐴 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐴 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐴 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
174		df-br	⊢ ( 𝑓 ( 𝐵 Func 𝐷 ) 𝑔 ↔ ⟨ 𝑓 , 𝑔 ⟩ ∈ ( 𝐵 Func 𝐷 ) )
175		funcrcl	⊢ ( ⟨ 𝑓 , 𝑔 ⟩ ∈ ( 𝐵 Func 𝐷 ) → ( 𝐵 ∈ Cat ∧ 𝐷 ∈ Cat ) )
176	174 175	sylbi	⊢ ( 𝑓 ( 𝐵 Func 𝐷 ) 𝑔 → ( 𝐵 ∈ Cat ∧ 𝐷 ∈ Cat ) )
177		eqid	⊢ ( Base ‘ 𝐵 ) = ( Base ‘ 𝐵 )
178		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
179		eqid	⊢ ( Id ‘ 𝐵 ) = ( Id ‘ 𝐵 )
180		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
181		simpl	⊢ ( ( 𝐵 ∈ Cat ∧ 𝐷 ∈ Cat ) → 𝐵 ∈ Cat )
182		simpr	⊢ ( ( 𝐵 ∈ Cat ∧ 𝐷 ∈ Cat ) → 𝐷 ∈ Cat )
183	177 178 105 121 179 180 36 49 181 182	isfunc	⊢ ( ( 𝐵 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝑓 ( 𝐵 Func 𝐷 ) 𝑔 ↔ ( 𝑓 : ( Base ‘ 𝐵 ) ⟶ ( Base ‘ 𝐷 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑧 ∈ ( Base ‘ 𝐵 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
184	176 183	biadanii	⊢ ( 𝑓 ( 𝐵 Func 𝐷 ) 𝑔 ↔ ( ( 𝐵 ∈ Cat ∧ 𝐷 ∈ Cat ) ∧ ( 𝑓 : ( Base ‘ 𝐵 ) ⟶ ( Base ‘ 𝐷 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐵 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐵 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑧 ∈ ( Base ‘ 𝐵 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
185	164 173 184	3bitr4g	⊢ ( 𝜑 → ( 𝑓 ( 𝐴 Func 𝐶 ) 𝑔 ↔ 𝑓 ( 𝐵 Func 𝐷 ) 𝑔 ) )
186	9 10 185	eqbrrdiv	⊢ ( 𝜑 → ( 𝐴 Func 𝐶 ) = ( 𝐵 Func 𝐷 ) )

Metamath Proof Explorer

Theorem funcpropd

Proof