This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑂 ) )