Metamath Proof Explorer

Theorem postcof2

Description: A component of the action of a post-composition functor is obtained by applying the morphism part of F to the component morphism. (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 |-
postcof2.g ⊢ φ → G ∈ C Func D
postcof2.h ⊢ φ → H ∈ C Func D
postcof2.a ⊢ φ → A ∈ G C Nat D H
postcof2.x ⊢ φ → X ∈ Base C
Assertion postcof2 ⊢ φ → G 2 nd ⁡ K H ⁡ A ⁡ X = 1 st ⁡ G ⁡ X 2 nd ⁡ F 1 st ⁡ H ⁡ X ⁡ A ⁡ X

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 postcof2.g ⊢ φ → G ∈ C Func D
8 postcof2.h ⊢ φ → H ∈ C Func D
9 postcof2.a ⊢ φ → A ∈ G C Nat D H
10 postcof2.x ⊢ φ → X ∈ Base C
11 1 2 3 4 5 6 postcof2nd ⊢ φ → 2 nd ⁡ K = 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
12 simprl ⊢ φ ∧ g = G ∧ h = H → g = G
13 simprr ⊢ φ ∧ g = G ∧ h = H → h = H
14 12 13 oveq12d ⊢ φ ∧ g = G ∧ h = H → g C Nat D h = G C Nat D H
15 12 fveq2d ⊢ φ ∧ g = G ∧ h = H → 1 st ⁡ g = 1 st ⁡ G
16 15 fveq1d ⊢ φ ∧ g = G ∧ h = H → 1 st ⁡ g ⁡ x = 1 st ⁡ G ⁡ x
17 13 fveq2d ⊢ φ ∧ g = G ∧ h = H → 1 st ⁡ h = 1 st ⁡ H
18 17 fveq1d ⊢ φ ∧ g = G ∧ h = H → 1 st ⁡ h ⁡ x = 1 st ⁡ H ⁡ x
19 16 18 oveq12d ⊢ φ ∧ g = G ∧ h = H → 1 st ⁡ g ⁡ x 2 nd ⁡ F 1 st ⁡ h ⁡ x = 1 st ⁡ G ⁡ x 2 nd ⁡ F 1 st ⁡ H ⁡ x
20 19 fveq1d ⊢ φ ∧ g = G ∧ h = H → 1 st ⁡ g ⁡ x 2 nd ⁡ F 1 st ⁡ h ⁡ x ⁡ a ⁡ x = 1 st ⁡ G ⁡ x 2 nd ⁡ F 1 st ⁡ H ⁡ x ⁡ a ⁡ x
21 20 mpteq2dv ⊢ φ ∧ g = G ∧ h = H → x ∈ Base C ⟼ 1 st ⁡ g ⁡ x 2 nd ⁡ F 1 st ⁡ h ⁡ x ⁡ a ⁡ x = x ∈ Base C ⟼ 1 st ⁡ G ⁡ x 2 nd ⁡ F 1 st ⁡ H ⁡ x ⁡ a ⁡ x
22 14 21 mpteq12dv ⊢ φ ∧ g = G ∧ h = H → a ∈ g C Nat D h ⟼ x ∈ Base C ⟼ 1 st ⁡ g ⁡ x 2 nd ⁡ F 1 st ⁡ h ⁡ x ⁡ a ⁡ x = a ∈ G C Nat D H ⟼ x ∈ Base C ⟼ 1 st ⁡ G ⁡ x 2 nd ⁡ F 1 st ⁡ H ⁡ x ⁡ a ⁡ x
23 ovex ⊢ G C Nat D H ∈ V
24 23 mptex ⊢ a ∈ G C Nat D H ⟼ x ∈ Base C ⟼ 1 st ⁡ G ⁡ x 2 nd ⁡ F 1 st ⁡ H ⁡ x ⁡ a ⁡ x ∈ V
25 24 a1i ⊢ φ → a ∈ G C Nat D H ⟼ x ∈ Base C ⟼ 1 st ⁡ G ⁡ x 2 nd ⁡ F 1 st ⁡ H ⁡ x ⁡ a ⁡ x ∈ V
26 11 22 7 8 25 ovmpod ⊢ φ → G 2 nd ⁡ K H = a ∈ G C Nat D H ⟼ x ∈ Base C ⟼ 1 st ⁡ G ⁡ x 2 nd ⁡ F 1 st ⁡ H ⁡ x ⁡ a ⁡ x
27 simpr ⊢ φ ∧ a = A → a = A
28 27 fveq1d ⊢ φ ∧ a = A → a ⁡ x = A ⁡ x
29 28 fveq2d ⊢ φ ∧ a = A → 1 st ⁡ G ⁡ x 2 nd ⁡ F 1 st ⁡ H ⁡ x ⁡ a ⁡ x = 1 st ⁡ G ⁡ x 2 nd ⁡ F 1 st ⁡ H ⁡ x ⁡ A ⁡ x
30 29 mpteq2dv ⊢ φ ∧ a = A → x ∈ Base C ⟼ 1 st ⁡ G ⁡ x 2 nd ⁡ F 1 st ⁡ H ⁡ x ⁡ a ⁡ x = x ∈ Base C ⟼ 1 st ⁡ G ⁡ x 2 nd ⁡ F 1 st ⁡ H ⁡ x ⁡ A ⁡ x
31 fvex ⊢ Base C ∈ V
32 31 mptex ⊢ x ∈ Base C ⟼ 1 st ⁡ G ⁡ x 2 nd ⁡ F 1 st ⁡ H ⁡ x ⁡ A ⁡ x ∈ V
33 32 a1i ⊢ φ → x ∈ Base C ⟼ 1 st ⁡ G ⁡ x 2 nd ⁡ F 1 st ⁡ H ⁡ x ⁡ A ⁡ x ∈ V
34 26 30 9 33 fvmptd ⊢ φ → G 2 nd ⁡ K H ⁡ A = x ∈ Base C ⟼ 1 st ⁡ G ⁡ x 2 nd ⁡ F 1 st ⁡ H ⁡ x ⁡ A ⁡ x
35 simpr ⊢ φ ∧ x = X → x = X
36 35 fveq2d ⊢ φ ∧ x = X → 1 st ⁡ G ⁡ x = 1 st ⁡ G ⁡ X
37 35 fveq2d ⊢ φ ∧ x = X → 1 st ⁡ H ⁡ x = 1 st ⁡ H ⁡ X
38 36 37 oveq12d ⊢ φ ∧ x = X → 1 st ⁡ G ⁡ x 2 nd ⁡ F 1 st ⁡ H ⁡ x = 1 st ⁡ G ⁡ X 2 nd ⁡ F 1 st ⁡ H ⁡ X
39 35 fveq2d ⊢ φ ∧ x = X → A ⁡ x = A ⁡ X
40 38 39 fveq12d ⊢ φ ∧ x = X → 1 st ⁡ G ⁡ x 2 nd ⁡ F 1 st ⁡ H ⁡ x ⁡ A ⁡ x = 1 st ⁡ G ⁡ X 2 nd ⁡ F 1 st ⁡ H ⁡ X ⁡ A ⁡ X
41 fvexd ⊢ φ → 1 st ⁡ G ⁡ X 2 nd ⁡ F 1 st ⁡ H ⁡ X ⁡ A ⁡ X ∈ V
42 34 40 10 41 fvmptd ⊢ φ → G 2 nd ⁡ K H ⁡ A ⁡ X = 1 st ⁡ G ⁡ X 2 nd ⁡ F 1 st ⁡ H ⁡ X ⁡ A ⁡ X