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 ( ⟨ 𝑍 , 𝑌· 𝑋 ) )