Theorem tposcurf2

Description: Value of the transposed curry functor at a morphism. (Contributed by Zhi Wang, 10-Oct-2025)

	Ref	Expression
Hypotheses	tposcurf2.g	⊢ ( 𝜑 → 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) )
	tposcurf2.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	tposcurf2.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	tposcurf2.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	tposcurf2.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐷 ×c 𝐶 ) Func 𝐸 ) )
	tposcurf2.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	tposcurf2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	tposcurf2.i	⊢ 𝐼 = ( Id ‘ 𝐷 )
	tposcurf2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	tposcurf2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
	tposcurf2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
	tposcurf2.l	⊢ ( 𝜑 → 𝐿 = ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) )
Assertion	tposcurf2	⊢ ( 𝜑 → 𝐿 = ( 𝑧 ∈ 𝐵 ↦ ( ( 𝐼 ‘ 𝑧 ) ( ⟨ 𝑧 , 𝑋 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑌 ⟩ ) 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tposcurf2.g	⊢ ( 𝜑 → 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) )
2		tposcurf2.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		tposcurf2.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		tposcurf2.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
5		tposcurf2.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐷 ×c 𝐶 ) Func 𝐸 ) )
6		tposcurf2.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
7		tposcurf2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
8		tposcurf2.i	⊢ 𝐼 = ( Id ‘ 𝐷 )
9		tposcurf2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
10		tposcurf2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
11		tposcurf2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
12		tposcurf2.l	⊢ ( 𝜑 → 𝐿 = ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) )
13	1	fveq2d	⊢ ( 𝜑 → ( 2nd ‘ 𝐺 ) = ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) ) )
14	13	oveqd	⊢ ( 𝜑 → ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) = ( 𝑋 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) ) 𝑌 ) )
15	14	fveq1d	⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) = ( ( 𝑋 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) ) 𝑌 ) ‘ 𝐾 ) )
16	12 15	eqtrd	⊢ ( 𝜑 → 𝐿 = ( ( 𝑋 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) ) 𝑌 ) ‘ 𝐾 ) )
17		eqid	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) )
18		eqidd	⊢ ( 𝜑 → ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) = ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) )
19	3 4 5 18	cofuswapfcl	⊢ ( 𝜑 → ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
20		eqid	⊢ ( ( 𝑋 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) ) 𝑌 ) ‘ 𝐾 ) = ( ( 𝑋 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) ) 𝑌 ) ‘ 𝐾 )
21	17 2 3 4 19 6 7 8 9 10 11 20	curf2	⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) ) 𝑌 ) ‘ 𝐾 ) = ( 𝑧 ∈ 𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd ‘ ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) )
22	3	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝐶 ∈ Cat )
23	4	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝐷 ∈ Cat )
24	5	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝐹 ∈ ( ( 𝐷 ×c 𝐶 ) Func 𝐸 ) )
25		eqidd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) = ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) )
26	9	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑋 ∈ 𝐴 )
27		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
28	10	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑌 ∈ 𝐴 )
29		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
30	11	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
31	6 29 8 23 27	catidcl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑧 ) ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑧 ) )
32	22 23 24 25 2 6 26 27 28 27 7 29 30 31	cofuswapf2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd ‘ ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) = ( ( 𝐼 ‘ 𝑧 ) ( ⟨ 𝑧 , 𝑋 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑌 ⟩ ) 𝐾 ) )
33	32	mpteq2dva	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd ‘ ( 𝐹 ∘func ( 𝐶 swapF 𝐷 ) ) ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝐵 ↦ ( ( 𝐼 ‘ 𝑧 ) ( ⟨ 𝑧 , 𝑋 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑌 ⟩ ) 𝐾 ) ) )
34	16 21 33	3eqtrd	⊢ ( 𝜑 → 𝐿 = ( 𝑧 ∈ 𝐵 ↦ ( ( 𝐼 ‘ 𝑧 ) ( ⟨ 𝑧 , 𝑋 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑌 ⟩ ) 𝐾 ) ) )