Database
BASIC CATEGORY THEORY
Categorical constructions
Hom functor
yonval
Next ⟩
yoncl
Metamath Proof Explorer
Ascii
Unicode
Theorem
yonval
Description:
Value of the Yoneda embedding.
(Contributed by
Mario Carneiro
, 17-Jan-2017)
Ref
Expression
Hypotheses
yonval.y
⊢
Y
=
Yon
⁡
C
yonval.c
⊢
φ
→
C
∈
Cat
yonval.o
⊢
O
=
oppCat
⁡
C
yonval.m
⊢
M
=
Hom
F
⁡
O
Assertion
yonval
⊢
φ
→
Y
=
C
O
curry
F
M
Proof
Step
Hyp
Ref
Expression
1
yonval.y
⊢
Y
=
Yon
⁡
C
2
yonval.c
⊢
φ
→
C
∈
Cat
3
yonval.o
⊢
O
=
oppCat
⁡
C
4
yonval.m
⊢
M
=
Hom
F
⁡
O
5
df-yon
⊢
Yon
=
c
∈
Cat
⟼
c
oppCat
⁡
c
curry
F
Hom
F
⁡
oppCat
⁡
c
6
simpr
⊢
φ
∧
c
=
C
→
c
=
C
7
6
fveq2d
⊢
φ
∧
c
=
C
→
oppCat
⁡
c
=
oppCat
⁡
C
8
7
3
eqtr4di
⊢
φ
∧
c
=
C
→
oppCat
⁡
c
=
O
9
6
8
opeq12d
⊢
φ
∧
c
=
C
→
c
oppCat
⁡
c
=
C
O
10
8
fveq2d
⊢
φ
∧
c
=
C
→
Hom
F
⁡
oppCat
⁡
c
=
Hom
F
⁡
O
11
10
4
eqtr4di
⊢
φ
∧
c
=
C
→
Hom
F
⁡
oppCat
⁡
c
=
M
12
9
11
oveq12d
⊢
φ
∧
c
=
C
→
c
oppCat
⁡
c
curry
F
Hom
F
⁡
oppCat
⁡
c
=
C
O
curry
F
M
13
ovexd
⊢
φ
→
C
O
curry
F
M
∈
V
14
5
12
2
13
fvmptd2
⊢
φ
→
Yon
⁡
C
=
C
O
curry
F
M
15
1
14
syl5eq
⊢
φ
→
Y
=
C
O
curry
F
M