Metamath Proof Explorer


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