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 ⊢ tpos H = Hom ⁡ O

Proof

Step Hyp Ref Expression
1 oppchom.h ⊢ H = Hom ⁡ C
2 oppchom.o ⊢ O = oppCat ⁡ C
3 homid ⊢ Hom = Slot Hom ⁡ ndx
4 slotsbhcdif ⊢ Base ndx ≠ Hom ⁡ ndx ∧ Base ndx ≠ comp ⁡ ndx ∧ Hom ⁡ ndx ≠ comp ⁡ ndx
5 4 simp3i ⊢ Hom ⁡ ndx ≠ comp ⁡ ndx
6 3 5 setsnid ⊢ Hom ⁡ C sSet Hom ⁡ ndx tpos H = Hom ⁡ C sSet Hom ⁡ ndx tpos H sSet comp ⁡ ndx u ∈ Base C × Base C , z ∈ Base C ⟼ tpos z 2 nd ⁡ u comp ⁡ C 1 st ⁡ u
7 1 fvexi ⊢ H ∈ V
8 7 tposex ⊢ tpos H ∈ V
9 3 setsid ⊢ C ∈ V ∧ tpos H ∈ V → tpos H = Hom ⁡ C sSet Hom ⁡ ndx tpos H
10 8 9 mpan2 ⊢ C ∈ V → tpos H = Hom ⁡ C sSet Hom ⁡ ndx tpos H
11 eqid ⊢ Base C = Base C
12 eqid ⊢ comp ⁡ C = comp ⁡ C
13 11 1 12 2 oppcval ⊢ C ∈ V → O = C sSet Hom ⁡ ndx tpos H sSet comp ⁡ ndx u ∈ Base C × Base C , z ∈ Base C ⟼ tpos z 2 nd ⁡ u comp ⁡ C 1 st ⁡ u
14 13 fveq2d ⊢ C ∈ V → Hom ⁡ O = Hom ⁡ C sSet Hom ⁡ ndx tpos H sSet comp ⁡ ndx u ∈ Base C × Base C , z ∈ Base C ⟼ tpos z 2 nd ⁡ u comp ⁡ C 1 st ⁡ u
15 6 10 14 3eqtr4a ⊢ C ∈ V → tpos H = Hom ⁡ O
16 tpos0 ⊢ tpos ∅ = ∅
17 fvprc ⊢ ¬ C ∈ V → Hom ⁡ C = ∅
18 1 17 eqtrid ⊢ ¬ C ∈ V → H = ∅
19 18 tposeqd ⊢ ¬ C ∈ V → tpos H = 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 → tpos H = Hom ⁡ O
26 15 25 pm2.61i ⊢ tpos H = Hom ⁡ O