Metamath Proof Explorer

Theorem monpropd

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

Ref Expression
Hypotheses monpropd.3 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
monpropd.4 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
monpropd.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
monpropd.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
Assertion monpropd ( 𝜑 → ( Mono ‘ 𝐶 ) = ( Mono ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 monpropd.3 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
2 monpropd.4 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
3 monpropd.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 monpropd.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
5 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
7 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
8 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
9 8 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝐶 ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
10 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝐶 ) ) → 𝑐 ∈ ( Base ‘ 𝐶 ) )
11 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝐶 ) ) → 𝑎 ∈ ( Base ‘ 𝐶 ) )
12 5 6 7 9 10 11 homfeqval ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) = ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) )
13 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
14 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
15 1 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
16 2 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ) → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
17 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ) → 𝑐 ∈ ( Base ‘ 𝐶 ) )
18 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ) → 𝑎 ∈ ( Base ‘ 𝐶 ) )
19 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ) → 𝑏 ∈ ( Base ‘ 𝐶 ) )
20 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ) → 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) )
21 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ) → 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) )
22 5 6 13 14 15 16 17 18 19 20 21 comfeqval ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ) → ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) )
23 12 22 mpteq12dva ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) )
24 23 cnveqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝐶 ) ) → ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑔 ) ) = ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) )
25 24 funeqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝐶 ) ) → ( Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑔 ) ) ↔ Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) ) )
26 25 ralbidva ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) → ( ∀ 𝑐 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑔 ) ) ↔ ∀ 𝑐 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) ) )
27 26 rabbidva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑔 ) ) } = { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) } )
28 simplr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → 𝑎 ∈ ( Base ‘ 𝐶 ) )
29 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → 𝑏 ∈ ( Base ‘ 𝐶 ) )
30 5 6 7 8 28 29 homfeqval ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) = ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) )
31 1 homfeqbas ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
32 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
33 32 raleqdv ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → ( ∀ 𝑐 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) ↔ ∀ 𝑐 ∈ ( Base ‘ 𝐷 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) ) )
34 30 33 rabeqbidv ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) } = { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐷 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) } )
35 27 34 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑔 ) ) } = { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐷 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) } )
36 35 3impa ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑔 ) ) } = { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐷 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) } )
37 36 mpoeq3dva ⊢ ( 𝜑 → ( 𝑎 ∈ ( Base ‘ 𝐶 ) , 𝑏 ∈ ( Base ‘ 𝐶 ) ↦ { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑔 ) ) } ) = ( 𝑎 ∈ ( Base ‘ 𝐶 ) , 𝑏 ∈ ( Base ‘ 𝐶 ) ↦ { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐷 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) } ) )
38 mpoeq12 ⊢ ( ( ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) ∧ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) ) → ( 𝑎 ∈ ( Base ‘ 𝐶 ) , 𝑏 ∈ ( Base ‘ 𝐶 ) ↦ { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐷 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) } ) = ( 𝑎 ∈ ( Base ‘ 𝐷 ) , 𝑏 ∈ ( Base ‘ 𝐷 ) ↦ { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐷 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) } ) )
39 31 31 38 syl2anc ⊢ ( 𝜑 → ( 𝑎 ∈ ( Base ‘ 𝐶 ) , 𝑏 ∈ ( Base ‘ 𝐶 ) ↦ { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐷 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) } ) = ( 𝑎 ∈ ( Base ‘ 𝐷 ) , 𝑏 ∈ ( Base ‘ 𝐷 ) ↦ { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐷 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) } ) )
40 37 39 eqtrd ⊢ ( 𝜑 → ( 𝑎 ∈ ( Base ‘ 𝐶 ) , 𝑏 ∈ ( Base ‘ 𝐶 ) ↦ { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑔 ) ) } ) = ( 𝑎 ∈ ( Base ‘ 𝐷 ) , 𝑏 ∈ ( Base ‘ 𝐷 ) ↦ { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐷 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) } ) )
41 eqid ⊢ ( Mono ‘ 𝐶 ) = ( Mono ‘ 𝐶 )
42 5 6 13 41 3 monfval ⊢ ( 𝜑 → ( Mono ‘ 𝐶 ) = ( 𝑎 ∈ ( Base ‘ 𝐶 ) , 𝑏 ∈ ( Base ‘ 𝐶 ) ↦ { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐶 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐶 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐶 ) 𝑏 ) 𝑔 ) ) } ) )
43 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
44 eqid ⊢ ( Mono ‘ 𝐷 ) = ( Mono ‘ 𝐷 )
45 43 7 14 44 4 monfval ⊢ ( 𝜑 → ( Mono ‘ 𝐷 ) = ( 𝑎 ∈ ( Base ‘ 𝐷 ) , 𝑏 ∈ ( Base ‘ 𝐷 ) ↦ { 𝑓 ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ∣ ∀ 𝑐 ∈ ( Base ‘ 𝐷 ) Fun ◡ ( 𝑔 ∈ ( 𝑐 ( Hom ‘ 𝐷 ) 𝑎 ) ↦ ( 𝑓 ( ⟨ 𝑐 , 𝑎 ⟩ ( comp ‘ 𝐷 ) 𝑏 ) 𝑔 ) ) } ) )
46 40 42 45 3eqtr4d ⊢ ( 𝜑 → ( Mono ‘ 𝐶 ) = ( Mono ‘ 𝐷 ) )