Theorem tposcurfcl

Description: The transposed curry functor of a functor F : D X. C --> E is a functor tposcurry ( F ) : C --> ( D --> E ) . (Contributed by Zhi Wang, 9-Oct-2025)

	Ref	Expression
Hypotheses	tposcurfcl.g	⊢ ( 𝜑 → 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) )
	tposcurfcl.q	⊢ 𝑄 = ( 𝐷 FuncCat 𝐸 )
	tposcurfcl.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	tposcurfcl.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	tposcurfcl.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐷 ×c 𝐶 ) Func 𝐸 ) )
Assertion	tposcurfcl	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		tposcurfcl.g	⊢ ( 𝜑 → 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) )
2		tposcurfcl.q	⊢ 𝑄 = ( 𝐷 FuncCat 𝐸 )
3		tposcurfcl.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		tposcurfcl.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
5		tposcurfcl.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐷 ×c 𝐶 ) Func 𝐸 ) )
6		eqid	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) )
7		eqidd	⊢ ( 𝜑 → ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) = ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) )
8	3 4 5 7	cofuswapfcl	⊢ ( 𝜑 → ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
9	6 2 3 4 8	curfcl	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) ∈ ( 𝐶 Func 𝑄 ) )
10	1 9	eqeltrd	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝑄 ) )