Theorem tendo02

Description: Value of additive identity endomorphism. (Contributed by NM, 11-Jun-2013)

	Ref	Expression
Hypotheses	tendo0cbv.o	$$⊢O=\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)$$
	tendo02.b	$$⊢B={\mathrm{Base}}_K$$
Assertion	tendo02	$$⊢F\in T\to O\left(F\right)={\mathrm{I}\upharpoonright }_B$$

Proof

Step	Hyp	Ref	Expression
1		tendo0cbv.o	$$⊢O=\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)$$
2		tendo02.b	$$⊢B={\mathrm{Base}}_K$$
3		eqidd	$$⊢g=F\to {\mathrm{I}\upharpoonright }_B={\mathrm{I}\upharpoonright }_B$$
4	1	tendo0cbv	$$⊢O=\left(g\in T⟼{\mathrm{I}\upharpoonright }_B\right)$$
5		funi	$$⊢\mathrm{Fun}\mathrm{I}$$
6	2	fvexi	$$⊢B\in \mathrm{V}$$
7		resfunexg	$$⊢\left(\mathrm{Fun}\mathrm{I}\wedge B\in \mathrm{V}\right)\to {\mathrm{I}\upharpoonright }_B\in \mathrm{V}$$
8	5 6 7	mp2an	$$⊢{\mathrm{I}\upharpoonright }_B\in \mathrm{V}$$
9	3 4 8	fvmpt	$$⊢F\in T\to O\left(F\right)={\mathrm{I}\upharpoonright }_B$$