Theorem curf12

Description: The partially evaluated curry functor at a morphism. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	curfval.g	⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF 𝐹 )
	curfval.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	curfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	curfval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	curfval.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
	curfval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	curf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	curf1.k	⊢ 𝐾 = ( ( 1st ‘ 𝐺 ) ‘ 𝑋 )
	curf11.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	curf12.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	curf12.1	⊢ 1 = ( Id ‘ 𝐶 )
	curf12.y	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	curf12.g	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑌 𝐽 𝑍 ) )
Assertion	curf12	⊢ ( 𝜑 → ( ( 𝑌 ( 2nd ‘ 𝐾 ) 𝑍 ) ‘ 𝐻 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑍 ⟩ ) 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		curfval.g	⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curryF 𝐹 )
2		curfval.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		curfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		curfval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
5		curfval.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
6		curfval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
7		curf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
8		curf1.k	⊢ 𝐾 = ( ( 1st ‘ 𝐺 ) ‘ 𝑋 )
9		curf11.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
10		curf12.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
11		curf12.1	⊢ 1 = ( Id ‘ 𝐶 )
12		curf12.y	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
13		curf12.g	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑌 𝐽 𝑍 ) )
14	1 2 3 4 5 6 7 8 10 11	curf1	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ )
15	6	fvexi	⊢ 𝐵 ∈ V
16	15	mptex	⊢ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1st ‘ 𝐹 ) 𝑦 ) ) ∈ V
17	15 15	mpoex	⊢ ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ∈ V
18	16 17	op2ndd	⊢ ( 𝐾 = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑋 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ → ( 2nd ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) )
19	14 18	syl	⊢ ( 𝜑 → ( 2nd ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) )
20	12	adantr	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑌 ) → 𝑍 ∈ 𝐵 )
21		ovex	⊢ ( 𝑦 𝐽 𝑧 ) ∈ V
22	21	mptex	⊢ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ∈ V
23	22	a1i	⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) → ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ∈ V )
24	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) → 𝐻 ∈ ( 𝑌 𝐽 𝑍 ) )
25		simprl	⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) → 𝑦 = 𝑌 )
26		simprr	⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) → 𝑧 = 𝑍 )
27	25 26	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) → ( 𝑦 𝐽 𝑧 ) = ( 𝑌 𝐽 𝑍 ) )
28	24 27	eleqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) → 𝐻 ∈ ( 𝑦 𝐽 𝑧 ) )
29		ovexd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ∈ V )
30		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → 𝑦 = 𝑌 )
31	30	opeq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → ⟨ 𝑋 , 𝑦 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
32		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → 𝑧 = 𝑍 )
33	32	opeq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → ⟨ 𝑋 , 𝑧 ⟩ = ⟨ 𝑋 , 𝑍 ⟩ )
34	31 33	oveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) = ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑍 ⟩ ) )
35		eqidd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → ( 1 ‘ 𝑋 ) = ( 1 ‘ 𝑋 ) )
36		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → 𝑔 = 𝐻 )
37	34 35 36	oveq123d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) ∧ 𝑔 = 𝐻 ) → ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑍 ⟩ ) 𝐻 ) )
38	28 29 37	fvmptdv2	⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝑌 ∧ 𝑧 = 𝑍 ) ) → ( ( 𝑌 ( 2nd ‘ 𝐾 ) 𝑍 ) = ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) → ( ( 𝑌 ( 2nd ‘ 𝐾 ) 𝑍 ) ‘ 𝐻 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑍 ⟩ ) 𝐻 ) ) )
39	9 20 23 38	ovmpodv	⊢ ( 𝜑 → ( ( 2nd ‘ 𝐾 ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑧 ⟩ ) 𝑔 ) ) ) → ( ( 𝑌 ( 2nd ‘ 𝐾 ) 𝑍 ) ‘ 𝐻 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑍 ⟩ ) 𝐻 ) ) )
40	19 39	mpd	⊢ ( 𝜑 → ( ( 𝑌 ( 2nd ‘ 𝐾 ) 𝑍 ) ‘ 𝐻 ) = ( ( 1 ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑋 , 𝑍 ⟩ ) 𝐻 ) )