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 4 func1st2nd ⊢ φ → 1 st ⁡ F C Func D 2 nd ⁡ F
17 15 11 16 funcf1 ⊢ φ → 1 st ⁡ F : Base C ⟶ Base D
18 fcompt ⊢ a : Base D ⟶ V ∧ 1 st ⁡ F : Base C ⟶ Base D → a ∘ 1 st ⁡ F = x ∈ Base C ⟼ a ⁡ 1 st ⁡ F ⁡ x
19 14 17 18 syl2anr ⊢ φ ∧ a ∈ g D Nat E h → a ∘ 1 st ⁡ F = x ∈ Base C ⟼ a ⁡ 1 st ⁡ F ⁡ x
20 19 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
21 20 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
22 21 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
23 7 22 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