Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Zhi Wang
Examples of categories
Monoids as categories
mndtccatid
Next ⟩
mndtccat
Metamath Proof Explorer
Ascii
Unicode
Theorem
mndtccatid
Description:
Lemma for
mndtccat
and
mndtcid
.
(Contributed by
Zhi Wang
, 22-Sep-2024)
Ref
Expression
Hypotheses
mndtccat.c
⊢
φ
→
C
=
MndToCat
M
mndtccat.m
⊢
φ
→
M
∈
Mnd
Assertion
mndtccatid
⊢
φ
→
C
∈
Cat
∧
Id
C
=
y
∈
Base
C
⟼
0
M
Proof
Step
Hyp
Ref
Expression
1
mndtccat.c
⊢
φ
→
C
=
MndToCat
M
2
mndtccat.m
⊢
φ
→
M
∈
Mnd
3
eqidd
⊢
φ
→
Base
C
=
Base
C
4
eqidd
⊢
φ
→
Hom
C
=
Hom
C
5
eqidd
⊢
φ
→
comp
C
=
comp
C
6
fvexd
⊢
φ
→
MndToCat
M
∈
V
7
1
6
eqeltrd
⊢
φ
→
C
∈
V
8
biid
⊢
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
↔
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
9
eqid
⊢
Base
M
=
Base
M
10
eqid
⊢
0
M
=
0
M
11
9
10
mndidcl
⊢
M
∈
Mnd
→
0
M
∈
Base
M
12
2
11
syl
⊢
φ
→
0
M
∈
Base
M
13
12
adantr
⊢
φ
∧
y
∈
Base
C
→
0
M
∈
Base
M
14
1
adantr
⊢
φ
∧
y
∈
Base
C
→
C
=
MndToCat
M
15
2
adantr
⊢
φ
∧
y
∈
Base
C
→
M
∈
Mnd
16
eqidd
⊢
φ
∧
y
∈
Base
C
→
Base
C
=
Base
C
17
simpr
⊢
φ
∧
y
∈
Base
C
→
y
∈
Base
C
18
eqidd
⊢
φ
∧
y
∈
Base
C
→
Hom
C
=
Hom
C
19
14
15
16
17
17
18
mndtchom
⊢
φ
∧
y
∈
Base
C
→
y
Hom
C
y
=
Base
M
20
13
19
eleqtrrd
⊢
φ
∧
y
∈
Base
C
→
0
M
∈
y
Hom
C
y
21
1
adantr
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
C
=
MndToCat
M
22
2
adantr
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
M
∈
Mnd
23
eqidd
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
Base
C
=
Base
C
24
simpr1l
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
x
∈
Base
C
25
simpr1r
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
y
∈
Base
C
26
eqidd
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
comp
C
=
comp
C
27
21
22
23
24
25
25
26
mndtcco
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
x
y
comp
C
y
=
+
M
28
27
oveqd
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
0
M
x
y
comp
C
y
f
=
0
M
+
M
f
29
simpr31
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
f
∈
x
Hom
C
y
30
eqidd
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
Hom
C
=
Hom
C
31
21
22
23
24
25
30
mndtchom
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
x
Hom
C
y
=
Base
M
32
29
31
eleqtrd
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
f
∈
Base
M
33
eqid
⊢
+
M
=
+
M
34
9
33
10
mndlid
⊢
M
∈
Mnd
∧
f
∈
Base
M
→
0
M
+
M
f
=
f
35
22
32
34
syl2anc
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
0
M
+
M
f
=
f
36
28
35
eqtrd
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
0
M
x
y
comp
C
y
f
=
f
37
simpr2l
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
z
∈
Base
C
38
21
22
23
25
25
37
26
mndtcco
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
y
y
comp
C
z
=
+
M
39
38
oveqd
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
g
y
y
comp
C
z
0
M
=
g
+
M
0
M
40
simpr32
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
g
∈
y
Hom
C
z
41
21
22
23
25
37
30
mndtchom
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
y
Hom
C
z
=
Base
M
42
40
41
eleqtrd
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
g
∈
Base
M
43
9
33
10
mndrid
⊢
M
∈
Mnd
∧
g
∈
Base
M
→
g
+
M
0
M
=
g
44
22
42
43
syl2anc
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
g
+
M
0
M
=
g
45
39
44
eqtrd
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
g
y
y
comp
C
z
0
M
=
g
46
9
33
mndcl
⊢
M
∈
Mnd
∧
g
∈
Base
M
∧
f
∈
Base
M
→
g
+
M
f
∈
Base
M
47
22
42
32
46
syl3anc
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
g
+
M
f
∈
Base
M
48
21
22
23
24
25
37
26
mndtcco
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
x
y
comp
C
z
=
+
M
49
48
oveqd
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
g
x
y
comp
C
z
f
=
g
+
M
f
50
21
22
23
24
37
30
mndtchom
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
x
Hom
C
z
=
Base
M
51
47
49
50
3eltr4d
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
g
x
y
comp
C
z
f
∈
x
Hom
C
z
52
simpr33
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
k
∈
z
Hom
C
w
53
simpr2r
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
w
∈
Base
C
54
21
22
23
37
53
30
mndtchom
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
z
Hom
C
w
=
Base
M
55
52
54
eleqtrd
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
k
∈
Base
M
56
9
33
mndass
⊢
M
∈
Mnd
∧
k
∈
Base
M
∧
g
∈
Base
M
∧
f
∈
Base
M
→
k
+
M
g
+
M
f
=
k
+
M
g
+
M
f
57
22
55
42
32
56
syl13anc
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
k
+
M
g
+
M
f
=
k
+
M
g
+
M
f
58
21
22
23
24
25
53
26
mndtcco
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
x
y
comp
C
w
=
+
M
59
21
22
23
25
37
53
26
mndtcco
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
y
z
comp
C
w
=
+
M
60
59
oveqd
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
k
y
z
comp
C
w
g
=
k
+
M
g
61
eqidd
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
f
=
f
62
58
60
61
oveq123d
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
k
y
z
comp
C
w
g
x
y
comp
C
w
f
=
k
+
M
g
+
M
f
63
21
22
23
24
37
53
26
mndtcco
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
x
z
comp
C
w
=
+
M
64
eqidd
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
k
=
k
65
63
64
49
oveq123d
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
k
x
z
comp
C
w
g
x
y
comp
C
z
f
=
k
+
M
g
+
M
f
66
57
62
65
3eqtr4d
⊢
φ
∧
x
∈
Base
C
∧
y
∈
Base
C
∧
z
∈
Base
C
∧
w
∈
Base
C
∧
f
∈
x
Hom
C
y
∧
g
∈
y
Hom
C
z
∧
k
∈
z
Hom
C
w
→
k
y
z
comp
C
w
g
x
y
comp
C
w
f
=
k
x
z
comp
C
w
g
x
y
comp
C
z
f
67
3
4
5
7
8
20
36
45
51
66
iscatd2
⊢
φ
→
C
∈
Cat
∧
Id
C
=
y
∈
Base
C
⟼
0
M