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	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	postcof1st.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
	postcof1st.o	⊢ ⚬ = ( ⟨ 𝑅 , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) )
	postcof1st.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
	postcof1st.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	postcof1st.k	⊢ 𝐾 = ( ( 1^st ‘ ⚬ ) ‘ 𝐹 )
	postcof2.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
	postcof2.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝐶 Func 𝐷 ) )
	postcof2.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐻 ) )
	postcof2.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
Assertion	postcof2	⊢ ( 𝜑 → ( ( ( 𝐺 ( 2^nd ‘ 𝐾 ) 𝐻 ) ‘ 𝐴 ) ‘ 𝑋 ) = ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		postcof1st.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		postcof1st.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
3		postcof1st.o	⊢ ⚬ = ( ⟨ 𝑅 , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) )
4		postcof1st.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
5		postcof1st.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
6		postcof1st.k	⊢ 𝐾 = ( ( 1^st ‘ ⚬ ) ‘ 𝐹 )
7		postcof2.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
8		postcof2.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝐶 Func 𝐷 ) )
9		postcof2.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐻 ) )
10		postcof2.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
11	1 2 3 4 5 6	postcof2nd	⊢ ( 𝜑 → ( 2^nd ‘ 𝐾 ) = ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
12		simprl	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) ) → 𝑔 = 𝐺 )
13		simprr	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) ) → ℎ = 𝐻 )
14	12 13	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) ) → ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) = ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐻 ) )
15	12	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) ) → ( 1^st ‘ 𝑔 ) = ( 1^st ‘ 𝐺 ) )
16	15	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) ) → ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) )
17	13	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) ) → ( 1^st ‘ ℎ ) = ( 1^st ‘ 𝐻 ) )
18	17	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) ) → ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) )
19	16 18	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) ) → ( ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) = ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) )
20	19	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) ) → ( ( ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) = ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) )
21	20	mpteq2dv	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) )
22	14 21	mpteq12dv	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) ) → ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑎 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐻 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) )
23		ovex	⊢ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐻 ) ∈ V
24	23	mptex	⊢ ( 𝑎 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐻 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ V
25	24	a1i	⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐻 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ V )
26	11 22 7 8 25	ovmpod	⊢ ( 𝜑 → ( 𝐺 ( 2^nd ‘ 𝐾 ) 𝐻 ) = ( 𝑎 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐻 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) )
27		simpr	⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → 𝑎 = 𝐴 )
28	27	fveq1d	⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → ( 𝑎 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
29	28	fveq2d	⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) = ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) )
30	29	mpteq2dv	⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) )
31		fvex	⊢ ( Base ‘ 𝐶 ) ∈ V
32	31	mptex	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) ∈ V
33	32	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) ∈ V )
34	26 30 9 33	fvmptd	⊢ ( 𝜑 → ( ( 𝐺 ( 2^nd ‘ 𝐾 ) 𝐻 ) ‘ 𝐴 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) )
35		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
36	35	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) )
37	35	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐻 ) ‘ 𝑋 ) )
38	36 37	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) = ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑋 ) ) )
39	35	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑋 ) )
40	38 39	fveq12d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) = ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) )
41		fvexd	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ∈ V )
42	34 40 10 41	fvmptd	⊢ ( 𝜑 → ( ( ( 𝐺 ( 2^nd ‘ 𝐾 ) 𝐻 ) ‘ 𝐴 ) ‘ 𝑋 ) = ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) )

Metamath Proof Explorer

Theorem postcof2

Proof