Theorem precofval2

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	precofval2	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘func 𝐹 ) ) , ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ∘ ( 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 2 3 4 5 6	precofval	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘func 𝐹 ) ) , ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑎 ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) ) ⟩ )
8		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
9		id	⊢ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) → 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) )
10	8 9	nat1st2nd	⊢ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) → 𝑎 ∈ ( ⟨ ( 1st ‘ 𝑔 ) , ( 2nd ‘ 𝑔 ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1st ‘ ℎ ) , ( 2nd ‘ ℎ ) ⟩ ) )
11		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
12	8 10 11	natfn	⊢ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) → 𝑎 Fn ( Base ‘ 𝐷 ) )
13		dffn2	⊢ ( 𝑎 Fn ( Base ‘ 𝐷 ) ↔ 𝑎 : ( Base ‘ 𝐷 ) ⟶ V )
14	12 13	sylib	⊢ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) → 𝑎 : ( Base ‘ 𝐷 ) ⟶ V )
15		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
16	4	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
17	15 11 16	funcf1	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
18		fcompt	⊢ ( ( 𝑎 : ( Base ‘ 𝐷 ) ⟶ V ∧ ( 1st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) ) → ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑎 ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
19	14 17 18	syl2anr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) → ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑎 ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
20	19	mpteq2dva	⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) = ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑎 ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) )
21	20	mpoeq3dv	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) = ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑎 ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) ) )
22	21	opeq2d	⊢ ( 𝜑 → ⟨ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘func 𝐹 ) ) , ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ = ⟨ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘func 𝐹 ) ) , ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑎 ‘ ( ( 1st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) ) ⟩ )
23	7 22	eqtr4d	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘func 𝐹 ) ) , ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ )