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 ⊢ 𝐻 = ( Hom ‘ 𝐶 )
oppchom.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
Assertion oppchomfval tpos 𝐻 = ( Hom ‘ 𝑂 )

Proof

Step Hyp Ref Expression
1 oppchom.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
2 oppchom.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
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 ‘ ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos 𝐻 ⟩ ) ) = ( Hom ‘ ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos 𝐻 ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) )
7 1 fvexi ⊢ 𝐻 ∈ V
8 7 tposex ⊢ tpos 𝐻 ∈ V
9 3 setsid ⊢ ( ( 𝐶 ∈ V ∧ tpos 𝐻 ∈ V ) → tpos 𝐻 = ( Hom ‘ ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos 𝐻 ⟩ ) ) )
10 8 9 mpan2 ⊢ ( 𝐶 ∈ V → tpos 𝐻 = ( Hom ‘ ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos 𝐻 ⟩ ) ) )
11 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
12 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
13 11 1 12 2 oppcval ⊢ ( 𝐶 ∈ V → 𝑂 = ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos 𝐻 ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) )
14 13 fveq2d ⊢ ( 𝐶 ∈ V → ( Hom ‘ 𝑂 ) = ( Hom ‘ ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos 𝐻 ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) , 𝑧 ∈ ( Base ‘ 𝐶 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) ) )
15 6 10 14 3eqtr4a ⊢ ( 𝐶 ∈ V → tpos 𝐻 = ( Hom ‘ 𝑂 ) )
16 tpos0 ⊢ tpos ∅ = ∅
17 fvprc ⊢ ( ¬ 𝐶 ∈ V → ( Hom ‘ 𝐶 ) = ∅ )
18 1 17 eqtrid ⊢ ( ¬ 𝐶 ∈ V → 𝐻 = ∅ )
19 18 tposeqd ⊢ ( ¬ 𝐶 ∈ V → tpos 𝐻 = tpos ∅ )
20 fvprc ⊢ ( ¬ 𝐶 ∈ V → ( oppCat ‘ 𝐶 ) = ∅ )
21 2 20 eqtrid ⊢ ( ¬ 𝐶 ∈ V → 𝑂 = ∅ )
22 21 fveq2d ⊢ ( ¬ 𝐶 ∈ V → ( Hom ‘ 𝑂 ) = ( Hom ‘ ∅ ) )
23 3 str0 ⊢ ∅ = ( Hom ‘ ∅ )
24 22 23 eqtr4di ⊢ ( ¬ 𝐶 ∈ V → ( Hom ‘ 𝑂 ) = ∅ )
25 16 19 24 3eqtr4a ⊢ ( ¬ 𝐶 ∈ V → tpos 𝐻 = ( Hom ‘ 𝑂 ) )
26 15 25 pm2.61i ⊢ tpos 𝐻 = ( Hom ‘ 𝑂 )