Database
BASIC CATEGORY THEORY
Arrows (disjointified hom-sets)
Identity and composition for arrows
ida2
Next ⟩
idahom
Metamath Proof Explorer
Ascii
Unicode
Theorem
ida2
Description:
Morphism part of the identity arrow.
(Contributed by
Mario Carneiro
, 11-Jan-2017)
Ref
Expression
Hypotheses
idafval.i
⊢
I
=
Id
a
⁡
C
idafval.b
⊢
B
=
Base
C
idafval.c
⊢
φ
→
C
∈
Cat
idafval.1
⊢
1
˙
=
Id
⁡
C
idaval.x
⊢
φ
→
X
∈
B
Assertion
ida2
⊢
φ
→
2
nd
⁡
I
⁡
X
=
1
˙
⁡
X
Proof
Step
Hyp
Ref
Expression
1
idafval.i
⊢
I
=
Id
a
⁡
C
2
idafval.b
⊢
B
=
Base
C
3
idafval.c
⊢
φ
→
C
∈
Cat
4
idafval.1
⊢
1
˙
=
Id
⁡
C
5
idaval.x
⊢
φ
→
X
∈
B
6
1
2
3
4
5
idaval
⊢
φ
→
I
⁡
X
=
X
X
1
˙
⁡
X
7
6
fveq2d
⊢
φ
→
2
nd
⁡
I
⁡
X
=
2
nd
⁡
X
X
1
˙
⁡
X
8
fvex
⊢
1
˙
⁡
X
∈
V
9
ot3rdg
⊢
1
˙
⁡
X
∈
V
→
2
nd
⁡
X
X
1
˙
⁡
X
=
1
˙
⁡
X
10
8
9
ax-mp
⊢
2
nd
⁡
X
X
1
˙
⁡
X
=
1
˙
⁡
X
11
7
10
eqtrdi
⊢
φ
→
2
nd
⁡
I
⁡
X
=
1
˙
⁡
X