Theorem precofval3

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

	Ref	Expression
Hypotheses	precoffunc.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
	precoffunc.b	⊢ 𝐵 = ( 𝐷 Func 𝐸 )
	precoffunc.n	⊢ 𝑁 = ( 𝐷 Nat 𝐸 )
	precoffunc.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
	precoffunc.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	precoffunc.k	⊢ ( 𝜑 → 𝐾 = ( 𝑔 ∈ 𝐵 ↦ ( 𝑔 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) )
	precoffunc.l	⊢ ( 𝜑 → 𝐿 = ( 𝑔 ∈ 𝐵 , ℎ ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑔 𝑁 ℎ ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) )
	precofval3.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	precofval3.o	⊢ ( 𝜑 → ⚬ = ( ⟨ 𝑄 , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( 𝑄 swapF 𝑅 ) ) ) )
	precofval3.m	⊢ ( 𝜑 → 𝑀 = ( ( 1st ‘ ⚬ ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
Assertion	precofval3	⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ = 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		precoffunc.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
2		precoffunc.b	⊢ 𝐵 = ( 𝐷 Func 𝐸 )
3		precoffunc.n	⊢ 𝑁 = ( 𝐷 Nat 𝐸 )
4		precoffunc.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
5		precoffunc.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
6		precoffunc.k	⊢ ( 𝜑 → 𝐾 = ( 𝑔 ∈ 𝐵 ↦ ( 𝑔 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) )
7		precoffunc.l	⊢ ( 𝜑 → 𝐿 = ( 𝑔 ∈ 𝐵 , ℎ ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑔 𝑁 ℎ ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) )
8		precofval3.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
9		precofval3.o	⊢ ( 𝜑 → ⚬ = ( ⟨ 𝑄 , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( 𝑄 swapF 𝑅 ) ) ) )
10		precofval3.m	⊢ ( 𝜑 → 𝑀 = ( ( 1st ‘ ⚬ ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
11	2	mpteq1i	⊢ ( 𝑔 ∈ 𝐵 ↦ ( 𝑔 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) = ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) )
12	6 11	eqtrdi	⊢ ( 𝜑 → 𝐾 = ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) )
13	2	a1i	⊢ ( 𝜑 → 𝐵 = ( 𝐷 Func 𝐸 ) )
14	3	a1i	⊢ ( 𝜑 → 𝑁 = ( 𝐷 Nat 𝐸 ) )
15	14	oveqd	⊢ ( 𝜑 → ( 𝑔 𝑁 ℎ ) = ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) )
16		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
17		brrelex12	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
18	16 4 17	sylancr	⊢ ( 𝜑 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
19		op1stg	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
20	18 19	syl	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
21	20	eqcomd	⊢ ( 𝜑 → 𝐹 = ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
22	21	coeq2d	⊢ ( 𝜑 → ( 𝑎 ∘ 𝐹 ) = ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) )
23	15 22	mpteq12dv	⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝑔 𝑁 ℎ ) ↦ ( 𝑎 ∘ 𝐹 ) ) = ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ) )
24	13 13 23	mpoeq123dv	⊢ ( 𝜑 → ( 𝑔 ∈ 𝐵 , ℎ ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑔 𝑁 ℎ ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) = ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ) ) )
25	7 24	eqtrd	⊢ ( 𝜑 → 𝐿 = ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ) ) )
26	12 25	opeq12d	⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ = ⟨ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ) ) ⟩ )
27		df-br	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
28	4 27	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
29	8 1 9 28 5 10	precofval2	⊢ ( 𝜑 → 𝑀 = ⟨ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ) ) ⟩ )
30	26 29	eqtr4d	⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ = 𝑀 )