| 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 ‘ 𝑀 ) ) ) ) |