Metamath Proof Explorer

Theorem tposcurf1cl

Description: The partially evaluated transposed curry functor is a functor. (Contributed by Zhi Wang, 9-Oct-2025)

		Ref	Expression
	Hypotheses	tposcurf1.g	⊢ ( 𝜑 → 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) )
		tposcurf1.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
		tposcurf1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
		tposcurf1.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
		tposcurf1.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐷 ×_c 𝐶 ) Func 𝐸 ) )
		tposcurf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
		tposcurf1.k	⊢ ( 𝜑 → 𝐾 = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) )
	Assertion	tposcurf1cl	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		tposcurf1.g	⊢ ( 𝜑 → 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) )
2		tposcurf1.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		tposcurf1.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		tposcurf1.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
5		tposcurf1.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐷 ×_c 𝐶 ) Func 𝐸 ) )
6		tposcurf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
7		tposcurf1.k	⊢ ( 𝜑 → 𝐾 = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) )
8	1	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) = ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) )
9	8	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) = ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 ) )
10	7 9	eqtrd	⊢ ( 𝜑 → 𝐾 = ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 ) )
11		eqid	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) )
12		eqidd	⊢ ( 𝜑 → ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) = ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) )
13	3 4 5 12	cofuswapfcl	⊢ ( 𝜑 → ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
14		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
15		eqid	⊢ ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 ) = ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 )
16	11 2 3 4 13 14 6 15	curf1cl	⊢ ( 𝜑 → ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 ) ∈ ( 𝐷 Func 𝐸 ) )
17	10 16	eqeltrd	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )