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 = ( oppCat ` C )
Assertion	2oppchomf	|- ( Homf ` C ) = ( Homf ` ( oppCat ` O ) )

Proof

Step	Hyp	Ref	Expression
1		oppcbas.1	|- O = ( oppCat ` C )
2		eqid	|- ( Homf ` C ) = ( Homf ` C )
3		eqid	|- ( Base ` C ) = ( Base ` C )
4	2 3	homffn	|- ( Homf ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) )
5		fnrel	|- ( ( Homf ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) -> Rel ( Homf ` C ) )
6	4 5	ax-mp	|- Rel ( Homf ` C )
7		relxp	|- Rel ( ( Base ` C ) X. ( Base ` C ) )
8	4	fndmi	|- dom ( Homf ` C ) = ( ( Base ` C ) X. ( Base ` C ) )
9	8	releqi	|- ( Rel dom ( Homf ` C ) <-> Rel ( ( Base ` C ) X. ( Base ` C ) ) )
10	7 9	mpbir	|- Rel dom ( Homf ` C )
11		tpostpos2	|- ( ( Rel ( Homf ` C ) /\ Rel dom ( Homf ` C ) ) -> tpos tpos ( Homf ` C ) = ( Homf ` C ) )
12	6 10 11	mp2an	|- tpos tpos ( Homf ` C ) = ( Homf ` C )
13		eqid	|- ( oppCat ` O ) = ( oppCat ` O )
14	1 2	oppchomf	|- tpos ( Homf ` C ) = ( Homf ` O )
15	13 14	oppchomf	|- tpos tpos ( Homf ` C ) = ( Homf ` ( oppCat ` O ) )
16	12 15	eqtr3i	|- ( Homf ` C ) = ( Homf ` ( oppCat ` O ) )