curf2ndf

Description: As shown in diagval , the currying of the first projection is the diagonal functor. On the other hand, the currying of the second projection is x e. C |-> ( y e. D |-> y ) , which is a constant functor of the identity functor at D . (Contributed by Mario Carneiro, 15-Jan-2017)

	Ref	Expression
Hypotheses	curf2ndf.q	⊢ 𝑄 = ( 𝐷 FuncCat 𝐷 )
	curf2ndf.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	curf2ndf.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
Assertion	curf2ndf	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) = ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		curf2ndf.q	⊢ 𝑄 = ( 𝐷 FuncCat 𝐷 )
2		curf2ndf.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		curf2ndf.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
4		df-ov	⊢ ( 𝑥 ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) 𝑦 ) = ( ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
5		eqid	⊢ ( 𝐶 ×_c 𝐷 ) = ( 𝐶 ×_c 𝐷 )
6		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
8	5 6 7	xpcbas	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ ( 𝐶 ×_c 𝐷 ) )
9		eqid	⊢ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×_c 𝐷 ) )
10	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝐶 ∈ Cat )
11	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝐷 ∈ Cat )
12		eqid	⊢ ( 𝐶 2^nd_F 𝐷 ) = ( 𝐶 2^nd_F 𝐷 )
13		opelxpi	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
14	13	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
15	5 8 9 10 11 12 14	2ndf1	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 2^nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
16		vex	⊢ 𝑥 ∈ V
17		vex	⊢ 𝑦 ∈ V
18	16 17	op2nd	⊢ ( 2^nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦
19	15 18	eqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦 )
20	4 19	syl5eq	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑥 ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) 𝑦 ) = 𝑦 )
21	20	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) 𝑦 ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ 𝑦 ) )
22		mptresid	⊢ ( I ↾ ( Base ‘ 𝐷 ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ 𝑦 )
23	21 22	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) 𝑦 ) ) = ( I ↾ ( Base ‘ 𝐷 ) ) )
24		df-ov	⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) = ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ )
25	10	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝐶 ∈ Cat )
26	11	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝐷 ∈ Cat )
27	14	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
28		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
29		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑧 ∈ ( Base ‘ 𝐷 ) )
30	28 29	opelxpd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
31	5 8 9 25 26 12 27 30	2ndf2	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) = ( 2^nd ↾ ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) ) )
32	31	fveq1d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ) = ( ( 2^nd ↾ ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ) )
33	24 32	syl5eq	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) = ( ( 2^nd ↾ ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ) )
34		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
35		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
36	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
37		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
38	6 34 35 36 37	catidcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
39	38	ad5ant12	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
40		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) )
41	39 40	opelxpd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ∈ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
42		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
43		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
44	5 6 7 34 42 28 43 28 29 9	xpchom2	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) = ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
45	41 44	eleqtrrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ∈ ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) )
46	45	fvresd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( 2^nd ↾ ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ) = ( 2^nd ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ) )
47		fvex	⊢ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ V
48		vex	⊢ 𝑓 ∈ V
49	47 48	op2nd	⊢ ( 2^nd ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ) = 𝑓
50	46 49	eqtrdi	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( 2^nd ↾ ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ) = 𝑓 )
51	33 50	eqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) = 𝑓 )
52	51	mpteq2dva	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) ) = ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ 𝑓 ) )
53		mptresid	⊢ ( I ↾ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) = ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ 𝑓 )
54	52 53	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) ) = ( I ↾ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
55	54	3impa	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) ) = ( I ↾ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
56	55	mpoeq3dva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( I ↾ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) )
57		fveq2	⊢ ( 𝑢 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) = ( ( Hom ‘ 𝐷 ) ‘ ⟨ 𝑦 , 𝑧 ⟩ ) )
58		df-ov	⊢ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) = ( ( Hom ‘ 𝐷 ) ‘ ⟨ 𝑦 , 𝑧 ⟩ )
59	57 58	eqtr4di	⊢ ( 𝑢 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) = ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) )
60	59	reseq2d	⊢ ( 𝑢 = ⟨ 𝑦 , 𝑧 ⟩ → ( I ↾ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ) = ( I ↾ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
61	60	mpompt	⊢ ( 𝑢 ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( I ↾ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
62	56 61	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ) ) )
63	23 62	opeq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) ) ) ⟩ = ⟨ ( I ↾ ( Base ‘ 𝐷 ) ) , ( 𝑢 ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ) ) ⟩ )
64		eqid	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) )
65	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
66	5 2 3 12	2ndfcl	⊢ ( 𝜑 → ( 𝐶 2^nd_F 𝐷 ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐷 ) )
67	66	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐶 2^nd_F 𝐷 ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐷 ) )
68		eqid	⊢ ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ 𝑥 ) = ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ 𝑥 )
69	64 6 36 65 67 7 37 68 42 35	curf1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ 𝑥 ) = ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) ) ) ⟩ )
70		eqid	⊢ ( id_func ‘ 𝐷 ) = ( id_func ‘ 𝐷 )
71	70 7 65 42	idfuval	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( id_func ‘ 𝐷 ) = ⟨ ( I ↾ ( Base ‘ 𝐷 ) ) , ( 𝑢 ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ) ) ⟩ )
72	63 69 71	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ 𝑥 ) = ( id_func ‘ 𝐷 ) )
73		eqid	⊢ ( 𝑄 Δ_func 𝐶 ) = ( 𝑄 Δ_func 𝐶 )
74	1 3 3	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
75	74	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑄 ∈ Cat )
76	1	fucbas	⊢ ( 𝐷 Func 𝐷 ) = ( Base ‘ 𝑄 )
77	70	idfucl	⊢ ( 𝐷 ∈ Cat → ( id_func ‘ 𝐷 ) ∈ ( 𝐷 Func 𝐷 ) )
78	3 77	syl	⊢ ( 𝜑 → ( id_func ‘ 𝐷 ) ∈ ( 𝐷 Func 𝐷 ) )
79	78	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( id_func ‘ 𝐷 ) ∈ ( 𝐷 Func 𝐷 ) )
80		eqid	⊢ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) = ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) )
81	73 75 36 76 79 80 6 37	diag11	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) ‘ 𝑥 ) = ( id_func ‘ 𝐷 ) )
82	72 81	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ 𝑥 ) = ( ( 1^st ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) ‘ 𝑥 ) )
83	82	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ 𝑥 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) ‘ 𝑥 ) ) )
84		relfunc	⊢ Rel ( 𝐶 Func 𝑄 )
85	64 1 2 3 66	curfcl	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ∈ ( 𝐶 Func 𝑄 ) )
86		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ∈ ( 𝐶 Func 𝑄 ) ) → ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) )
87	84 85 86	sylancr	⊢ ( 𝜑 → ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) )
88	6 76 87	funcf1	⊢ ( 𝜑 → ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) : ( Base ‘ 𝐶 ) ⟶ ( 𝐷 Func 𝐷 ) )
89	88	feqmptd	⊢ ( 𝜑 → ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ 𝑥 ) ) )
90	73 74 2 76 78 80	diag1cl	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ∈ ( 𝐶 Func 𝑄 ) )
91		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ∈ ( 𝐶 Func 𝑄 ) ) → ( 1^st ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) )
92	84 90 91	sylancr	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) )
93	6 76 92	funcf1	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) : ( Base ‘ 𝐶 ) ⟶ ( 𝐷 Func 𝐷 ) )
94	93	feqmptd	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) ‘ 𝑥 ) ) )
95	83 89 94	3eqtr4d	⊢ ( 𝜑 → ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) = ( 1^st ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) )
96	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐷 ∈ Cat )
97	70 7 96	idfu1st	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 1^st ‘ ( id_func ‘ 𝐷 ) ) = ( I ↾ ( Base ‘ 𝐷 ) ) )
98	97	coeq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ ( id_func ‘ 𝐷 ) ) ) = ( ( Id ‘ 𝐷 ) ∘ ( I ↾ ( Base ‘ 𝐷 ) ) ) )
99		eqid	⊢ ( Id ‘ 𝑄 ) = ( Id ‘ 𝑄 )
100		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
101	78	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( id_func ‘ 𝐷 ) ∈ ( 𝐷 Func 𝐷 ) )
102	1 99 100 101	fucid	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( Id ‘ 𝑄 ) ‘ ( id_func ‘ 𝐷 ) ) = ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ ( id_func ‘ 𝐷 ) ) ) )
103	7 100	cidfn	⊢ ( 𝐷 ∈ Cat → ( Id ‘ 𝐷 ) Fn ( Base ‘ 𝐷 ) )
104	96 103	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( Id ‘ 𝐷 ) Fn ( Base ‘ 𝐷 ) )
105		dffn2	⊢ ( ( Id ‘ 𝐷 ) Fn ( Base ‘ 𝐷 ) ↔ ( Id ‘ 𝐷 ) : ( Base ‘ 𝐷 ) ⟶ V )
106	104 105	sylib	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( Id ‘ 𝐷 ) : ( Base ‘ 𝐷 ) ⟶ V )
107	106	feqmptd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( Id ‘ 𝐷 ) = ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) )
108		fcoi1	⊢ ( ( Id ‘ 𝐷 ) : ( Base ‘ 𝐷 ) ⟶ V → ( ( Id ‘ 𝐷 ) ∘ ( I ↾ ( Base ‘ 𝐷 ) ) ) = ( Id ‘ 𝐷 ) )
109	106 108	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( Id ‘ 𝐷 ) ∘ ( I ↾ ( Base ‘ 𝐷 ) ) ) = ( Id ‘ 𝐷 ) )
110	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐶 ∈ Cat )
111	110	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝐶 ∈ Cat )
112	96	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝐷 ∈ Cat )
113		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
114		opelxpi	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
115	113 114	sylan	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
116		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
117		opelxpi	⊢ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
118	116 117	sylan	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
119	5 8 9 111 112 12 115 118	2ndf2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) = ( 2^nd ↾ ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ) )
120	119	oveqd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) = ( 𝑓 ( 2^nd ↾ ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) )
121		df-ov	⊢ ( 𝑓 ( 2^nd ↾ ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) = ( ( 2^nd ↾ ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ⟩ )
122		simplr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
123		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝑧 ∈ ( Base ‘ 𝐷 ) )
124	7 42 100 112 123	catidcl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑧 ) )
125	122 124	opelxpd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ⟩ ∈ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( 𝑧 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
126	113	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
127	116	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
128	5 6 7 34 42 126 123 127 123 9	xpchom2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) = ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( 𝑧 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
129	125 128	eleqtrrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ⟩ ∈ ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) )
130	129	fvresd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ( 2^nd ↾ ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ⟩ ) = ( 2^nd ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ⟩ ) )
131	121 130	syl5eq	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑓 ( 2^nd ↾ ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) = ( 2^nd ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ⟩ ) )
132		fvex	⊢ ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ∈ V
133	48 132	op2nd	⊢ ( 2^nd ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ⟩ ) = ( ( Id ‘ 𝐷 ) ‘ 𝑧 )
134	131 133	eqtrdi	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑓 ( 2^nd ↾ ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) = ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) )
135	120 134	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) = ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) )
136	135	mpteq2dva	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑓 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) )
137	107 109 136	3eqtr4rd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑓 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) = ( ( Id ‘ 𝐷 ) ∘ ( I ↾ ( Base ‘ 𝐷 ) ) ) )
138	98 102 137	3eqtr4rd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑓 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) = ( ( Id ‘ 𝑄 ) ‘ ( id_func ‘ 𝐷 ) ) )
139	66	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝐶 2^nd_F 𝐷 ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐷 ) )
140		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
141		eqid	⊢ ( ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) = ( ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 )
142	64 6 110 96 139 7 34 100 113 116 140 141	curf2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) = ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑓 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) )
143	74	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑄 ∈ Cat )
144	73 143 110 76 101 80 6 113 34 99 116 140	diag12	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) = ( ( Id ‘ 𝑄 ) ‘ ( id_func ‘ 𝐷 ) ) )
145	138 142 144	3eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) = ( ( 𝑥 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) )
146	145	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( 𝑥 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) ) )
147		eqid	⊢ ( 𝐷 Nat 𝐷 ) = ( 𝐷 Nat 𝐷 )
148	1 147	fuchom	⊢ ( 𝐷 Nat 𝐷 ) = ( Hom ‘ 𝑄 )
149	87	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) )
150		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
151		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
152	6 34 148 149 150 151	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐷 ) ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ 𝑦 ) ) )
153	152	feqmptd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) 𝑦 ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) ) )
154	92	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) )
155	6 34 148 154 150 151	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐷 ) ( ( 1^st ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) ‘ 𝑦 ) ) )
156	155	feqmptd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) 𝑦 ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( 𝑥 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) ) )
157	146 153 156	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) 𝑦 ) = ( 𝑥 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) 𝑦 ) )
158	157	3impb	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) 𝑦 ) = ( 𝑥 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) 𝑦 ) )
159	158	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) 𝑦 ) ) )
160	6 87	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
161		fnov	⊢ ( ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) 𝑦 ) ) )
162	160 161	sylib	⊢ ( 𝜑 → ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) 𝑦 ) ) )
163	6 92	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
164		fnov	⊢ ( ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) 𝑦 ) ) )
165	163 164	sylib	⊢ ( 𝜑 → ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) 𝑦 ) ) )
166	159 162 165	3eqtr4d	⊢ ( 𝜑 → ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) = ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) )
167	95 166	opeq12d	⊢ ( 𝜑 → ⟨ ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) , ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) ⟩ = ⟨ ( 1^st ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) , ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) ⟩ )
168		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ∈ ( 𝐶 Func 𝑄 ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) = ⟨ ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) , ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) ⟩ )
169	84 85 168	sylancr	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) = ⟨ ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) , ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) ) ⟩ )
170		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ∈ ( 𝐶 Func 𝑄 ) ) → ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) = ⟨ ( 1^st ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) , ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) ⟩ )
171	84 90 170	sylancr	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) = ⟨ ( 1^st ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) , ( 2^nd ‘ ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) ) ⟩ )
172	167 169 171	3eqtr4d	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ curry_F ( 𝐶 2^nd_F 𝐷 ) ) = ( ( 1^st ‘ ( 𝑄 Δ_func 𝐶 ) ) ‘ ( id_func ‘ 𝐷 ) ) )

Metamath Proof Explorer

Theorem curf2ndf

Proof