Theorem 2oppchomf

Description: The double opposite category has the same morphisms as the original category. Intended for use with property lemmas such as monpropd . (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypothesis	oppcbas.1	$$⊢O=\mathrm{oppCat}\left(C\right)$$
Assertion	2oppchomf	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		oppcbas.1	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
3		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
4	2 3	homffn	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
5		fnrel	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\to \mathrm{Rel}{\mathrm{Hom}}_{𝑓}\left(C\right)$$
6	4 5	ax-mp	$$⊢\mathrm{Rel}{\mathrm{Hom}}_{𝑓}\left(C\right)$$
7		relxp	$$⊢\mathrm{Rel}\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
8	4	fndmi	$$⊢\mathrm{dom}{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Base}}_C\times {\mathrm{Base}}_C$$
9	8	releqi	$$⊢\mathrm{Rel}\mathrm{dom}{\mathrm{Hom}}_{𝑓}\left(C\right)\leftrightarrow \mathrm{Rel}\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
10	7 9	mpbir	$$⊢\mathrm{Rel}\mathrm{dom}{\mathrm{Hom}}_{𝑓}\left(C\right)$$
11		tpostpos2	$$⊢\left(\mathrm{Rel}{\mathrm{Hom}}_{𝑓}\left(C\right)\wedge \mathrm{Rel}\mathrm{dom}{\mathrm{Hom}}_{𝑓}\left(C\right)\right)\to tpostpos{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
12	6 10 11	mp2an	$$⊢tpostpos{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
13		eqid	$$⊢\mathrm{oppCat}\left(O\right)=\mathrm{oppCat}\left(O\right)$$
14	1 2	oppchomf	$$⊢tpos{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(O\right)$$
15	13 14	oppchomf	$$⊢tpostpos{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
16	12 15	eqtr3i	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$