Theorem curf2ndf 17489

Description: As shown in diagval 17482, the currying of the first projection is the diagonal functor. On the other hand, the currying of the second projection is 𝑥 ∈ 𝐶 ↦ (𝑦 ∈ 𝐷 ↦ 𝑦), which is a constant functor of the identity functor at 𝐷. (Contributed by Mario Carneiro, 15-Jan-2017.)

Hypotheses

Ref	Expression
curf2ndf.q	⊢ 𝑄 = (𝐷 FuncCat 𝐷)
curf2ndf.c	⊢ (𝜑 → 𝐶 ∈ Cat)
curf2ndf.d	⊢ (𝜑 → 𝐷 ∈ Cat)

Assertion

Ref	Expression
curf2ndf	⊢ (𝜑 → (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) = ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))

Proof of Theorem curf2ndf

Dummy variables 𝑢 𝑓 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ov 7138	. . . . . . . . . . 11 ⊢ (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦) = ((1st ‘(𝐶 2ndF 𝐷))‘⟨𝑥, 𝑦⟩)
2		eqid 2798	. . . . . . . . . . . . 13 ⊢ (𝐶 ×c 𝐷) = (𝐶 ×c 𝐷)
3		eqid 2798	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐶) = (Base‘𝐶)
4		eqid 2798	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐷) = (Base‘𝐷)
5	2, 3, 4	xpcbas 17420	. . . . . . . . . . . . 13 ⊢ ((Base‘𝐶) × (Base‘𝐷)) = (Base‘(𝐶 ×c 𝐷))
6		eqid 2798	. . . . . . . . . . . . 13 ⊢ (Hom ‘(𝐶 ×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷))
7		curf2ndf.c	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ Cat)
8	7	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝐶 ∈ Cat)
9		curf2ndf.d	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ Cat)
10	9	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝐷 ∈ Cat)
11		eqid 2798	. . . . . . . . . . . . 13 ⊢ (𝐶 2ndF 𝐷) = (𝐶 2ndF 𝐷)
12		opelxpi 5556	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
13	12	adantll 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
14	2, 5, 6, 8, 10, 11, 13	2ndf1 17437	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((1st ‘(𝐶 2ndF 𝐷))‘⟨𝑥, 𝑦⟩) = (2nd ‘⟨𝑥, 𝑦⟩))
15		vex 3444	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
16		vex 3444	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
17	15, 16	op2nd 7680	. . . . . . . . . . . 12 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
18	14, 17	eqtrdi 2849	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((1st ‘(𝐶 2ndF 𝐷))‘⟨𝑥, 𝑦⟩) = 𝑦)
19	1, 18	syl5eq 2845	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦) = 𝑦)
20	19	mpteq2dva 5125	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦)) = (𝑦 ∈ (Base‘𝐷) ↦ 𝑦))
21		mptresid 5885	. . . . . . . . 9 ⊢ ( I ↾ (Base‘𝐷)) = (𝑦 ∈ (Base‘𝐷) ↦ 𝑦)
22	20, 21	eqtr4di 2851	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦)) = ( I ↾ (Base‘𝐷)))
23		df-ov 7138	. . . . . . . . . . . . . . 15 ⊢ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓) = ((⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩)
24	8	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐶 ∈ Cat)
25	10	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐷 ∈ Cat)
26	13	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
27		simp-4r 783	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑥 ∈ (Base‘𝐶))
28		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑧 ∈ (Base‘𝐷))
29	27, 28	opelxpd 5557	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑥, 𝑧⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
30	2, 5, 6, 24, 25, 11, 26, 29	2ndf2 17438	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩) = (2nd ↾ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩)))
31	30	fveq1d 6647	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩) = ((2nd ↾ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩))‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩))
32	23, 31	syl5eq 2845	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓) = ((2nd ↾ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩))‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩))
33		eqid 2798	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
34		eqid 2798	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Id‘𝐶) = (Id‘𝐶)
35	7	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
36		simpr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
37	3, 33, 34, 35, 36	catidcl 16945	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
38	37	ad5ant12 755	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
39		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧))
40	38, 39	opelxpd 5557	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨((Id‘𝐶)‘𝑥), 𝑓⟩ ∈ ((𝑥(Hom ‘𝐶)𝑥) × (𝑦(Hom ‘𝐷)𝑧)))
41		eqid 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
42		simpllr 775	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑦 ∈ (Base‘𝐷))
43	2, 3, 4, 33, 41, 27, 42, 27, 28, 6	xpchom2 17428	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩) = ((𝑥(Hom ‘𝐶)𝑥) × (𝑦(Hom ‘𝐷)𝑧)))
44	40, 43	eleqtrrd 2893	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨((Id‘𝐶)‘𝑥), 𝑓⟩ ∈ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩))
45	44	fvresd 6665	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((2nd ↾ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩))‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩) = (2nd ‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩))
46		fvex 6658	. . . . . . . . . . . . . . . 16 ⊢ ((Id‘𝐶)‘𝑥) ∈ V
47		vex 3444	. . . . . . . . . . . . . . . 16 ⊢ 𝑓 ∈ V
48	46, 47	op2nd 7680	. . . . . . . . . . . . . . 15 ⊢ (2nd ‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩) = 𝑓
49	45, 48	eqtrdi 2849	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((2nd ↾ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩))‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩) = 𝑓)
50	32, 49	eqtrd 2833	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓) = 𝑓)
51	50	mpteq2dva 5125	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓)) = (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ 𝑓))
52		mptresid 5885	. . . . . . . . . . . 12 ⊢ ( I ↾ (𝑦(Hom ‘𝐷)𝑧)) = (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ 𝑓)
53	51, 52	eqtr4di 2851	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓)) = ( I ↾ (𝑦(Hom ‘𝐷)𝑧)))
54	53	3impa 1107	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓)) = ( I ↾ (𝑦(Hom ‘𝐷)𝑧)))
55	54	mpoeq3dva 7210	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓))) = (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ ( I ↾ (𝑦(Hom ‘𝐷)𝑧))))
56		fveq2 6645	. . . . . . . . . . . 12 ⊢ (𝑢 = ⟨𝑦, 𝑧⟩ → ((Hom ‘𝐷)‘𝑢) = ((Hom ‘𝐷)‘⟨𝑦, 𝑧⟩))
57		df-ov 7138	. . . . . . . . . . . 12 ⊢ (𝑦(Hom ‘𝐷)𝑧) = ((Hom ‘𝐷)‘⟨𝑦, 𝑧⟩)
58	56, 57	eqtr4di 2851	. . . . . . . . . . 11 ⊢ (𝑢 = ⟨𝑦, 𝑧⟩ → ((Hom ‘𝐷)‘𝑢) = (𝑦(Hom ‘𝐷)𝑧))
59	58	reseq2d 5818	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑦, 𝑧⟩ → ( I ↾ ((Hom ‘𝐷)‘𝑢)) = ( I ↾ (𝑦(Hom ‘𝐷)𝑧)))
60	59	mpompt 7245	. . . . . . . . 9 ⊢ (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ ( I ↾ ((Hom ‘𝐷)‘𝑢))) = (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ ( I ↾ (𝑦(Hom ‘𝐷)𝑧)))
61	55, 60	eqtr4di 2851	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓))) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ ( I ↾ ((Hom ‘𝐷)‘𝑢))))
62	22, 61	opeq12d 4773	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓)))⟩ = ⟨( I ↾ (Base‘𝐷)), (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ ( I ↾ ((Hom ‘𝐷)‘𝑢)))⟩)
63		eqid 2798	. . . . . . . 8 ⊢ (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) = (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))
64	9	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐷 ∈ Cat)
65	2, 7, 9, 11	2ndfcl 17440	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 2ndF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐷))
66	65	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝐶 2ndF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐷))
67		eqid 2798	. . . . . . . 8 ⊢ ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥) = ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥)
68	63, 3, 35, 64, 66, 4, 36, 67, 41, 34	curf1 17467	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥) = ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓)))⟩)
69		eqid 2798	. . . . . . . 8 ⊢ (idfunc‘𝐷) = (idfunc‘𝐷)
70	69, 4, 64, 41	idfuval 17138	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (idfunc‘𝐷) = ⟨( I ↾ (Base‘𝐷)), (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ ( I ↾ ((Hom ‘𝐷)‘𝑢)))⟩)
71	62, 68, 70	3eqtr4d 2843	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥) = (idfunc‘𝐷))
72		eqid 2798	. . . . . . 7 ⊢ (𝑄Δfunc𝐶) = (𝑄Δfunc𝐶)
73		curf2ndf.q	. . . . . . . . 9 ⊢ 𝑄 = (𝐷 FuncCat 𝐷)
74	73, 9, 9	fuccat 17232	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ Cat)
75	74	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑄 ∈ Cat)
76	73	fucbas 17222	. . . . . . 7 ⊢ (𝐷 Func 𝐷) = (Base‘𝑄)
77	69	idfucl 17143	. . . . . . . . 9 ⊢ (𝐷 ∈ Cat → (idfunc‘𝐷) ∈ (𝐷 Func 𝐷))
78	9, 77	syl 17	. . . . . . . 8 ⊢ (𝜑 → (idfunc‘𝐷) ∈ (𝐷 Func 𝐷))
79	78	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (idfunc‘𝐷) ∈ (𝐷 Func 𝐷))
80		eqid 2798	. . . . . . 7 ⊢ ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)) = ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))
81	72, 75, 35, 76, 79, 80, 3, 36	diag11 17485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑥) = (idfunc‘𝐷))
82	71, 81	eqtr4d 2836	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥) = ((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑥))
83	82	mpteq2dva 5125	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥)) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑥)))
84		relfunc 17124	. . . . . . 7 ⊢ Rel (𝐶 Func 𝑄)
85	63, 73, 7, 9, 65	curfcl 17474	. . . . . . 7 ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) ∈ (𝐶 Func 𝑄))
86		1st2ndbr 7723	. . . . . . 7 ⊢ ((Rel (𝐶 Func 𝑄) ∧ (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) ∈ (𝐶 Func 𝑄)) → (1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))(𝐶 Func 𝑄)(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))))
87	84, 85, 86	sylancr 590	. . . . . 6 ⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))(𝐶 Func 𝑄)(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))))
88	3, 76, 87	funcf1 17128	. . . . 5 ⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))):(Base‘𝐶)⟶(𝐷 Func 𝐷))
89	88	feqmptd 6708	. . . 4 ⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥)))
90	72, 74, 7, 76, 78, 80	diag1cl 17484	. . . . . . 7 ⊢ (𝜑 → ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)) ∈ (𝐶 Func 𝑄))
91		1st2ndbr 7723	. . . . . . 7 ⊢ ((Rel (𝐶 Func 𝑄) ∧ ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)) ∈ (𝐶 Func 𝑄)) → (1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))(𝐶 Func 𝑄)(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))))
92	84, 90, 91	sylancr 590	. . . . . 6 ⊢ (𝜑 → (1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))(𝐶 Func 𝑄)(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))))
93	3, 76, 92	funcf1 17128	. . . . 5 ⊢ (𝜑 → (1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))):(Base‘𝐶)⟶(𝐷 Func 𝐷))
94	93	feqmptd 6708	. . . 4 ⊢ (𝜑 → (1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑥)))
95	83, 89, 94	3eqtr4d 2843	. . 3 ⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))) = (1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))))
96	9	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐷 ∈ Cat)
97	69, 4, 96	idfu1st 17141	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (1st ‘(idfunc‘𝐷)) = ( I ↾ (Base‘𝐷)))
98	97	coeq2d 5697	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((Id‘𝐷) ∘ (1st ‘(idfunc‘𝐷))) = ((Id‘𝐷) ∘ ( I ↾ (Base‘𝐷))))
99		eqid 2798	. . . . . . . . . . 11 ⊢ (Id‘𝑄) = (Id‘𝑄)
100		eqid 2798	. . . . . . . . . . 11 ⊢ (Id‘𝐷) = (Id‘𝐷)
101	78	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (idfunc‘𝐷) ∈ (𝐷 Func 𝐷))
102	73, 99, 100, 101	fucid 17233	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((Id‘𝑄)‘(idfunc‘𝐷)) = ((Id‘𝐷) ∘ (1st ‘(idfunc‘𝐷))))
103	4, 100	cidfn 16942	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ Cat → (Id‘𝐷) Fn (Base‘𝐷))
104	96, 103	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (Id‘𝐷) Fn (Base‘𝐷))
105		dffn2 6489	. . . . . . . . . . . . 13 ⊢ ((Id‘𝐷) Fn (Base‘𝐷) ↔ (Id‘𝐷):(Base‘𝐷)⟶V)
106	104, 105	sylib 221	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (Id‘𝐷):(Base‘𝐷)⟶V)
107	106	feqmptd 6708	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (Id‘𝐷) = (𝑧 ∈ (Base‘𝐷) ↦ ((Id‘𝐷)‘𝑧)))
108		fcoi1 6526	. . . . . . . . . . . 12 ⊢ ((Id‘𝐷):(Base‘𝐷)⟶V → ((Id‘𝐷) ∘ ( I ↾ (Base‘𝐷))) = (Id‘𝐷))
109	106, 108	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((Id‘𝐷) ∘ ( I ↾ (Base‘𝐷))) = (Id‘𝐷))
110	7	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐶 ∈ Cat)
111	110	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝐶 ∈ Cat)
112	96	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝐷 ∈ Cat)
113		simplrl 776	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑥 ∈ (Base‘𝐶))
114		opelxpi 5556	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐷)) → ⟨𝑥, 𝑧⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
115	113, 114	sylan 583	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ⟨𝑥, 𝑧⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
116		simplrr 777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑦 ∈ (Base‘𝐶))
117		opelxpi 5556	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐷)) → ⟨𝑦, 𝑧⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
118	116, 117	sylan 583	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ⟨𝑦, 𝑧⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
119	2, 5, 6, 111, 112, 11, 115, 118	2ndf2 17438	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩) = (2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩)))
120	119	oveqd 7152	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓(⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)) = (𝑓(2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))((Id‘𝐷)‘𝑧)))
121		df-ov 7138	. . . . . . . . . . . . . . 15 ⊢ (𝑓(2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))((Id‘𝐷)‘𝑧)) = ((2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))‘⟨𝑓, ((Id‘𝐷)‘𝑧)⟩)
122		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
123		simpr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝑧 ∈ (Base‘𝐷))
124	4, 41, 100, 112, 123	catidcl 16945	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ((Id‘𝐷)‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧))
125	122, 124	opelxpd 5557	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ⟨𝑓, ((Id‘𝐷)‘𝑧)⟩ ∈ ((𝑥(Hom ‘𝐶)𝑦) × (𝑧(Hom ‘𝐷)𝑧)))
126	113	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝑥 ∈ (Base‘𝐶))
127	116	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝑦 ∈ (Base‘𝐶))
128	2, 3, 4, 33, 41, 126, 123, 127, 123, 6	xpchom2 17428	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩) = ((𝑥(Hom ‘𝐶)𝑦) × (𝑧(Hom ‘𝐷)𝑧)))
129	125, 128	eleqtrrd 2893	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ⟨𝑓, ((Id‘𝐷)‘𝑧)⟩ ∈ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))
130	129	fvresd 6665	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ((2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))‘⟨𝑓, ((Id‘𝐷)‘𝑧)⟩) = (2nd ‘⟨𝑓, ((Id‘𝐷)‘𝑧)⟩))
131	121, 130	syl5eq 2845	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓(2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))((Id‘𝐷)‘𝑧)) = (2nd ‘⟨𝑓, ((Id‘𝐷)‘𝑧)⟩))
132		fvex 6658	. . . . . . . . . . . . . . 15 ⊢ ((Id‘𝐷)‘𝑧) ∈ V
133	47, 132	op2nd 7680	. . . . . . . . . . . . . 14 ⊢ (2nd ‘⟨𝑓, ((Id‘𝐷)‘𝑧)⟩) = ((Id‘𝐷)‘𝑧)
134	131, 133	eqtrdi 2849	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓(2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))((Id‘𝐷)‘𝑧)) = ((Id‘𝐷)‘𝑧))
135	120, 134	eqtrd 2833	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓(⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)) = ((Id‘𝐷)‘𝑧))
136	135	mpteq2dva 5125	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑧 ∈ (Base‘𝐷) ↦ (𝑓(⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))) = (𝑧 ∈ (Base‘𝐷) ↦ ((Id‘𝐷)‘𝑧)))
137	107, 109, 136	3eqtr4rd 2844	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑧 ∈ (Base‘𝐷) ↦ (𝑓(⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))) = ((Id‘𝐷) ∘ ( I ↾ (Base‘𝐷))))
138	98, 102, 137	3eqtr4rd 2844	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑧 ∈ (Base‘𝐷) ↦ (𝑓(⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))) = ((Id‘𝑄)‘(idfunc‘𝐷)))
139	65	ad2antrr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝐶 2ndF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐷))
140		simpr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
141		eqid 2798	. . . . . . . . . 10 ⊢ ((𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)‘𝑓) = ((𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)‘𝑓)
142	63, 3, 110, 96, 139, 4, 33, 100, 113, 116, 140, 141	curf2 17471	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)‘𝑓) = (𝑧 ∈ (Base‘𝐷) ↦ (𝑓(⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))))
143	74	ad2antrr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑄 ∈ Cat)
144	72, 143, 110, 76, 101, 80, 3, 113, 33, 99, 116, 140	diag12 17486	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)‘𝑓) = ((Id‘𝑄)‘(idfunc‘𝐷)))
145	138, 142, 144	3eqtr4d 2843	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)‘𝑓) = ((𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)‘𝑓))
146	145	mpteq2dva 5125	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)‘𝑓)) = (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)‘𝑓)))
147		eqid 2798	. . . . . . . . . 10 ⊢ (𝐷 Nat 𝐷) = (𝐷 Nat 𝐷)
148	73, 147	fuchom 17223	. . . . . . . . 9 ⊢ (𝐷 Nat 𝐷) = (Hom ‘𝑄)
149	87	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))(𝐶 Func 𝑄)(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))))
150		simprl 770	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶))
151		simprr 772	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶))
152	3, 33, 148, 149, 150, 151	funcf2 17130	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥)(𝐷 Nat 𝐷)((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑦)))
153	152	feqmptd 6708	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦) = (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)‘𝑓)))
154	92	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))(𝐶 Func 𝑄)(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))))
155	3, 33, 148, 154, 150, 151	funcf2 17130	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑥)(𝐷 Nat 𝐷)((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑦)))
156	155	feqmptd 6708	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦) = (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)‘𝑓)))
157	146, 153, 156	3eqtr4d 2843	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦) = (𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦))
158	157	3impb 1112	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦) = (𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦))
159	158	mpoeq3dva 7210	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)))
160	3, 87	funcfn2 17131	. . . . 5 ⊢ (𝜑 → (2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))) Fn ((Base‘𝐶) × (Base‘𝐶)))
161		fnov 7261	. . . . 5 ⊢ ((2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)))
162	160, 161	sylib 221	. . . 4 ⊢ (𝜑 → (2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)))
163	3, 92	funcfn2 17131	. . . . 5 ⊢ (𝜑 → (2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))) Fn ((Base‘𝐶) × (Base‘𝐶)))
164		fnov 7261	. . . . 5 ⊢ ((2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)))
165	163, 164	sylib 221	. . . 4 ⊢ (𝜑 → (2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)))
166	159, 162, 165	3eqtr4d 2843	. . 3 ⊢ (𝜑 → (2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))) = (2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))))
167	95, 166	opeq12d 4773	. 2 ⊢ (𝜑 → ⟨(1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))), (2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))⟩ = ⟨(1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))), (2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))⟩)
168		1st2nd 7720	. . 3 ⊢ ((Rel (𝐶 Func 𝑄) ∧ (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) ∈ (𝐶 Func 𝑄)) → (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) = ⟨(1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))), (2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))⟩)
169	84, 85, 168	sylancr 590	. 2 ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) = ⟨(1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))), (2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))⟩)
170		1st2nd 7720	. . 3 ⊢ ((Rel (𝐶 Func 𝑄) ∧ ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)) ∈ (𝐶 Func 𝑄)) → ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)) = ⟨(1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))), (2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))⟩)
171	84, 90, 170	sylancr 590	. 2 ⊢ (𝜑 → ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)) = ⟨(1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))), (2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))⟩)
172	167, 169, 171	3eqtr4d 2843	1 ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) = ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Vcvv 3441  ⟨cop 4531   class class class wbr 5030   ↦ cmpt 5110   I cid 5424   × cxp 5517   ↾ cres 5521   ∘ ccom 5523  Rel wrel 5524   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135   ∈ cmpo 7137  1^st c1st 7669  2^nd c2nd 7670  Basecbs 16475  Hom chom 16568  Catccat 16927  Idccid 16928   Func cfunc 17116  id_funccidfu 17117   Nat cnat 17203   FuncCat cfuc 17204   ×_c cxpc 17410   2^nd_F c2ndf 17412   curry_F ccurf 17452  Δ_funccdiag 17454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-er 8272  df-map 8391  df-ixp 8445  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-fz 12886  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-hom 16581  df-cco 16582  df-cat 16931  df-cid 16932  df-func 17120  df-idfu 17121  df-nat 17205  df-fuc 17206  df-xpc 17414  df-1stf 17415  df-2ndf 17416  df-curf 17456  df-diag 17458

This theorem is referenced by: (None)