Theorem curf2ndf 18426

Description: As shown in diagval 18419, 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 7423	. . . . . . . . . . 11 ⊢ (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦) = ((1st ‘(𝐶 2ndF 𝐷))‘⟨𝑥, 𝑦⟩)
2		eqid 2760	. . . . . . . . . . . . 13 ⊢ (𝐶 ×c 𝐷) = (𝐶 ×c 𝐷)
3		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐶) = (Base‘𝐶)
4		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐷) = (Base‘𝐷)
5	2, 3, 4	xpcbas 18357	. . . . . . . . . . . . 13 ⊢ ((Base‘𝐶) × (Base‘𝐷)) = (Base‘(𝐶 ×c 𝐷))
6		eqid 2760	. . . . . . . . . . . . 13 ⊢ (Hom ‘(𝐶 ×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷))
7		curf2ndf.c	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ Cat)
8	7	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝐶 ∈ Cat)
9		curf2ndf.d	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ Cat)
10	9	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝐷 ∈ Cat)
11		eqid 2760	. . . . . . . . . . . . 13 ⊢ (𝐶 2ndF 𝐷) = (𝐶 2ndF 𝐷)
12		opelxpi 5687	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
13	12	adantll 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
14	2, 5, 6, 8, 10, 11, 13	2ndf1 18374	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((1st ‘(𝐶 2ndF 𝐷))‘⟨𝑥, 𝑦⟩) = (2nd ‘⟨𝑥, 𝑦⟩))
15		vex 3454	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
16		vex 3454	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
17	15, 16	op2nd 8010	. . . . . . . . . . . 12 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
18	14, 17	eqtrdi 2811	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((1st ‘(𝐶 2ndF 𝐷))‘⟨𝑥, 𝑦⟩) = 𝑦)
19	1, 18	eqtrid 2807	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦) = 𝑦)
20	19	mpteq2dva 5197	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦)) = (𝑦 ∈ (Base‘𝐷) ↦ 𝑦))
21		mptresid 6042	. . . . . . . . 9 ⊢ ( I ↾ (Base‘𝐷)) = (𝑦 ∈ (Base‘𝐷) ↦ 𝑦)
22	20, 21	eqtr4di 2813	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦)) = ( I ↾ (Base‘𝐷)))
23		df-ov 7423	. . . . . . . . . . . . . . 15 ⊢ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓) = ((⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩)
24	8	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐶 ∈ Cat)
25	10	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐷 ∈ Cat)
26	13	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
27		simp-4r 796	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑥 ∈ (Base‘𝐶))
28		simplr 781	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑧 ∈ (Base‘𝐷))
29	27, 28	opelxpd 5689	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑥, 𝑧⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
30	2, 5, 6, 24, 25, 11, 26, 29	2ndf2 18375	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩) = (2nd ↾ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩)))
31	30	fveq1d 6887	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩) = ((2nd ↾ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩))‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩))
32	23, 31	eqtrid 2807	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓) = ((2nd ↾ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩))‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩))
33		eqid 2760	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
34		eqid 2760	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Id‘𝐶) = (Id‘𝐶)
35	7	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
36		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
37	3, 33, 34, 35, 36	catidcl 17861	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
38	37	ad3antrrr 743	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
39		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧))
40	38, 39	opelxpd 5689	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨((Id‘𝐶)‘𝑥), 𝑓⟩ ∈ ((𝑥(Hom ‘𝐶)𝑥) × (𝑦(Hom ‘𝐷)𝑧)))
41		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
42		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑦 ∈ (Base‘𝐷))
43	2, 3, 4, 33, 41, 27, 42, 27, 28, 6	xpchom2 18365	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩) = ((𝑥(Hom ‘𝐶)𝑥) × (𝑦(Hom ‘𝐷)𝑧)))
44	40, 43	eleqtrrd 2863	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨((Id‘𝐶)‘𝑥), 𝑓⟩ ∈ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩))
45	44	fvresd 6905	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((2nd ↾ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩))‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩) = (2nd ‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩))
46		fvex 6898	. . . . . . . . . . . . . . . 16 ⊢ ((Id‘𝐶)‘𝑥) ∈ V
47		vex 3454	. . . . . . . . . . . . . . . 16 ⊢ 𝑓 ∈ V
48	46, 47	op2nd 8010	. . . . . . . . . . . . . . 15 ⊢ (2nd ‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩) = 𝑓
49	45, 48	eqtrdi 2811	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((2nd ↾ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩))‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩) = 𝑓)
50	32, 49	eqtrd 2795	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓) = 𝑓)
51	50	mpteq2dva 5197	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓)) = (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ 𝑓))
52		mptresid 6042	. . . . . . . . . . . 12 ⊢ ( I ↾ (𝑦(Hom ‘𝐷)𝑧)) = (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ 𝑓)
53	51, 52	eqtr4di 2813	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓)) = ( I ↾ (𝑦(Hom ‘𝐷)𝑧)))
54	53	3impa 1127	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓)) = ( I ↾ (𝑦(Hom ‘𝐷)𝑧)))
55	54	mpoeq3dva 7497	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓))) = (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ ( I ↾ (𝑦(Hom ‘𝐷)𝑧))))
56		fveq2 6885	. . . . . . . . . . . 12 ⊢ (𝑢 = ⟨𝑦, 𝑧⟩ → ((Hom ‘𝐷)‘𝑢) = ((Hom ‘𝐷)‘⟨𝑦, 𝑧⟩))
57		df-ov 7423	. . . . . . . . . . . 12 ⊢ (𝑦(Hom ‘𝐷)𝑧) = ((Hom ‘𝐷)‘⟨𝑦, 𝑧⟩)
58	56, 57	eqtr4di 2813	. . . . . . . . . . 11 ⊢ (𝑢 = ⟨𝑦, 𝑧⟩ → ((Hom ‘𝐷)‘𝑢) = (𝑦(Hom ‘𝐷)𝑧))
59	58	reseq2d 5969	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑦, 𝑧⟩ → ( I ↾ ((Hom ‘𝐷)‘𝑢)) = ( I ↾ (𝑦(Hom ‘𝐷)𝑧)))
60	59	mpompt 7534	. . . . . . . . 9 ⊢ (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ ( I ↾ ((Hom ‘𝐷)‘𝑢))) = (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ ( I ↾ (𝑦(Hom ‘𝐷)𝑧)))
61	55, 60	eqtr4di 2813	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓))) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ ( I ↾ ((Hom ‘𝐷)‘𝑢))))
62	22, 61	opeq12d 4847	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓)))⟩ = ⟨( I ↾ (Base‘𝐷)), (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ ( I ↾ ((Hom ‘𝐷)‘𝑢)))⟩)
63		eqid 2760	. . . . . . . 8 ⊢ (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) = (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))
64	9	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐷 ∈ Cat)
65	2, 7, 9, 11	2ndfcl 18377	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 2ndF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐷))
66	65	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝐶 2ndF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐷))
67		eqid 2760	. . . . . . . 8 ⊢ ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥) = ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥)
68	63, 3, 35, 64, 66, 4, 36, 67, 41, 34	curf1 18404	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥) = ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓)))⟩)
69		eqid 2760	. . . . . . . 8 ⊢ (idfunc‘𝐷) = (idfunc‘𝐷)
70	69, 4, 64, 41	idfuval 18056	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (idfunc‘𝐷) = ⟨( I ↾ (Base‘𝐷)), (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ ( I ↾ ((Hom ‘𝐷)‘𝑢)))⟩)
71	62, 68, 70	3eqtr4d 2805	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥) = (idfunc‘𝐷))
72		eqid 2760	. . . . . . 7 ⊢ (𝑄Δfunc𝐶) = (𝑄Δfunc𝐶)
73		curf2ndf.q	. . . . . . . . 9 ⊢ 𝑄 = (𝐷 FuncCat 𝐷)
74	73, 9, 9	fuccat 18153	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ Cat)
75	74	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑄 ∈ Cat)
76	73	fucbas 18143	. . . . . . 7 ⊢ (𝐷 Func 𝐷) = (Base‘𝑄)
77	69	idfucl 18061	. . . . . . . . 9 ⊢ (𝐷 ∈ Cat → (idfunc‘𝐷) ∈ (𝐷 Func 𝐷))
78	9, 77	syl 18	. . . . . . . 8 ⊢ (𝜑 → (idfunc‘𝐷) ∈ (𝐷 Func 𝐷))
79	78	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (idfunc‘𝐷) ∈ (𝐷 Func 𝐷))
80		eqid 2760	. . . . . . 7 ⊢ ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)) = ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))
81	72, 75, 35, 76, 79, 80, 3, 36	diag11 18422	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑥) = (idfunc‘𝐷))
82	71, 81	eqtr4d 2798	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥) = ((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑥))
83	82	mpteq2dva 5197	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥)) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑥)))
84		relfunc 18042	. . . . . . 7 ⊢ Rel (𝐶 Func 𝑄)
85	63, 73, 7, 9, 65	curfcl 18411	. . . . . . 7 ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) ∈ (𝐶 Func 𝑄))
86		1st2ndbr 8053	. . . . . . 7 ⊢ ((Rel (𝐶 Func 𝑄) ∧ (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) ∈ (𝐶 Func 𝑄)) → (1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))(𝐶 Func 𝑄)(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))))
87	84, 85, 86	sylancr 599	. . . . . 6 ⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))(𝐶 Func 𝑄)(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))))
88	3, 76, 87	funcf1 18046	. . . . 5 ⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))):(Base‘𝐶)⟶(𝐷 Func 𝐷))
89	88	feqmptd 6953	. . . 4 ⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥)))
90	72, 74, 7, 76, 78, 80	diag1cl 18421	. . . . . . 7 ⊢ (𝜑 → ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)) ∈ (𝐶 Func 𝑄))
91		1st2ndbr 8053	. . . . . . 7 ⊢ ((Rel (𝐶 Func 𝑄) ∧ ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)) ∈ (𝐶 Func 𝑄)) → (1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))(𝐶 Func 𝑄)(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))))
92	84, 90, 91	sylancr 599	. . . . . 6 ⊢ (𝜑 → (1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))(𝐶 Func 𝑄)(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))))
93	3, 76, 92	funcf1 18046	. . . . 5 ⊢ (𝜑 → (1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))):(Base‘𝐶)⟶(𝐷 Func 𝐷))
94	93	feqmptd 6953	. . . 4 ⊢ (𝜑 → (1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑥)))
95	83, 89, 94	3eqtr4d 2805	. . 3 ⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))) = (1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))))
96	9	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐷 ∈ Cat)
97	69, 4, 96	idfu1st 18059	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (1st ‘(idfunc‘𝐷)) = ( I ↾ (Base‘𝐷)))
98	97	coeq2d 5839	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((Id‘𝐷) ∘ (1st ‘(idfunc‘𝐷))) = ((Id‘𝐷) ∘ ( I ↾ (Base‘𝐷))))
99		eqid 2760	. . . . . . . . . . 11 ⊢ (Id‘𝑄) = (Id‘𝑄)
100		eqid 2760	. . . . . . . . . . 11 ⊢ (Id‘𝐷) = (Id‘𝐷)
101	78	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (idfunc‘𝐷) ∈ (𝐷 Func 𝐷))
102	73, 99, 100, 101	fucid 18154	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((Id‘𝑄)‘(idfunc‘𝐷)) = ((Id‘𝐷) ∘ (1st ‘(idfunc‘𝐷))))
103	4, 100	cidfn 17858	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ Cat → (Id‘𝐷) Fn (Base‘𝐷))
104	96, 103	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (Id‘𝐷) Fn (Base‘𝐷))
105		dffn2 6711	. . . . . . . . . . . . 13 ⊢ ((Id‘𝐷) Fn (Base‘𝐷) ↔ (Id‘𝐷):(Base‘𝐷)⟶V)
106	104, 105	sylib 221	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (Id‘𝐷):(Base‘𝐷)⟶V)
107	106	feqmptd 6953	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (Id‘𝐷) = (𝑧 ∈ (Base‘𝐷) ↦ ((Id‘𝐷)‘𝑧)))
108		fcoi1 6756	. . . . . . . . . . . 12 ⊢ ((Id‘𝐷):(Base‘𝐷)⟶V → ((Id‘𝐷) ∘ ( I ↾ (Base‘𝐷))) = (Id‘𝐷))
109	106, 108	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((Id‘𝐷) ∘ ( I ↾ (Base‘𝐷))) = (Id‘𝐷))
110	7	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐶 ∈ Cat)
111	110	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝐶 ∈ Cat)
112	96	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝐷 ∈ Cat)
113		simplrl 789	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑥 ∈ (Base‘𝐶))
114		opelxpi 5687	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐷)) → ⟨𝑥, 𝑧⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
115	113, 114	sylan 592	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ⟨𝑥, 𝑧⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
116		simplrr 790	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑦 ∈ (Base‘𝐶))
117		opelxpi 5687	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐷)) → ⟨𝑦, 𝑧⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
118	116, 117	sylan 592	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ⟨𝑦, 𝑧⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
119	2, 5, 6, 111, 112, 11, 115, 118	2ndf2 18375	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩) = (2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩)))
120	119	oveqd 7437	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓(⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)) = (𝑓(2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))((Id‘𝐷)‘𝑧)))
121		df-ov 7423	. . . . . . . . . . . . . . 15 ⊢ (𝑓(2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))((Id‘𝐷)‘𝑧)) = ((2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))‘⟨𝑓, ((Id‘𝐷)‘𝑧)⟩)
122		simplr 781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
123		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝑧 ∈ (Base‘𝐷))
124	4, 41, 100, 112, 123	catidcl 17861	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ((Id‘𝐷)‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧))
125	122, 124	opelxpd 5689	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ⟨𝑓, ((Id‘𝐷)‘𝑧)⟩ ∈ ((𝑥(Hom ‘𝐶)𝑦) × (𝑧(Hom ‘𝐷)𝑧)))
126	113	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝑥 ∈ (Base‘𝐶))
127	116	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝑦 ∈ (Base‘𝐶))
128	2, 3, 4, 33, 41, 126, 123, 127, 123, 6	xpchom2 18365	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩) = ((𝑥(Hom ‘𝐶)𝑦) × (𝑧(Hom ‘𝐷)𝑧)))
129	125, 128	eleqtrrd 2863	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ⟨𝑓, ((Id‘𝐷)‘𝑧)⟩ ∈ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))
130	129	fvresd 6905	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ((2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))‘⟨𝑓, ((Id‘𝐷)‘𝑧)⟩) = (2nd ‘⟨𝑓, ((Id‘𝐷)‘𝑧)⟩))
131	121, 130	eqtrid 2807	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓(2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))((Id‘𝐷)‘𝑧)) = (2nd ‘⟨𝑓, ((Id‘𝐷)‘𝑧)⟩))
132		fvex 6898	. . . . . . . . . . . . . . 15 ⊢ ((Id‘𝐷)‘𝑧) ∈ V
133	47, 132	op2nd 8010	. . . . . . . . . . . . . 14 ⊢ (2nd ‘⟨𝑓, ((Id‘𝐷)‘𝑧)⟩) = ((Id‘𝐷)‘𝑧)
134	131, 133	eqtrdi 2811	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓(2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))((Id‘𝐷)‘𝑧)) = ((Id‘𝐷)‘𝑧))
135	120, 134	eqtrd 2795	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓(⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)) = ((Id‘𝐷)‘𝑧))
136	135	mpteq2dva 5197	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑧 ∈ (Base‘𝐷) ↦ (𝑓(⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))) = (𝑧 ∈ (Base‘𝐷) ↦ ((Id‘𝐷)‘𝑧)))
137	107, 109, 136	3eqtr4rd 2806	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑧 ∈ (Base‘𝐷) ↦ (𝑓(⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))) = ((Id‘𝐷) ∘ ( I ↾ (Base‘𝐷))))
138	98, 102, 137	3eqtr4rd 2806	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑧 ∈ (Base‘𝐷) ↦ (𝑓(⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))) = ((Id‘𝑄)‘(idfunc‘𝐷)))
139	65	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝐶 2ndF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐷))
140		simpr 490	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
141		eqid 2760	. . . . . . . . . 10 ⊢ ((𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)‘𝑓) = ((𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)‘𝑓)
142	63, 3, 110, 96, 139, 4, 33, 100, 113, 116, 140, 141	curf2 18408	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)‘𝑓) = (𝑧 ∈ (Base‘𝐷) ↦ (𝑓(⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))))
143	74	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑄 ∈ Cat)
144	72, 143, 110, 76, 101, 80, 3, 113, 33, 99, 116, 140	diag12 18423	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)‘𝑓) = ((Id‘𝑄)‘(idfunc‘𝐷)))
145	138, 142, 144	3eqtr4d 2805	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)‘𝑓) = ((𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)‘𝑓))
146	145	mpteq2dva 5197	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)‘𝑓)) = (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)‘𝑓)))
147		eqid 2760	. . . . . . . . . 10 ⊢ (𝐷 Nat 𝐷) = (𝐷 Nat 𝐷)
148	73, 147	fuchom 18144	. . . . . . . . 9 ⊢ (𝐷 Nat 𝐷) = (Hom ‘𝑄)
149	87	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))(𝐶 Func 𝑄)(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))))
150		simprl 783	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶))
151		simprr 785	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶))
152	3, 33, 148, 149, 150, 151	funcf2 18048	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥)(𝐷 Nat 𝐷)((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑦)))
153	152	feqmptd 6953	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦) = (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)‘𝑓)))
154	92	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))(𝐶 Func 𝑄)(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))))
155	3, 33, 148, 154, 150, 151	funcf2 18048	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑥)(𝐷 Nat 𝐷)((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑦)))
156	155	feqmptd 6953	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦) = (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)‘𝑓)))
157	146, 153, 156	3eqtr4d 2805	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦) = (𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦))
158	157	3impb 1132	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦) = (𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦))
159	158	mpoeq3dva 7497	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)))
160	3, 87	funcfn2 18049	. . . . 5 ⊢ (𝜑 → (2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))) Fn ((Base‘𝐶) × (Base‘𝐶)))
161		fnov 7551	. . . . 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 18049	. . . . 5 ⊢ (𝜑 → (2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))) Fn ((Base‘𝐶) × (Base‘𝐶)))
164		fnov 7551	. . . . 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 2805	. . 3 ⊢ (𝜑 → (2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))) = (2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))))
167	95, 166	opeq12d 4847	. 2 ⊢ (𝜑 → ⟨(1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))), (2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))⟩ = ⟨(1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))), (2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))⟩)
168		1st2nd 8050	. . 3 ⊢ ((Rel (𝐶 Func 𝑄) ∧ (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) ∈ (𝐶 Func 𝑄)) → (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) = ⟨(1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))), (2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))⟩)
169	84, 85, 168	sylancr 599	. 2 ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) = ⟨(1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))), (2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))⟩)
170		1st2nd 8050	. . 3 ⊢ ((Rel (𝐶 Func 𝑄) ∧ ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)) ∈ (𝐶 Func 𝑄)) → ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)) = ⟨(1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))), (2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))⟩)
171	84, 90, 170	sylancr 599	. 2 ⊢ (𝜑 → ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)) = ⟨(1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))), (2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))⟩)
172	167, 169, 171	3eqtr4d 2805	1 ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) = ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  Vcvv 3450  ⟨cop 4834   class class class wbr 5102   ↦ cmpt 5185   I cid 5544   × cxp 5648   ↾ cres 5652   ∘ ccom 5654  Rel wrel 5655   Fn wfn 6533  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420   ∈ cmpo 7422  1^st c1st 7999  2^nd c2nd 8000  Basecbs 17392  Hom chom 17444  Catccat 17843  Idccid 17844   Func cfunc 18034  id_funccidfu 18035   Nat cnat 18124   FuncCat cfuc 18125   ×_c cxpc 18347   2^nd_F c2ndf 18349   curry_F ccurf 18389  Δ_funccdiag 18391

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11259  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-addrcl 11264  ax-mulcl 11265  ax-mulrcl 11266  ax-mulcom 11267  ax-addass 11268  ax-mulass 11269  ax-distr 11270  ax-i2m1 11271  ax-1ne0 11272  ax-1rid 11273  ax-rnegex 11274  ax-rrecex 11275  ax-cnre 11276  ax-pre-lttri 11277  ax-pre-lttrn 11278  ax-pre-ltadd 11279  ax-pre-mulgt0 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-1o 8479  df-er 8720  df-map 8852  df-ixp 8929  df-en 8977  df-dom 8978  df-sdom 8979  df-fin 8980  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351  df-le 11352  df-sub 11546  df-neg 11547  df-nn 12339  df-2 12408  df-3 12409  df-4 12410  df-5 12411  df-6 12412  df-7 12413  df-8 12414  df-9 12415  df-n0 12610  df-z 12697  df-dec 12818  df-uz 12969  df-fz 13643  df-struct 17330  df-slot 17365  df-ndx 17377  df-base 17393  df-hom 17457  df-cco 17458  df-cat 17847  df-cid 17848  df-func 18038  df-idfu 18039  df-nat 18126  df-fuc 18127  df-xpc 18351  df-1stf 18352  df-2ndf 18353  df-curf 18393  df-diag 18395

This theorem is used by: (None)