Metamath Proof Explorer

Theorem precofval2

Description: Value of the pre-composition functor as a transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 11-Oct-2025)

Ref Expression
Hypotheses precofval.q ⊢ Q = C FuncCat D
precofval.r ⊢ R = D FuncCat E
precofval.o No typesetting found for |- ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) ) with typecode |-
precofval.f ⊢ φ → F ∈ C Func D
precofval.e ⊢ φ → E ∈ Cat
precofval.k No typesetting found for |- ( ph -> K = ( ( 1st ` .o. ) ` F ) ) with typecode |-
Assertion precofval2 ⊢ φ → K = g ∈ D Func E ⟼ g ∘ func F g ∈ D Func E , h ∈ D Func E ⟼ a ∈ g D Nat E h ⟼ a ∘ 1 st ⁡ F

Proof

Step Hyp Ref Expression
1 precofval.q ⊢ Q = C FuncCat D
2 precofval.r ⊢ R = D FuncCat E
3 precofval.o Could not format ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) ) : No typesetting found for |- ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) ) with typecode |-
4 precofval.f ⊢ φ → F ∈ C Func D
5 precofval.e ⊢ φ → E ∈ Cat
6 precofval.k Could not format ( ph -> K = ( ( 1st ` .o. ) ` F ) ) : No typesetting found for |- ( ph -> K = ( ( 1st ` .o. ) ` F ) ) with typecode |-
7 1 2 3 4 5 6 precofval ⊢ φ → K = g ∈ D Func E ⟼ g ∘ func F g ∈ D Func E , h ∈ D Func E ⟼ a ∈ g D Nat E h ⟼ x ∈ Base C ⟼ a ⁡ 1 st ⁡ F ⁡ x
8 eqid ⊢ D Nat E = D Nat E
9 id ⊢ a ∈ g D Nat E h → a ∈ g D Nat E h
10 8 9 nat1st2nd ⊢ a ∈ g D Nat E h → a ∈ 1 st ⁡ g 2 nd ⁡ g D Nat E 1 st ⁡ h 2 nd ⁡ h
11 eqid ⊢ Base D = Base D
12 8 10 11 natfn ⊢ a ∈ g D Nat E h → a Fn Base D
13 dffn2 ⊢ a Fn Base D ↔ a : Base D ⟶ V
14 12 13 sylib ⊢ a ∈ g D Nat E h → a : Base D ⟶ V
15 eqid ⊢ Base C = Base C
16 relfunc ⊢ Rel ⁡ C Func D
17 1st2ndbr ⊢ Rel ⁡ C Func D ∧ F ∈ C Func D → 1 st ⁡ F C Func D 2 nd ⁡ F
18 16 4 17 sylancr ⊢ φ → 1 st ⁡ F C Func D 2 nd ⁡ F
19 15 11 18 funcf1 ⊢ φ → 1 st ⁡ F : Base C ⟶ Base D
20 fcompt ⊢ a : Base D ⟶ V ∧ 1 st ⁡ F : Base C ⟶ Base D → a ∘ 1 st ⁡ F = x ∈ Base C ⟼ a ⁡ 1 st ⁡ F ⁡ x
21 14 19 20 syl2anr ⊢ φ ∧ a ∈ g D Nat E h → a ∘ 1 st ⁡ F = x ∈ Base C ⟼ a ⁡ 1 st ⁡ F ⁡ x
22 21 mpteq2dva ⊢ φ → a ∈ g D Nat E h ⟼ a ∘ 1 st ⁡ F = a ∈ g D Nat E h ⟼ x ∈ Base C ⟼ a ⁡ 1 st ⁡ F ⁡ x
23 22 mpoeq3dv ⊢ φ → g ∈ D Func E , h ∈ D Func E ⟼ a ∈ g D Nat E h ⟼ a ∘ 1 st ⁡ F = g ∈ D Func E , h ∈ D Func E ⟼ a ∈ g D Nat E h ⟼ x ∈ Base C ⟼ a ⁡ 1 st ⁡ F ⁡ x
24 23 opeq2d ⊢ φ → g ∈ D Func E ⟼ g ∘ func F g ∈ D Func E , h ∈ D Func E ⟼ a ∈ g D Nat E h ⟼ a ∘ 1 st ⁡ F = g ∈ D Func E ⟼ g ∘ func F g ∈ D Func E , h ∈ D Func E ⟼ a ∈ g D Nat E h ⟼ x ∈ Base C ⟼ a ⁡ 1 st ⁡ F ⁡ x
25 7 24 eqtr4d ⊢ φ → K = g ∈ D Func E ⟼ g ∘ func F g ∈ D Func E , h ∈ D Func E ⟼ a ∈ g D Nat E h ⟼ a ∘ 1 st ⁡ F