Theorem precofval

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

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

Proof

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