Database
BASIC CATEGORY THEORY
Arrows (disjointified hom-sets)
Identity and composition for arrows
idafval
Next ⟩
idaval
Metamath Proof Explorer
Ascii
Unicode
Theorem
idafval
Description:
Value of the identity arrow function.
(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
Assertion
idafval
⊢
φ
→
I
=
x
∈
B
⟼
x
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
fveq2
⊢
c
=
C
→
Base
c
=
Base
C
6
5
2
eqtr4di
⊢
c
=
C
→
Base
c
=
B
7
fveq2
⊢
c
=
C
→
Id
⁡
c
=
Id
⁡
C
8
7
4
eqtr4di
⊢
c
=
C
→
Id
⁡
c
=
1
˙
9
8
fveq1d
⊢
c
=
C
→
Id
⁡
c
⁡
x
=
1
˙
⁡
x
10
9
oteq3d
⊢
c
=
C
→
x
x
Id
⁡
c
⁡
x
=
x
x
1
˙
⁡
x
11
6
10
mpteq12dv
⊢
c
=
C
→
x
∈
Base
c
⟼
x
x
Id
⁡
c
⁡
x
=
x
∈
B
⟼
x
x
1
˙
⁡
x
12
df-ida
⊢
Id
a
=
c
∈
Cat
⟼
x
∈
Base
c
⟼
x
x
Id
⁡
c
⁡
x
13
11
12
2
mptfvmpt
⊢
C
∈
Cat
→
Id
a
⁡
C
=
x
∈
B
⟼
x
x
1
˙
⁡
x
14
3
13
syl
⊢
φ
→
Id
a
⁡
C
=
x
∈
B
⟼
x
x
1
˙
⁡
x
15
1
14
eqtrid
⊢
φ
→
I
=
x
∈
B
⟼
x
x
1
˙
⁡
x