Theorem ida2

Description: Morphism part of the identity arrow. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	idafval.i	$$⊢I={Id}_a\left(C\right)$$
	idafval.b	$$⊢B={\mathrm{Base}}_C$$
	idafval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	idafval.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	idaval.x	$$⊢\phi \to X\in B$$
Assertion	ida2	$$⊢\phi \to 2^{nd}\left(I\left(X\right)\right)=\underset{\dot{}}{1}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		idafval.i	$$⊢I={Id}_a\left(C\right)$$
2		idafval.b	$$⊢B={\mathrm{Base}}_C$$
3		idafval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		idafval.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
5		idaval.x	$$⊢\phi \to X\in B$$
6	1 2 3 4 5	idaval	$$⊢\phi \to I\left(X\right)=⟨X,X,\underset{\dot{}}{1}\left(X\right)⟩$$
7	6	fveq2d	$$⊢\phi \to 2^{nd}\left(I\left(X\right)\right)=2^{nd}\left(⟨X,X,\underset{\dot{}}{1}\left(X\right)⟩\right)$$
8		fvex	$$⊢\underset{\dot{}}{1}\left(X\right)\in \mathrm{V}$$
9		ot3rdg	$$⊢\underset{\dot{}}{1}\left(X\right)\in \mathrm{V}\to 2^{nd}\left(⟨X,X,\underset{\dot{}}{1}\left(X\right)⟩\right)=\underset{\dot{}}{1}\left(X\right)$$
10	8 9	ax-mp	$$⊢2^{nd}\left(⟨X,X,\underset{\dot{}}{1}\left(X\right)⟩\right)=\underset{\dot{}}{1}\left(X\right)$$
11	7 10	syl6eq	$$⊢\phi \to 2^{nd}\left(I\left(X\right)\right)=\underset{\dot{}}{1}\left(X\right)$$