This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mndtccatid

Description: Lemma for mndtccat and mndtcid . (Contributed by Zhi Wang, 22-Sep-2024)

Ref Expression
Hypotheses mndtccat.c ⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
mndtccat.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
Assertion mndtccatid ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 0g ‘ 𝑀 ) ) ) )

Proof

Step Hyp Ref Expression
1 mndtccat.c ⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
2 mndtccat.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 ) )
4 eqidd ⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )
5 eqidd ⊢ ( 𝜑 → ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 ) )
6 fvexd ⊢ ( 𝜑 → ( MndToCat ‘ 𝑀 ) ∈ V )
7 1 6 eqeltrd ⊢ ( 𝜑 → 𝐶 ∈ V )
8 biid ⊢ ( ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) )
9 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
10 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
11 9 10 mndidcl ⊢ ( 𝑀 ∈ Mnd → ( 0g ‘ 𝑀 ) ∈ ( Base ‘ 𝑀 ) )
12 2 11 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑀 ) ∈ ( Base ‘ 𝑀 ) )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 0g ‘ 𝑀 ) ∈ ( Base ‘ 𝑀 ) )
14 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 = ( MndToCat ‘ 𝑀 ) )
15 2 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝑀 ∈ Mnd )
16 eqidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 ) )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
18 eqidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )
19 14 15 16 17 17 18 mndtchom ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ( Hom ‘ 𝐶 ) 𝑦 ) = ( Base ‘ 𝑀 ) )
20 13 19 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 0g ‘ 𝑀 ) ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑦 ) )
21 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → 𝐶 = ( MndToCat ‘ 𝑀 ) )
22 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → 𝑀 ∈ Mnd )
23 eqidd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 ) )
24 simpr1l ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
25 simpr1r ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
26 eqidd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 ) )
27 21 22 23 24 25 25 26 mndtcco ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) = ( +g ‘ 𝑀 ) )
28 27 oveqd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( ( 0g ‘ 𝑀 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) = ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) 𝑓 ) )
29 simpr31 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
30 eqidd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )
31 21 22 23 24 25 30 mndtchom ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ( Base ‘ 𝑀 ) )
32 29 31 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → 𝑓 ∈ ( Base ‘ 𝑀 ) )
33 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
34 9 33 10 mndlid ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑓 ∈ ( Base ‘ 𝑀 ) ) → ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) 𝑓 ) = 𝑓 )
35 22 32 34 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) 𝑓 ) = 𝑓 )
36 28 35 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( ( 0g ‘ 𝑀 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) = 𝑓 )
37 simpr2l ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
38 21 22 23 25 25 37 26 mndtcco ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( ⟨ 𝑦 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) = ( +g ‘ 𝑀 ) )
39 38 oveqd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 0g ‘ 𝑀 ) ) = ( 𝑔 ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) )
40 simpr32 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
41 21 22 23 25 37 30 mndtchom ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) = ( Base ‘ 𝑀 ) )
42 40 41 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → 𝑔 ∈ ( Base ‘ 𝑀 ) )
43 9 33 10 mndrid ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑔 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑔 ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) = 𝑔 )
44 22 42 43 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( 𝑔 ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) = 𝑔 )
45 39 44 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 0g ‘ 𝑀 ) ) = 𝑔 )
46 9 33 mndcl ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑔 ∈ ( Base ‘ 𝑀 ) ∧ 𝑓 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑔 ( +g ‘ 𝑀 ) 𝑓 ) ∈ ( Base ‘ 𝑀 ) )
47 22 42 32 46 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( 𝑔 ( +g ‘ 𝑀 ) 𝑓 ) ∈ ( Base ‘ 𝑀 ) )
48 21 22 23 24 25 37 26 mndtcco ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) = ( +g ‘ 𝑀 ) )
49 48 oveqd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( +g ‘ 𝑀 ) 𝑓 ) )
50 21 22 23 24 37 30 mndtchom ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) = ( Base ‘ 𝑀 ) )
51 47 49 50 3eltr4d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
52 simpr33 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) )
53 simpr2r ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
54 21 22 23 37 53 30 mndtchom ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) = ( Base ‘ 𝑀 ) )
55 52 54 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → 𝑘 ∈ ( Base ‘ 𝑀 ) )
56 9 33 mndass ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑘 ∈ ( Base ‘ 𝑀 ) ∧ 𝑔 ∈ ( Base ‘ 𝑀 ) ∧ 𝑓 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝑘 ( +g ‘ 𝑀 ) 𝑔 ) ( +g ‘ 𝑀 ) 𝑓 ) = ( 𝑘 ( +g ‘ 𝑀 ) ( 𝑔 ( +g ‘ 𝑀 ) 𝑓 ) ) )
57 22 55 42 32 56 syl13anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( ( 𝑘 ( +g ‘ 𝑀 ) 𝑔 ) ( +g ‘ 𝑀 ) 𝑓 ) = ( 𝑘 ( +g ‘ 𝑀 ) ( 𝑔 ( +g ‘ 𝑀 ) 𝑓 ) ) )
58 21 22 23 24 25 53 26 mndtcco ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) = ( +g ‘ 𝑀 ) )
59 21 22 23 25 37 53 26 mndtcco ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) = ( +g ‘ 𝑀 ) )
60 59 oveqd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) = ( 𝑘 ( +g ‘ 𝑀 ) 𝑔 ) )
61 eqidd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → 𝑓 = 𝑓 )
62 58 60 61 oveq123d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( ( 𝑘 ( +g ‘ 𝑀 ) 𝑔 ) ( +g ‘ 𝑀 ) 𝑓 ) )
63 21 22 23 24 37 53 26 mndtcco ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) = ( +g ‘ 𝑀 ) )
64 eqidd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → 𝑘 = 𝑘 )
65 63 64 49 oveq123d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) = ( 𝑘 ( +g ‘ 𝑀 ) ( 𝑔 ( +g ‘ 𝑀 ) 𝑓 ) ) )
66 57 62 65 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ) ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ) )
67 3 4 5 7 8 20 36 45 51 66 iscatd2 ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 0g ‘ 𝑀 ) ) ) )