tposcurf12

Description: The partially evaluated transposed curry functor at a morphism. (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 ‘ 𝐺 ) ‘ 𝑋 ) )
	tposcurf1.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	tposcurf11.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	tposcurf12.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	tposcurf12.1	⊢ 1 = ( Id ‘ 𝐶 )
	tposcurf12.y	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	tposcurf12.g	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑌 𝐽 𝑍 ) )
Assertion	tposcurf12	⊢ ( 𝜑 → ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑍 ) ‘ 𝐻 ) = ( 𝐻 ( ⟨ 𝑌 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑍 , 𝑋 ⟩ ) ( 1 ‘ 𝑋 ) ) )

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		tposcurf1.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
9		tposcurf11.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
10		tposcurf12.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
11		tposcurf12.1	⊢ 1 = ( Id ‘ 𝐶 )
12		tposcurf12.y	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
13		tposcurf12.g	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑌 𝐽 𝑍 ) )
14	1	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) = ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) )
15	14	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) = ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 ) )
16	7 15	eqtrd	⊢ ( 𝜑 → 𝐾 = ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 ) )
17	16	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ 𝐾 ) = ( 2^nd ‘ ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 ) ) )
18	17	oveqd	⊢ ( 𝜑 → ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑍 ) = ( 𝑌 ( 2^nd ‘ ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 ) ) 𝑍 ) )
19	18	fveq1d	⊢ ( 𝜑 → ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑍 ) ‘ 𝐻 ) = ( ( 𝑌 ( 2^nd ‘ ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 ) ) 𝑍 ) ‘ 𝐻 ) )
20		eqid	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) )
21		eqidd	⊢ ( 𝜑 → ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) = ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) )
22	3 4 5 21	cofuswapfcl	⊢ ( 𝜑 → ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
23		eqid	⊢ ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 ) = ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 )
24	20 2 3 4 22 8 6 23 9 10 11 12 13	curf12	⊢ ( 𝜑 → ( ( 𝑌 ( 2^nd ‘ ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ) ‘ 𝑋 ) ) 𝑍 ) ‘ 𝐻 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑍 ⟩ ) 𝐻 ) )
25		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
26	2 25 11 3 6	catidcl	⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
27	3 4 5 21 2 8 6 9 6 12 25 10 26 13	cofuswapf2	⊢ ( 𝜑 → ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐹 ∘_func ( 𝐶 swap_F 𝐷 ) ) ) ⟨ 𝑋 , 𝑍 ⟩ ) 𝐻 ) = ( 𝐻 ( ⟨ 𝑌 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑍 , 𝑋 ⟩ ) ( 1 ‘ 𝑋 ) ) )
28	19 24 27	3eqtrd	⊢ ( 𝜑 → ( ( 𝑌 ( 2^nd ‘ 𝐾 ) 𝑍 ) ‘ 𝐻 ) = ( 𝐻 ( ⟨ 𝑌 , 𝑋 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑍 , 𝑋 ⟩ ) ( 1 ‘ 𝑋 ) ) )

Metamath Proof Explorer

Theorem tposcurf12

Proof