Theorem curf2

Description: Value of the curry functor at a morphism. (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 ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 )
Assertion	curf2	⊢ ( 𝜑 → 𝐿 = ( 𝑧 ∈ 𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 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		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
14		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
15	1 2 3 4 5 6 13 14 7 8	curfval	⊢ ( 𝜑 → 𝐺 = ⟨ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) ⟩ )
16	2	fvexi	⊢ 𝐴 ∈ V
17	16	mptex	⊢ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) ∈ V
18	16 16	mpoex	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) ∈ V
19	17 18	op2ndd	⊢ ( 𝐺 = ⟨ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) ⟩ → ( 2nd ‘ 𝐺 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) )
20	15 19	syl	⊢ ( 𝜑 → ( 2nd ‘ 𝐺 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) )
21	10	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑌 ∈ 𝐴 )
22		ovex	⊢ ( 𝑥 𝐻 𝑦 ) ∈ V
23	22	mptex	⊢ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ∈ V
24	23	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ∈ V )
25	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
26		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑥 = 𝑋 )
27		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 )
28	26 27	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
29	25 28	eleqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝐾 ∈ ( 𝑥 𝐻 𝑦 ) )
30	6	fvexi	⊢ 𝐵 ∈ V
31	30	mptex	⊢ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ∈ V
32	31	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ∈ V )
33		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → 𝑥 = 𝑋 )
34	33	opeq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑋 , 𝑧 ⟩ )
35		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → 𝑦 = 𝑌 )
36	35	opeq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑌 , 𝑧 ⟩ )
37	34 36	oveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) = ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) )
38		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → 𝑔 = 𝐾 )
39		eqidd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → ( 𝐼 ‘ 𝑧 ) = ( 𝐼 ‘ 𝑧 ) )
40	37 38 39	oveq123d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) = ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) )
41	40	mpteq2dv	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) ∧ 𝑔 = 𝐾 ) → ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) )
42	29 32 41	fvmptdv2	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) = ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) → ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) = ( 𝑧 ∈ 𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) )
43	9 21 24 42	ovmpodv	⊢ ( 𝜑 → ( ( 2nd ‘ 𝐺 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) → ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) = ( 𝑧 ∈ 𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) )
44	20 43	mpd	⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ 𝐺 ) 𝑌 ) ‘ 𝐾 ) = ( 𝑧 ∈ 𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) )
45	12 44	eqtrid	⊢ ( 𝜑 → 𝐿 = ( 𝑧 ∈ 𝐵 ↦ ( 𝐾 ( ⟨ 𝑋 , 𝑧 ⟩ ( 2nd ‘ 𝐹 ) ⟨ 𝑌 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) )