Metamath Proof Explorer

Theorem fthcomf

Description: Source categories of a faithful functor have the same base, hom-sets and composition operation if the composition is compatible in images of the functor. (Contributed by Zhi Wang, 10-Nov-2025)

Ref Expression
Hypotheses fthcomf.1 ⊢ ( 𝜑 → 𝐹 ( 𝐴 Faith 𝐶 ) 𝐺 )
fthcomf.2 ⊢ ( 𝜑 → 𝐹 ( 𝐵 Func 𝐷 ) 𝐺 )
fthcomf.3 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) )
Assertion fthcomf ( 𝜑 → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fthcomf.1 ⊢ ( 𝜑 → 𝐹 ( 𝐴 Faith 𝐶 ) 𝐺 )
2 fthcomf.2 ⊢ ( 𝜑 → 𝐹 ( 𝐵 Func 𝐷 ) 𝐺 )
3 fthcomf.3 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) )
4 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
5 eqid ⊢ ( Hom ‘ 𝐴 ) = ( Hom ‘ 𝐴 )
6 eqid ⊢ ( comp ‘ 𝐴 ) = ( comp ‘ 𝐴 )
7 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
8 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → 𝐹 ( 𝐴 Faith 𝐶 ) 𝐺 )
9 fthfunc ⊢ ( 𝐴 Faith 𝐶 ) ⊆ ( 𝐴 Func 𝐶 )
10 9 ssbri ⊢ ( 𝐹 ( 𝐴 Faith 𝐶 ) 𝐺 → 𝐹 ( 𝐴 Func 𝐶 ) 𝐺 )
11 8 10 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → 𝐹 ( 𝐴 Func 𝐶 ) 𝐺 )
12 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
13 simplr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
14 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐴 ) )
15 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) )
16 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) )
17 4 5 6 7 11 12 13 14 15 16 funcco ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) )
18 eqid ⊢ ( Base ‘ 𝐵 ) = ( Base ‘ 𝐵 )
19 eqid ⊢ ( Hom ‘ 𝐵 ) = ( Hom ‘ 𝐵 )
20 eqid ⊢ ( comp ‘ 𝐵 ) = ( comp ‘ 𝐵 )
21 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
22 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → 𝐹 ( 𝐵 Func 𝐷 ) 𝐺 )
23 1 10 syl ⊢ ( 𝜑 → 𝐹 ( 𝐴 Func 𝐶 ) 𝐺 )
24 23 2 funchomf ⊢ ( 𝜑 → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )
25 24 homfeqbas ⊢ ( 𝜑 → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
26 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
27 12 26 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐵 ) )
28 13 26 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐵 ) )
29 14 26 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐵 ) )
30 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )
31 4 5 19 30 12 13 homfeqval ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) )
32 15 31 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) )
33 4 5 19 30 13 14 homfeqval ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) = ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) )
34 16 33 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐵 ) 𝑧 ) )
35 18 19 20 21 22 27 28 29 32 34 funcco ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) )
36 3 17 35 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑓 ) ) = ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑓 ) ) )
37 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
38 23 funcrcl2 ⊢ ( 𝜑 → 𝐴 ∈ Cat )
39 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → 𝐴 ∈ Cat )
40 4 5 6 39 12 13 14 15 16 catcocl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑧 ) )
41 2 funcrcl2 ⊢ ( 𝜑 → 𝐵 ∈ Cat )
42 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → 𝐵 ∈ Cat )
43 18 19 20 42 27 28 29 32 34 catcocl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑧 ) )
44 4 5 19 30 12 14 homfeqval ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → ( 𝑥 ( Hom ‘ 𝐴 ) 𝑧 ) = ( 𝑥 ( Hom ‘ 𝐵 ) 𝑧 ) )
45 43 44 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑧 ) )
46 4 5 37 8 12 14 40 45 fthi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → ( ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑓 ) ) = ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑓 ) ) ↔ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑓 ) ) )
47 36 46 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑓 ) )
48 47 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) ) → ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑓 ) )
49 48 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑓 ) )
50 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 ) )
51 6 20 5 50 25 24 comfeq ⊢ ( 𝜑 → ( ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑧 ∈ ( Base ‘ 𝐴 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐴 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐴 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐵 ) 𝑧 ) 𝑓 ) ) )
52 49 51 mpbird ⊢ ( 𝜑 → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )