Theorem oppcid

Description: Identity function of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	oppcbas.1	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	oppcid.2	$$⊢B=\mathrm{Id}\left(C\right)$$
Assertion	oppcid	$$⊢C\in \mathrm{Cat}\to \mathrm{Id}\left(O\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		oppcbas.1	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		oppcid.2	$$⊢B=\mathrm{Id}\left(C\right)$$
3	1	oppccatid	$$⊢C\in \mathrm{Cat}\to \left(O\in \mathrm{Cat}\wedge \mathrm{Id}\left(O\right)=\mathrm{Id}\left(C\right)\right)$$
4	3	simprd	$$⊢C\in \mathrm{Cat}\to \mathrm{Id}\left(O\right)=\mathrm{Id}\left(C\right)$$
5	4 2	eqtr4di	$$⊢C\in \mathrm{Cat}\to \mathrm{Id}\left(O\right)=B$$