Theorem curf2val

Description: Value of a component of the curry functor natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		curf2.g	⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF 𝐹 )
2		curf2.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		curf2.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		curf2.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
5		curf2.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
6		curf2.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
7		curf2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
8		curf2.i	⊢ 𝐼 = ( Id ‘ 𝐷 )
9		curf2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
10		curf2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
11		curf2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
12		curf2.l	⊢ 𝐿 = ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 )
13		curf2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
14	1 2 3 4 5 6 7 8 9 10 11 12	curf2	⊢ ( 𝜑 → 𝐿 = ( 𝑧 ∈ 𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → 𝑧 = 𝑍 )
16	15	opeq2d	⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → ⟨ 𝑋 , 𝑧 ⟩ = ⟨ 𝑋 , 𝑍 ⟩ )
17	15	opeq2d	⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → ⟨ 𝑌 , 𝑧 ⟩ = ⟨ 𝑌 , 𝑍 ⟩ )
18	16 17	oveq12d	⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) = ( ⟨ 𝑋 , 𝑍 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑍 ⟩ ) )
19		eqidd	⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → 𝐾 = 𝐾 )
20	15	fveq2d	⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → ( 𝐼 ‘ 𝑧 ) = ( 𝐼 ‘ 𝑍 ) )
21	18 19 20	oveq123d	⊢ ( ( 𝜑 ∧ 𝑧 = 𝑍 ) → ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑍 ⟩ ) ( 𝐼 ‘ 𝑍 ) ) )
22		ovexd	⊢ ( 𝜑 → ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑍 ⟩ ) ( 𝐼 ‘ 𝑍 ) ) ∈ V )
23	14 21 13 22	fvmptd	⊢ ( 𝜑 → ( 𝐿 ‘ 𝑍 ) = ( 𝐾 ( ⟨ 𝑋 , 𝑍 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑍 ⟩ ) ( 𝐼 ‘ 𝑍 ) ) )