Theorem oppchomf

Description: Hom-sets of the opposite category. (Contributed by Mario Carneiro, 17-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		oppcbas.1	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		oppchomf.h	$$⊢H={\mathrm{Hom}}_{𝑓}\left(C\right)$$
3		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
4	3 1	oppchom	$$⊢y\mathrm{Hom}\left(O\right)x=x\mathrm{Hom}\left(C\right)y$$
5	4	a1i	$$⊢\left(y\in {\mathrm{Base}}_C\wedge x\in {\mathrm{Base}}_C\right)\to y\mathrm{Hom}\left(O\right)x=x\mathrm{Hom}\left(C\right)y$$
6	5	mpoeq3ia	$$⊢\left(y\in {\mathrm{Base}}_C,x\in {\mathrm{Base}}_C⟼y\mathrm{Hom}\left(O\right)x\right)=\left(y\in {\mathrm{Base}}_C,x\in {\mathrm{Base}}_C⟼x\mathrm{Hom}\left(C\right)y\right)$$
7		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(O\right)={\mathrm{Hom}}_{𝑓}\left(O\right)$$
8		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
9	1 8	oppcbas	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_O$$
10		eqid	$$⊢\mathrm{Hom}\left(O\right)=\mathrm{Hom}\left(O\right)$$
11	7 9 10	homffval	$$⊢{\mathrm{Hom}}_{𝑓}\left(O\right)=\left(y\in {\mathrm{Base}}_C,x\in {\mathrm{Base}}_C⟼y\mathrm{Hom}\left(O\right)x\right)$$
12	2 8 3	homffval	$$⊢H=\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼x\mathrm{Hom}\left(C\right)y\right)$$
13	12	tposmpo	$$⊢tposH=\left(y\in {\mathrm{Base}}_C,x\in {\mathrm{Base}}_C⟼x\mathrm{Hom}\left(C\right)y\right)$$
14	6 11 13	3eqtr4ri	$$⊢tposH={\mathrm{Hom}}_{𝑓}\left(O\right)$$