Metamath Proof Explorer

Theorem oppchomfval

Description: Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017) (Proof shortened by AV, 14-Oct-2024)

Ref Expression
Hypotheses oppchom.h ⊢H=Hom⁡C
oppchom.o ⊢O=oppCat⁡C
Assertion oppchomfval ⊢tposH=Hom⁡O

Proof

Step Hyp Ref Expression
1 oppchom.h ⊢H=Hom⁡C
2 oppchom.o ⊢O=oppCat⁡C
3 homid ⊢Hom=SlotHom⁡ndx
4 slotsbhcdif ⊢Basendx≠Hom⁡ndx∧Basendx≠comp⁡ndx∧Hom⁡ndx≠comp⁡ndx
5 4 simp3i ⊢Hom⁡ndx≠comp⁡ndx
6 3 5 setsnid ⊢Hom⁡CsSetHom⁡ndxtposH=Hom⁡CsSetHom⁡ndxtposHsSetcomp⁡ndxu∈BaseC×BaseC,z∈BaseC⟼tposz2nd⁡ucomp⁡C1st⁡u
7 1 fvexi ⊢H∈V
8 7 tposex ⊢tposH∈V
9 3 setsid ⊢C∈V∧tposH∈V→tposH=Hom⁡CsSetHom⁡ndxtposH
10 8 9 mpan2 ⊢C∈V→tposH=Hom⁡CsSetHom⁡ndxtposH
11 eqid ⊢BaseC=BaseC
12 eqid ⊢comp⁡C=comp⁡C
13 11 1 12 2 oppcval ⊢C∈V→O=CsSetHom⁡ndxtposHsSetcomp⁡ndxu∈BaseC×BaseC,z∈BaseC⟼tposz2nd⁡ucomp⁡C1st⁡u
14 13 fveq2d ⊢C∈V→Hom⁡O=Hom⁡CsSetHom⁡ndxtposHsSetcomp⁡ndxu∈BaseC×BaseC,z∈BaseC⟼tposz2nd⁡ucomp⁡C1st⁡u
15 6 10 14 3eqtr4a ⊢C∈V→tposH=Hom⁡O
16 tpos0 ⊢tpos∅=∅
17 fvprc ⊢¬C∈V→Hom⁡C=∅
18 1 17 eqtrid ⊢¬C∈V→H=∅
19 18 tposeqd ⊢¬C∈V→tposH=tpos∅
20 fvprc ⊢¬C∈V→oppCat⁡C=∅
21 2 20 eqtrid ⊢¬C∈V→O=∅
22 21 fveq2d ⊢¬C∈V→Hom⁡O=Hom⁡∅
23 3 str0 ⊢∅=Hom⁡∅
24 22 23 eqtr4di ⊢¬C∈V→Hom⁡O=∅
25 16 19 24 3eqtr4a ⊢¬C∈V→tposH=Hom⁡O
26 15 25 pm2.61i ⊢tposH=Hom⁡O