curfval

Description: Value of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	curfval.g	⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 )
	curfval.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	curfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	curfval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	curfval.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
	curfval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	curfval.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	curfval.1	⊢ 1 = ( Id ‘ 𝐶 )
	curfval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	curfval.i	⊢ 𝐼 = ( Id ‘ 𝐷 )
Assertion	curfval	⊢ ( 𝜑 → 𝐺 = ⟨ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		curfval.g	⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 )
2		curfval.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		curfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		curfval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
5		curfval.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
6		curfval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
7		curfval.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
8		curfval.1	⊢ 1 = ( Id ‘ 𝐶 )
9		curfval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
10		curfval.i	⊢ 𝐼 = ( Id ‘ 𝐷 )
11		df-curf	⊢ curry_F = ( 𝑒 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 1^st ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( 2^nd ‘ 𝑒 ) / 𝑑 ⦌ ⟨ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1^st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) ⟩ )
12	11	a1i	⊢ ( 𝜑 → curry_F = ( 𝑒 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 1^st ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( 2^nd ‘ 𝑒 ) / 𝑑 ⦌ ⟨ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1^st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) ⟩ ) )
13		fvexd	⊢ ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) → ( 1^st ‘ 𝑒 ) ∈ V )
14		simprl	⊢ ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) → 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ )
15	14	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) → ( 1^st ‘ 𝑒 ) = ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
16		op1stg	⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
17	3 4 16	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
18	17	adantr	⊢ ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) → ( 1^st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
19	15 18	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) → ( 1^st ‘ 𝑒 ) = 𝐶 )
20		fvexd	⊢ ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) → ( 2^nd ‘ 𝑒 ) ∈ V )
21	14	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) → 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ )
22	21	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) → ( 2^nd ‘ 𝑒 ) = ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
23		op2ndg	⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
24	3 4 23	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
25	24	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) → ( 2^nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
26	22 25	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) → ( 2^nd ‘ 𝑒 ) = 𝐷 )
27		simplr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑐 = 𝐶 )
28	27	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
29	28 2	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑐 ) = 𝐴 )
30		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
31	30	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑑 ) = ( Base ‘ 𝐷 ) )
32	31 6	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑑 ) = 𝐵 )
33		simprr	⊢ ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) → 𝑓 = 𝐹 )
34	33	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑓 = 𝐹 )
35	34	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 1^st ‘ 𝑓 ) = ( 1^st ‘ 𝐹 ) )
36	35	oveqd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑥 ( 1^st ‘ 𝑓 ) 𝑦 ) = ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) )
37	32 36	mpteq12dv	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1^st ‘ 𝑓 ) 𝑦 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) )
38	30	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Hom ‘ 𝑑 ) = ( Hom ‘ 𝐷 ) )
39	38 7	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Hom ‘ 𝑑 ) = 𝐽 )
40	39	oveqd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) = ( 𝑦 𝐽 𝑧 ) )
41	34	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 2^nd ‘ 𝑓 ) = ( 2^nd ‘ 𝐹 ) )
42	41	oveqd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) )
43	27	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Id ‘ 𝑐 ) = ( Id ‘ 𝐶 ) )
44	43 8	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Id ‘ 𝑐 ) = 1 )
45	44	fveq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) = ( 1 ‘ 𝑥 ) )
46		eqidd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑔 = 𝑔 )
47	42 45 46	oveq123d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) = ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) )
48	40 47	mpteq12dv	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) )
49	32 32 48	mpoeq123dv	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) )
50	37 49	opeq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ⟨ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1^st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ = ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ )
51	29 50	mpteq12dv	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1^st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) = ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) )
52	27	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) )
53	52 9	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Hom ‘ 𝑐 ) = 𝐻 )
54	53	oveqd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
55	41	oveqd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) = ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) )
56	30	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Id ‘ 𝑑 ) = ( Id ‘ 𝐷 ) )
57	56 10	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Id ‘ 𝑑 ) = 𝐼 )
58	57	fveq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) = ( 𝐼 ‘ 𝑧 ) )
59	55 46 58	oveq123d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) = ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) )
60	32 59	mpteq12dv	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) )
61	54 60	mpteq12dv	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) = ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) )
62	29 29 61	mpoeq123dv	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) )
63	51 62	opeq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ⟨ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1^st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) ⟩ = ⟨ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) ⟩ )
64	20 26 63	csbied2	⊢ ( ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) → ⦋ ( 2^nd ‘ 𝑒 ) / 𝑑 ⦌ ⟨ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1^st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) ⟩ = ⟨ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) ⟩ )
65	13 19 64	csbied2	⊢ ( ( 𝜑 ∧ ( 𝑒 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑓 = 𝐹 ) ) → ⦋ ( 1^st ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( 2^nd ‘ 𝑒 ) / 𝑑 ⦌ ⟨ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1^st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝑓 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) ⟩ = ⟨ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) ⟩ )
66		opex	⊢ ⟨ 𝐶 , 𝐷 ⟩ ∈ V
67	66	a1i	⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ V )
68	5	elexd	⊢ ( 𝜑 → 𝐹 ∈ V )
69		opex	⊢ ⟨ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) ⟩ ∈ V
70	69	a1i	⊢ ( 𝜑 → ⟨ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) ⟩ ∈ V )
71	12 65 67 68 70	ovmpod	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 ) = ⟨ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) ⟩ )
72	1 71	eqtrid	⊢ ( 𝜑 → 𝐺 = ⟨ ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑔 ) ) ) ⟩ ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑦 , 𝑧 ⟩ ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) ⟩ )

Metamath Proof Explorer

Theorem curfval

Proof