Metamath Proof Explorer

Theorem postcof1st

Description: The object part of the explicit post-composition functor sends each functor to its post-composition with F . (Contributed by Zhi Wang, 14-Sep-2026)

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

Proof

Step Hyp Ref Expression
1 postcof1st.q ⊢ Q = C FuncCat D
2 postcof1st.r ⊢ R = D FuncCat E
3 postcof1st.o Could not format .o. = ( <. R , Q >. curryF ( <. C , D >. o.F E ) ) : No typesetting found for |- .o. = ( <. R , Q >. curryF ( <. C , D >. o.F E ) ) with typecode |-
4 postcof1st.f ⊢ φ → F ∈ D Func E
5 postcof1st.c ⊢ φ → C ∈ Cat
6 postcof1st.k Could not format K = ( ( 1st ` .o. ) ` F ) : No typesetting found for |- K = ( ( 1st ` .o. ) ` F ) with typecode |-
7 1 2 3 4 5 6 postcofval ⊢ φ → K = g ∈ C Func D ⟼ F ∘ func g g ∈ C Func D , h ∈ C Func D ⟼ a ∈ g C Nat D h ⟼ x ∈ Base C ⟼ 1 st ⁡ g ⁡ x 2 nd ⁡ F 1 st ⁡ h ⁡ x ⁡ a ⁡ x
8 ovex ⊢ C Func D ∈ V
9 8 mptex ⊢ g ∈ C Func D ⟼ F ∘ func g ∈ V
10 8 8 mpoex ⊢ g ∈ C Func D , h ∈ C Func D ⟼ a ∈ g C Nat D h ⟼ x ∈ Base C ⟼ 1 st ⁡ g ⁡ x 2 nd ⁡ F 1 st ⁡ h ⁡ x ⁡ a ⁡ x ∈ V
11 9 10 op1std ⊢ K = g ∈ C Func D ⟼ F ∘ func g g ∈ C Func D , h ∈ C Func D ⟼ a ∈ g C Nat D h ⟼ x ∈ Base C ⟼ 1 st ⁡ g ⁡ x 2 nd ⁡ F 1 st ⁡ h ⁡ x ⁡ a ⁡ x → 1 st ⁡ K = g ∈ C Func D ⟼ F ∘ func g
12 7 11 syl ⊢ φ → 1 st ⁡ K = g ∈ C Func D ⟼ F ∘ func g