Theorem postcofval

Description: Value of the post-composition functor as a curry of the functor composition bifunctor. (Contributed by Zhi Wang, 11-Oct-2025)

	Ref	Expression
Hypotheses	postcofval.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	postcofval.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
	postcofval.o	⊢ ⚬ = ( ⟨ 𝑅 , 𝑄 ⟩ curryF ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) )
	postcofval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
	postcofval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	postcofval.k	⊢ 𝐾 = ( ( 1st ‘ ⚬ ) ‘ 𝐹 )
Assertion	postcofval	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝐹 ∘func 𝑔 ) ) , ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ( 2nd ‘ 𝐹 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		postcofval.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		postcofval.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
3		postcofval.o	⊢ ⚬ = ( ⟨ 𝑅 , 𝑄 ⟩ curryF ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) )
4		postcofval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
5		postcofval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
6		postcofval.k	⊢ 𝐾 = ( ( 1st ‘ ⚬ ) ‘ 𝐹 )
7	2	fucbas	⊢ ( 𝐷 Func 𝐸 ) = ( Base ‘ 𝑅 )
8		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
9		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐹 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝐹 ) )
10	8 4 9	sylancr	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝐹 ) )
11	10	funcrcl2	⊢ ( 𝜑 → 𝐷 ∈ Cat )
12	10	funcrcl3	⊢ ( 𝜑 → 𝐸 ∈ Cat )
13	2 11 12	fuccat	⊢ ( 𝜑 → 𝑅 ∈ Cat )
14	1 5 11	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
15	2 1	oveq12i	⊢ ( 𝑅 ×c 𝑄 ) = ( ( 𝐷 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐷 ) )
16		eqid	⊢ ( 𝐶 FuncCat 𝐸 ) = ( 𝐶 FuncCat 𝐸 )
17	15 16 5 11 12	fucofunca	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∈ ( ( 𝑅 ×c 𝑄 ) Func ( 𝐶 FuncCat 𝐸 ) ) )
18	1	fucbas	⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 )
19		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
20	1 19	fuchom	⊢ ( 𝐶 Nat 𝐷 ) = ( Hom ‘ 𝑄 )
21		eqid	⊢ ( Id ‘ 𝑅 ) = ( Id ‘ 𝑅 )
22	3 7 13 14 17 18 4 6 20 21	curf1	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝐹 ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) 𝑔 ) ) , ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( ( ( Id ‘ 𝑅 ) ‘ 𝐹 ) ( ⟨ 𝐹 , 𝑔 ⟩ ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ⟨ 𝐹 , ℎ ⟩ ) 𝑎 ) ) ) ⟩ )
23		eqidd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) = ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) )
24		simpr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → 𝑔 ∈ ( 𝐶 Func 𝐷 ) )
25	4	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
26	23 24 25	fuco11b	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) → ( 𝐹 ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) 𝑔 ) = ( 𝐹 ∘func 𝑔 ) )
27	26	mpteq2dva	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝐹 ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝐹 ∘func 𝑔 ) ) )
28		eqidd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ) → ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) = ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) )
29		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ) → 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) )
30	4	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ) → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
31	28 21 2 29 30	fucolid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ) → ( ( ( Id ‘ 𝑅 ) ‘ 𝐹 ) ( ⟨ 𝐹 , 𝑔 ⟩ ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ⟨ 𝐹 , ℎ ⟩ ) 𝑎 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ( 2nd ‘ 𝐹 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) )
32	31	mpteq2dva	⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( ( ( Id ‘ 𝑅 ) ‘ 𝐹 ) ( ⟨ 𝐹 , 𝑔 ⟩ ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ⟨ 𝐹 , ℎ ⟩ ) 𝑎 ) ) = ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ( 2nd ‘ 𝐹 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) )
33	32	mpoeq3dv	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( ( ( Id ‘ 𝑅 ) ‘ 𝐹 ) ( ⟨ 𝐹 , 𝑔 ⟩ ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ⟨ 𝐹 , ℎ ⟩ ) 𝑎 ) ) ) = ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ( 2nd ‘ 𝐹 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
34	27 33	opeq12d	⊢ ( 𝜑 → ⟨ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝐹 ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) 𝑔 ) ) , ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( ( ( Id ‘ 𝑅 ) ‘ 𝐹 ) ( ⟨ 𝐹 , 𝑔 ⟩ ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ⟨ 𝐹 , ℎ ⟩ ) 𝑎 ) ) ) ⟩ = ⟨ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝐹 ∘func 𝑔 ) ) , ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ( 2nd ‘ 𝐹 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ )
35	22 34	eqtrd	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝐹 ∘func 𝑔 ) ) , ( 𝑔 ∈ ( 𝐶 Func 𝐷 ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ( 2nd ‘ 𝐹 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ )