Metamath Proof Explorer

Theorem postcof2nd

Description: The morphism part of the explicit post-composition functor sends a pair of functors to the induced map on natural transformations. (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 ‘ ⚬ ) ‘ 𝐹 )
	Assertion	postcof2nd	⊢ ( 𝜑 → ( 2^nd ‘ 𝐾 ) = ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 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	1 2 3 4 5 6	postcofval	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝐹 ∘_func 𝑔 ) ) , ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ )
8		ovex	⊢ ( 𝐶 Func 𝐷 ) ∈ V
9	8	mptex	⊢ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝐹 ∘_func 𝑔 ) ) ∈ V
10	8 8	mpoex	⊢ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ V
11	9 10	op2ndd	⊢ ( 𝐾 = ⟨ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝐹 ∘_func 𝑔 ) ) , ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ → ( 2^nd ‘ 𝐾 ) = ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
12	7 11	syl	⊢ ( 𝜑 → ( 2^nd ‘ 𝐾 ) = ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )