Theorem idafval

Description: Value of the identity arrow function. (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)$$
Assertion	idafval	$$⊢\phi \to I=\left(x\in B⟼⟨x,x,\underset{\dot{}}{1}\left(x\right)⟩\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		fveq2	$$⊢c=C\to {\mathrm{Base}}_c={\mathrm{Base}}_C$$
6	5 2	eqtr4di	$$⊢c=C\to {\mathrm{Base}}_c=B$$
7		fveq2	$$⊢c=C\to \mathrm{Id}\left(c\right)=\mathrm{Id}\left(C\right)$$
8	7 4	eqtr4di	$$⊢c=C\to \mathrm{Id}\left(c\right)=\underset{\dot{}}{1}$$
9	8	fveq1d	$$⊢c=C\to \mathrm{Id}\left(c\right)\left(x\right)=\underset{\dot{}}{1}\left(x\right)$$
10	9	oteq3d	$$⊢c=C\to ⟨x,x,\mathrm{Id}\left(c\right)\left(x\right)⟩=⟨x,x,\underset{\dot{}}{1}\left(x\right)⟩$$
11	6 10	mpteq12dv	$$⊢c=C\to \left(x\in {\mathrm{Base}}_c⟼⟨x,x,\mathrm{Id}\left(c\right)\left(x\right)⟩\right)=\left(x\in B⟼⟨x,x,\underset{\dot{}}{1}\left(x\right)⟩\right)$$
12		df-ida	$$⊢{Id}_a=\left(c\in \mathrm{Cat}⟼\left(x\in {\mathrm{Base}}_c⟼⟨x,x,\mathrm{Id}\left(c\right)\left(x\right)⟩\right)\right)$$
13	11 12 2	mptfvmpt	$$⊢C\in \mathrm{Cat}\to {Id}_a\left(C\right)=\left(x\in B⟼⟨x,x,\underset{\dot{}}{1}\left(x\right)⟩\right)$$
14	3 13	syl	$$⊢\phi \to {Id}_a\left(C\right)=\left(x\in B⟼⟨x,x,\underset{\dot{}}{1}\left(x\right)⟩\right)$$
15	1 14	eqtrid	$$⊢\phi \to I=\left(x\in B⟼⟨x,x,\underset{\dot{}}{1}\left(x\right)⟩\right)$$