Metamath Proof Explorer

Theorem funcoppc

Description: A functor on categories yields a functor on the opposite categories (in the same direction), see definition 3.41 of Adamek p. 39. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses funcoppc.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
funcoppc.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
funcoppc.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
Assertion funcoppc ( 𝜑 → 𝐹 ( 𝑂 Func 𝑃 ) tpos 𝐺 )

Proof

Step Hyp Ref Expression
1 funcoppc.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 funcoppc.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3 funcoppc.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
4 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5 1 4 oppcbas ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
6 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
7 2 6 oppcbas ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝑃 )
8 eqid ⊢ ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 )
9 eqid ⊢ ( Hom ‘ 𝑃 ) = ( Hom ‘ 𝑃 )
10 eqid ⊢ ( Id ‘ 𝑂 ) = ( Id ‘ 𝑂 )
11 eqid ⊢ ( Id ‘ 𝑃 ) = ( Id ‘ 𝑃 )
12 eqid ⊢ ( comp ‘ 𝑂 ) = ( comp ‘ 𝑂 )
13 eqid ⊢ ( comp ‘ 𝑃 ) = ( comp ‘ 𝑃 )
14 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
15 3 14 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
16 funcrcl ⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
17 15 16 syl ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
18 17 simpld ⊢ ( 𝜑 → 𝐶 ∈ Cat )
19 1 oppccat ⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
20 18 19 syl ⊢ ( 𝜑 → 𝑂 ∈ Cat )
21 2 oppccat ⊢ ( 𝐷 ∈ Cat → 𝑃 ∈ Cat )
22 17 21 simpl2im ⊢ ( 𝜑 → 𝑃 ∈ Cat )
23 4 6 3 funcf1 ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
24 4 3 funcfn2 ⊢ ( 𝜑 → 𝐺 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
25 tposfn ⊢ ( 𝐺 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) → tpos 𝐺 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
26 24 25 syl ⊢ ( 𝜑 → tpos 𝐺 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
27 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
28 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
29 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
30 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
31 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
32 4 27 28 29 30 31 funcf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑦 𝐺 𝑥 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ⟶ ( ( 𝐹 ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑥 ) ) )
33 ovtpos ⊢ ( 𝑥 tpos 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 )
34 33 feq1i ⊢ ( ( 𝑥 tpos 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑦 𝐺 𝑥 ) : ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) )
35 27 1 oppchom ⊢ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 )
36 28 2 oppchom ⊢ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑥 ) )
37 35 36 feq23i ⊢ ( ( 𝑦 𝐺 𝑥 ) : ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑦 𝐺 𝑥 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ⟶ ( ( 𝐹 ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑥 ) ) )
38 34 37 bitri ⊢ ( ( 𝑥 tpos 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑦 𝐺 𝑥 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ⟶ ( ( 𝐹 ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑥 ) ) )
39 32 38 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 tpos 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) )
40 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
41 eqid ⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
42 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
43 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
44 4 40 41 42 43 funcid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
45 ovtpos ⊢ ( 𝑥 tpos 𝐺 𝑥 ) = ( 𝑥 𝐺 𝑥 )
46 45 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 tpos 𝐺 𝑥 ) = ( 𝑥 𝐺 𝑥 ) )
47 1 40 oppcid ⊢ ( 𝐶 ∈ Cat → ( Id ‘ 𝑂 ) = ( Id ‘ 𝐶 ) )
48 18 47 syl ⊢ ( 𝜑 → ( Id ‘ 𝑂 ) = ( Id ‘ 𝐶 ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( Id ‘ 𝑂 ) = ( Id ‘ 𝐶 ) )
50 49 fveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝑂 ) ‘ 𝑥 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) )
51 46 50 fveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 tpos 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝑂 ) ‘ 𝑥 ) ) = ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) )
52 2 41 oppcid ⊢ ( 𝐷 ∈ Cat → ( Id ‘ 𝑃 ) = ( Id ‘ 𝐷 ) )
53 17 52 simpl2im ⊢ ( 𝜑 → ( Id ‘ 𝑃 ) = ( Id ‘ 𝐷 ) )
54 53 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( Id ‘ 𝑃 ) = ( Id ‘ 𝐷 ) )
55 54 fveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝑃 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
56 44 51 55 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 tpos 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝑂 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑃 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
57 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
58 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
59 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
60 simp23 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
61 simp22 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
62 simp21 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
63 simp3r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) )
64 27 1 oppchom ⊢ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) = ( 𝑧 ( Hom ‘ 𝐶 ) 𝑦 )
65 63 64 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑦 ) )
66 simp3l ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) )
67 66 35 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) )
68 4 27 57 58 59 60 61 62 65 67 funcco ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → ( ( 𝑧 𝐺 𝑥 ) ‘ ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑔 ) ) = ( ( ( 𝑦 𝐺 𝑥 ) ‘ 𝑓 ) ( ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑥 ) ) ( ( 𝑧 𝐺 𝑦 ) ‘ 𝑔 ) ) )
69 4 57 1 62 61 60 oppcco ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) 𝑓 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑔 ) )
70 69 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → ( ( 𝑧 𝐺 𝑥 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) 𝑓 ) ) = ( ( 𝑧 𝐺 𝑥 ) ‘ ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑔 ) ) )
71 23 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
72 71 62 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
73 71 61 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
74 71 60 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) )
75 6 58 2 72 73 74 oppcco ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → ( ( ( 𝑧 𝐺 𝑦 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑦 𝐺 𝑥 ) ‘ 𝑓 ) ) = ( ( ( 𝑦 𝐺 𝑥 ) ‘ 𝑓 ) ( ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑥 ) ) ( ( 𝑧 𝐺 𝑦 ) ‘ 𝑔 ) ) )
76 68 70 75 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → ( ( 𝑧 𝐺 𝑥 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑧 𝐺 𝑦 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑦 𝐺 𝑥 ) ‘ 𝑓 ) ) )
77 ovtpos ⊢ ( 𝑥 tpos 𝐺 𝑧 ) = ( 𝑧 𝐺 𝑥 )
78 77 fveq1i ⊢ ( ( 𝑥 tpos 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) 𝑓 ) ) = ( ( 𝑧 𝐺 𝑥 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) 𝑓 ) )
79 ovtpos ⊢ ( 𝑦 tpos 𝐺 𝑧 ) = ( 𝑧 𝐺 𝑦 )
80 79 fveq1i ⊢ ( ( 𝑦 tpos 𝐺 𝑧 ) ‘ 𝑔 ) = ( ( 𝑧 𝐺 𝑦 ) ‘ 𝑔 )
81 33 fveq1i ⊢ ( ( 𝑥 tpos 𝐺 𝑦 ) ‘ 𝑓 ) = ( ( 𝑦 𝐺 𝑥 ) ‘ 𝑓 )
82 80 81 oveq12i ⊢ ( ( ( 𝑦 tpos 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 tpos 𝐺 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑧 𝐺 𝑦 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑦 𝐺 𝑥 ) ‘ 𝑓 ) )
83 76 78 82 3eqtr4g ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ) ) → ( ( 𝑥 tpos 𝐺 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑦 tpos 𝐺 𝑧 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 tpos 𝐺 𝑦 ) ‘ 𝑓 ) ) )
84 5 7 8 9 10 11 12 13 20 22 23 26 39 56 83 isfuncd ⊢ ( 𝜑 → 𝐹 ( 𝑂 Func 𝑃 ) tpos 𝐺 )