Metamath Proof Explorer


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