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	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
Assertion	2oppchomf	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		oppcbas.1	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		eqid	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
3		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
4	2 3	homffn	⊢ ( Homf ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
5		fnrel	⊢ ( ( Homf ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) → Rel ( Homf ‘ 𝐶 ) )
6	4 5	ax-mp	⊢ Rel ( Homf ‘ 𝐶 )
7		relxp	⊢ Rel ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
8	4	fndmi	⊢ dom ( Homf ‘ 𝐶 ) = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
9	8	releqi	⊢ ( Rel dom ( Homf ‘ 𝐶 ) ↔ Rel ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
10	7 9	mpbir	⊢ Rel dom ( Homf ‘ 𝐶 )
11		tpostpos2	⊢ ( ( Rel ( Homf ‘ 𝐶 ) ∧ Rel dom ( Homf ‘ 𝐶 ) ) → tpos tpos ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 ) )
12	6 10 11	mp2an	⊢ tpos tpos ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
13		eqid	⊢ ( oppCat ‘ 𝑂 ) = ( oppCat ‘ 𝑂 )
14	1 2	oppchomf	⊢ tpos ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝑂 )
15	13 14	oppchomf	⊢ tpos tpos ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) )
16	12 15	eqtr3i	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) )