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

Metamath Proof Explorer

Theorem oppccofval

Description: Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses oppcco.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
oppcco.c ⊢ · = ( comp ‘ 𝐶 )
oppcco.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppcco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
oppcco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
oppcco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion oppccofval ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑍 ) = tpos ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) )

Proof

Step Hyp Ref Expression
1 oppcco.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 oppcco.c ⊢ · = ( comp ‘ 𝐶 )
3 oppcco.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
4 oppcco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 oppcco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 oppcco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
7 elfvex ⊢ ( 𝑋 ∈ ( Base ‘ 𝐶 ) → 𝐶 ∈ V )
8 7 1 eleq2s ⊢ ( 𝑋 ∈ 𝐵 → 𝐶 ∈ V )
9 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
10 1 9 2 3 oppcval ⊢ ( 𝐶 ∈ V → 𝑂 = ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ · ( 1st ‘ 𝑢 ) ) ) ⟩ ) )
11 4 8 10 3syl ⊢ ( 𝜑 → 𝑂 = ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ · ( 1st ‘ 𝑢 ) ) ) ⟩ ) )
12 11 fveq2d ⊢ ( 𝜑 → ( comp ‘ 𝑂 ) = ( comp ‘ ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ · ( 1st ‘ 𝑢 ) ) ) ⟩ ) ) )
13 ovex ⊢ ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) ∈ V
14 1 fvexi ⊢ 𝐵 ∈ V
15 14 14 xpex ⊢ ( 𝐵 × 𝐵 ) ∈ V
16 15 14 mpoex ⊢ ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ · ( 1st ‘ 𝑢 ) ) ) ∈ V
17 ccoid ⊢ comp = Slot ( comp ‘ ndx )
18 17 setsid ⊢ ( ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) ∈ V ∧ ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ · ( 1st ‘ 𝑢 ) ) ) ∈ V ) → ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ · ( 1st ‘ 𝑢 ) ) ) = ( comp ‘ ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ · ( 1st ‘ 𝑢 ) ) ) ⟩ ) ) )
19 13 16 18 mp2an ⊢ ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ · ( 1st ‘ 𝑢 ) ) ) = ( comp ‘ ( ( 𝐶 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝐶 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ · ( 1st ‘ 𝑢 ) ) ) ⟩ ) )
20 12 19 eqtr4di ⊢ ( 𝜑 → ( comp ‘ 𝑂 ) = ( 𝑢 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ · ( 1st ‘ 𝑢 ) ) ) )
21 simprr ⊢ ( ( 𝜑 ∧ ( 𝑢 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → 𝑧 = 𝑍 )
22 simprl ⊢ ( ( 𝜑 ∧ ( 𝑢 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → 𝑢 = ⟨ 𝑋 , 𝑌 ⟩ )
23 22 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑢 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ 𝑢 ) = ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
24 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → 𝑌 ∈ 𝐵 )
25 op2ndg ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
26 4 24 25 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑢 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
27 23 26 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑢 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ 𝑢 ) = 𝑌 )
28 21 27 opeq12d ⊢ ( ( 𝜑 ∧ ( 𝑢 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ = ⟨ 𝑍 , 𝑌 ⟩ )
29 22 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑢 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 1st ‘ 𝑢 ) = ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
30 op1stg ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
31 4 24 30 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑢 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
32 29 31 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑢 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 1st ‘ 𝑢 ) = 𝑋 )
33 28 32 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑢 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ · ( 1st ‘ 𝑢 ) ) = ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) )
34 33 tposeqd ⊢ ( ( 𝜑 ∧ ( 𝑢 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ · ( 1st ‘ 𝑢 ) ) = tpos ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) )
35 4 5 opelxpd ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
36 ovex ⊢ ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ∈ V
37 36 tposex ⊢ tpos ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ∈ V
38 37 a1i ⊢ ( 𝜑 → tpos ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ∈ V )
39 20 34 35 6 38 ovmpod ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑍 ) = tpos ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) )