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

Metamath Proof Explorer

Theorem oppchomf

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

Ref Expression
Hypotheses oppcbas.1 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppchomf.h ⊢ 𝐻 = ( Homf ‘ 𝐶 )
Assertion oppchomf tpos 𝐻 = ( Homf ‘ 𝑂 )

Proof

Step Hyp Ref Expression
1 oppcbas.1 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 oppchomf.h ⊢ 𝐻 = ( Homf ‘ 𝐶 )
3 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
4 3 1 oppchom ⊢ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑥 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 )
5 4 a1i ⊢ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ( Hom ‘ 𝑂 ) 𝑥 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
6 5 mpoeq3ia ⊢ ( 𝑦 ∈ ( Base ‘ 𝐶 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑥 ) ) = ( 𝑦 ∈ ( Base ‘ 𝐶 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
7 eqid ⊢ ( Homf ‘ 𝑂 ) = ( Homf ‘ 𝑂 )
8 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9 1 8 oppcbas ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
10 eqid ⊢ ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 )
11 7 9 10 homffval ⊢ ( Homf ‘ 𝑂 ) = ( 𝑦 ∈ ( Base ‘ 𝐶 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑥 ) )
12 2 8 3 homffval ⊢ 𝐻 = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
13 12 tposmpo ⊢ tpos 𝐻 = ( 𝑦 ∈ ( Base ‘ 𝐶 ) , 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
14 6 11 13 3eqtr4ri ⊢ tpos 𝐻 = ( Homf ‘ 𝑂 )