Theorem curf2ndf 18328

Description: As shown in diagval 18321, 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 7426	. . . . . . . . . . 11 ⊢ (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦) = ((1st ‘(𝐶 2ndF 𝐷))‘⟨𝑥, 𝑦⟩)
2		eqid 2766	. . . . . . . . . . . . 13 ⊢ (𝐶 ×c 𝐷) = (𝐶 ×c 𝐷)
3		eqid 2766	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐶) = (Base‘𝐶)
4		eqid 2766	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐷) = (Base‘𝐷)
5	2, 3, 4	xpcbas 18259	. . . . . . . . . . . . 13 ⊢ ((Base‘𝐶) × (Base‘𝐷)) = (Base‘(𝐶 ×c 𝐷))
6		eqid 2766	. . . . . . . . . . . . 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 2766	. . . . . . . . . . . . 13 ⊢ (𝐶 2ndF 𝐷) = (𝐶 2ndF 𝐷)
12		opelxpi 5703	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
13	12	adantll 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
14	2, 5, 6, 8, 10, 11, 13	2ndf1 18276	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((1st ‘(𝐶 2ndF 𝐷))‘⟨𝑥, 𝑦⟩) = (2nd ‘⟨𝑥, 𝑦⟩))
15		vex 3462	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
16		vex 3462	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
17	15, 16	op2nd 8004	. . . . . . . . . . . 12 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
18	14, 17	eqtrdi 2817	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → ((1st ‘(𝐶 2ndF 𝐷))‘⟨𝑥, 𝑦⟩) = 𝑦)
19	1, 18	eqtrid 2813	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦) = 𝑦)
20	19	mpteq2dva 5209	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦)) = (𝑦 ∈ (Base‘𝐷) ↦ 𝑦))
21		mptresid 6058	. . . . . . . . 9 ⊢ ( I ↾ (Base‘𝐷)) = (𝑦 ∈ (Base‘𝐷) ↦ 𝑦)
22	20, 21	eqtr4di 2819	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦)) = ( I ↾ (Base‘𝐷)))
23		df-ov 7426	. . . . . . . . . . . . . . 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 5705	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑥, 𝑧⟩ ∈ ((Base‘𝐶) × (Base‘𝐷)))
30	2, 5, 6, 24, 25, 11, 26, 29	2ndf2 18277	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩) = (2nd ↾ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩)))
31	30	fveq1d 6890	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩) = ((2nd ↾ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩))‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩))
32	23, 31	eqtrid 2813	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓) = ((2nd ↾ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩))‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩))
33		eqid 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
34		eqid 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Id‘𝐶) = (Id‘𝐶)
35	7	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
36		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
37	3, 33, 34, 35, 36	catidcl 17763	. . . . . . . . . . . . . . . . . . 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 5705	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨((Id‘𝐶)‘𝑥), 𝑓⟩ ∈ ((𝑥(Hom ‘𝐶)𝑥) × (𝑦(Hom ‘𝐷)𝑧)))
41		eqid 2766	. . . . . . . . . . . . . . . . . 18 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
42		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑦 ∈ (Base‘𝐷))
43	2, 3, 4, 33, 41, 27, 42, 27, 28, 6	xpchom2 18267	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩) = ((𝑥(Hom ‘𝐶)𝑥) × (𝑦(Hom ‘𝐷)𝑧)))
44	40, 43	eleqtrrd 2869	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨((Id‘𝐶)‘𝑥), 𝑓⟩ ∈ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩))
45	44	fvresd 6908	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((2nd ↾ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩))‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩) = (2nd ‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩))
46		fvex 6901	. . . . . . . . . . . . . . . 16 ⊢ ((Id‘𝐶)‘𝑥) ∈ V
47		vex 3462	. . . . . . . . . . . . . . . 16 ⊢ 𝑓 ∈ V
48	46, 47	op2nd 8004	. . . . . . . . . . . . . . 15 ⊢ (2nd ‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩) = 𝑓
49	45, 48	eqtrdi 2817	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((2nd ↾ (⟨𝑥, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑥, 𝑧⟩))‘⟨((Id‘𝐶)‘𝑥), 𝑓⟩) = 𝑓)
50	32, 49	eqtrd 2801	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓) = 𝑓)
51	50	mpteq2dva 5209	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓)) = (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ 𝑓))
52		mptresid 6058	. . . . . . . . . . . 12 ⊢ ( I ↾ (𝑦(Hom ‘𝐷)𝑧)) = (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ 𝑓)
53	51, 52	eqtr4di 2819	. . . . . . . . . . 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 7500	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓))) = (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ ( I ↾ (𝑦(Hom ‘𝐷)𝑧))))
56		fveq2 6888	. . . . . . . . . . . 12 ⊢ (𝑢 = ⟨𝑦, 𝑧⟩ → ((Hom ‘𝐷)‘𝑢) = ((Hom ‘𝐷)‘⟨𝑦, 𝑧⟩))
57		df-ov 7426	. . . . . . . . . . . 12 ⊢ (𝑦(Hom ‘𝐷)𝑧) = ((Hom ‘𝐷)‘⟨𝑦, 𝑧⟩)
58	56, 57	eqtr4di 2819	. . . . . . . . . . 11 ⊢ (𝑢 = ⟨𝑦, 𝑧⟩ → ((Hom ‘𝐷)‘𝑢) = (𝑦(Hom ‘𝐷)𝑧))
59	58	reseq2d 5983	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑦, 𝑧⟩ → ( I ↾ ((Hom ‘𝐷)‘𝑢)) = ( I ↾ (𝑦(Hom ‘𝐷)𝑧)))
60	59	mpompt 7537	. . . . . . . . 9 ⊢ (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ ( I ↾ ((Hom ‘𝐷)‘𝑢))) = (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ ( I ↾ (𝑦(Hom ‘𝐷)𝑧)))
61	55, 60	eqtr4di 2819	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓))) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ ( I ↾ ((Hom ‘𝐷)‘𝑢))))
62	22, 61	opeq12d 4851	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓)))⟩ = ⟨( I ↾ (Base‘𝐷)), (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ ( I ↾ ((Hom ‘𝐷)‘𝑢)))⟩)
63		eqid 2766	. . . . . . . 8 ⊢ (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) = (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))
64	9	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐷 ∈ Cat)
65	2, 7, 9, 11	2ndfcl 18279	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 2ndF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐷))
66	65	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝐶 2ndF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐷))
67		eqid 2766	. . . . . . . 8 ⊢ ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥) = ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥)
68	63, 3, 35, 64, 66, 4, 36, 67, 41, 34	curf1 18306	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥) = ⟨(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘(𝐶 2ndF 𝐷))𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑓 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑥, 𝑧⟩)𝑓)))⟩)
69		eqid 2766	. . . . . . . 8 ⊢ (idfunc‘𝐷) = (idfunc‘𝐷)
70	69, 4, 64, 41	idfuval 17958	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (idfunc‘𝐷) = ⟨( I ↾ (Base‘𝐷)), (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ ( I ↾ ((Hom ‘𝐷)‘𝑢)))⟩)
71	62, 68, 70	3eqtr4d 2811	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥) = (idfunc‘𝐷))
72		eqid 2766	. . . . . . 7 ⊢ (𝑄Δfunc𝐶) = (𝑄Δfunc𝐶)
73		curf2ndf.q	. . . . . . . . 9 ⊢ 𝑄 = (𝐷 FuncCat 𝐷)
74	73, 9, 9	fuccat 18055	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ Cat)
75	74	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑄 ∈ Cat)
76	73	fucbas 18045	. . . . . . 7 ⊢ (𝐷 Func 𝐷) = (Base‘𝑄)
77	69	idfucl 17963	. . . . . . . . 9 ⊢ (𝐷 ∈ Cat → (idfunc‘𝐷) ∈ (𝐷 Func 𝐷))
78	9, 77	syl 18	. . . . . . . 8 ⊢ (𝜑 → (idfunc‘𝐷) ∈ (𝐷 Func 𝐷))
79	78	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (idfunc‘𝐷) ∈ (𝐷 Func 𝐷))
80		eqid 2766	. . . . . . 7 ⊢ ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)) = ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))
81	72, 75, 35, 76, 79, 80, 3, 36	diag11 18324	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑥) = (idfunc‘𝐷))
82	71, 81	eqtr4d 2804	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥) = ((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑥))
83	82	mpteq2dva 5209	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥)) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑥)))
84		relfunc 17944	. . . . . . 7 ⊢ Rel (𝐶 Func 𝑄)
85	63, 73, 7, 9, 65	curfcl 18313	. . . . . . 7 ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) ∈ (𝐶 Func 𝑄))
86		1st2ndbr 8048	. . . . . . 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 17948	. . . . 5 ⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))):(Base‘𝐶)⟶(𝐷 Func 𝐷))
89	88	feqmptd 6956	. . . 4 ⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥)))
90	72, 74, 7, 76, 78, 80	diag1cl 18323	. . . . . . 7 ⊢ (𝜑 → ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)) ∈ (𝐶 Func 𝑄))
91		1st2ndbr 8048	. . . . . . 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 17948	. . . . 5 ⊢ (𝜑 → (1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))):(Base‘𝐶)⟶(𝐷 Func 𝐷))
94	93	feqmptd 6956	. . . 4 ⊢ (𝜑 → (1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑥)))
95	83, 89, 94	3eqtr4d 2811	. . 3 ⊢ (𝜑 → (1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))) = (1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))))
96	9	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐷 ∈ Cat)
97	69, 4, 96	idfu1st 17961	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (1st ‘(idfunc‘𝐷)) = ( I ↾ (Base‘𝐷)))
98	97	coeq2d 5853	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((Id‘𝐷) ∘ (1st ‘(idfunc‘𝐷))) = ((Id‘𝐷) ∘ ( I ↾ (Base‘𝐷))))
99		eqid 2766	. . . . . . . . . . 11 ⊢ (Id‘𝑄) = (Id‘𝑄)
100		eqid 2766	. . . . . . . . . . 11 ⊢ (Id‘𝐷) = (Id‘𝐷)
101	78	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (idfunc‘𝐷) ∈ (𝐷 Func 𝐷))
102	73, 99, 100, 101	fucid 18056	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((Id‘𝑄)‘(idfunc‘𝐷)) = ((Id‘𝐷) ∘ (1st ‘(idfunc‘𝐷))))
103	4, 100	cidfn 17760	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ Cat → (Id‘𝐷) Fn (Base‘𝐷))
104	96, 103	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (Id‘𝐷) Fn (Base‘𝐷))
105		dffn2 6714	. . . . . . . . . . . . 13 ⊢ ((Id‘𝐷) Fn (Base‘𝐷) ↔ (Id‘𝐷):(Base‘𝐷)⟶V)
106	104, 105	sylib 221	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (Id‘𝐷):(Base‘𝐷)⟶V)
107	106	feqmptd 6956	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (Id‘𝐷) = (𝑧 ∈ (Base‘𝐷) ↦ ((Id‘𝐷)‘𝑧)))
108		fcoi1 6759	. . . . . . . . . . . 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 5703	. . . . . . . . . . . . . . . 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 5703	. . . . . . . . . . . . . . . 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 18277	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩) = (2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩)))
120	119	oveqd 7440	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓(⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)) = (𝑓(2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))((Id‘𝐷)‘𝑧)))
121		df-ov 7426	. . . . . . . . . . . . . . 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 17763	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ((Id‘𝐷)‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧))
125	122, 124	opelxpd 5705	. . . . . . . . . . . . . . . . 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 18267	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩) = ((𝑥(Hom ‘𝐶)𝑦) × (𝑧(Hom ‘𝐷)𝑧)))
129	125, 128	eleqtrrd 2869	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ⟨𝑓, ((Id‘𝐷)‘𝑧)⟩ ∈ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))
130	129	fvresd 6908	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ((2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))‘⟨𝑓, ((Id‘𝐷)‘𝑧)⟩) = (2nd ‘⟨𝑓, ((Id‘𝐷)‘𝑧)⟩))
131	121, 130	eqtrid 2813	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓(2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))((Id‘𝐷)‘𝑧)) = (2nd ‘⟨𝑓, ((Id‘𝐷)‘𝑧)⟩))
132		fvex 6901	. . . . . . . . . . . . . . 15 ⊢ ((Id‘𝐷)‘𝑧) ∈ V
133	47, 132	op2nd 8004	. . . . . . . . . . . . . 14 ⊢ (2nd ‘⟨𝑓, ((Id‘𝐷)‘𝑧)⟩) = ((Id‘𝐷)‘𝑧)
134	131, 133	eqtrdi 2817	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓(2nd ↾ (⟨𝑥, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑦, 𝑧⟩))((Id‘𝐷)‘𝑧)) = ((Id‘𝐷)‘𝑧))
135	120, 134	eqtrd 2801	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑓(⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)) = ((Id‘𝐷)‘𝑧))
136	135	mpteq2dva 5209	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑧 ∈ (Base‘𝐷) ↦ (𝑓(⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))) = (𝑧 ∈ (Base‘𝐷) ↦ ((Id‘𝐷)‘𝑧)))
137	107, 109, 136	3eqtr4rd 2812	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑧 ∈ (Base‘𝐷) ↦ (𝑓(⟨𝑥, 𝑧⟩(2nd ‘(𝐶 2ndF 𝐷))⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))) = ((Id‘𝐷) ∘ ( I ↾ (Base‘𝐷))))
138	98, 102, 137	3eqtr4rd 2812	. . . . . . . . 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 2766	. . . . . . . . . 10 ⊢ ((𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)‘𝑓) = ((𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)‘𝑓)
142	63, 3, 110, 96, 139, 4, 33, 100, 113, 116, 140, 141	curf2 18310	. . . . . . . . 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 18325	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)‘𝑓) = ((Id‘𝑄)‘(idfunc‘𝐷)))
145	138, 142, 144	3eqtr4d 2811	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)‘𝑓) = ((𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)‘𝑓))
146	145	mpteq2dva 5209	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)‘𝑓)) = (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)‘𝑓)))
147		eqid 2766	. . . . . . . . . 10 ⊢ (𝐷 Nat 𝐷) = (𝐷 Nat 𝐷)
148	73, 147	fuchom 18046	. . . . . . . . 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 17950	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑥)(𝐷 Nat 𝐷)((1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))‘𝑦)))
153	152	feqmptd 6956	. . . . . . 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 17950	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑥)(𝐷 Nat 𝐷)((1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))‘𝑦)))
156	155	feqmptd 6956	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦) = (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)‘𝑓)))
157	146, 153, 156	3eqtr4d 2811	. . . . . 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 7500	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))𝑦)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))𝑦)))
160	3, 87	funcfn2 17951	. . . . 5 ⊢ (𝜑 → (2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))) Fn ((Base‘𝐶) × (Base‘𝐶)))
161		fnov 7554	. . . . 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 17951	. . . . 5 ⊢ (𝜑 → (2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))) Fn ((Base‘𝐶) × (Base‘𝐶)))
164		fnov 7554	. . . . 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 2811	. . 3 ⊢ (𝜑 → (2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))) = (2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))))
167	95, 166	opeq12d 4851	. 2 ⊢ (𝜑 → ⟨(1st ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷))), (2nd ‘(⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)))⟩ = ⟨(1st ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷))), (2nd ‘((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))⟩)
168		1st2nd 8045	. . 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 8045	. . 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 2811	1 ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ curryF (𝐶 2ndF 𝐷)) = ((1st ‘(𝑄Δfunc𝐶))‘(idfunc‘𝐷)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  Vcvv 3458  ⟨cop 4600   class class class wbr 5114   ↦ cmpt 5197   I cid 5560   × cxp 5664   ↾ cres 5668   ∘ ccom 5670  Rel wrel 5671   Fn wfn 6538  ⟶wf 6539  ‘cfv 6543  (class class class)co 7423   ∈ cmpo 7425  1^st c1st 7993  2^nd c2nd 7994  Basecbs 17294  Hom chom 17346  Catccat 17745  Idccid 17746   Func cfunc 17936  id_funccidfu 17937   Nat cnat 18026   FuncCat cfuc 18027   ×_c cxpc 18249   2^nd_F c2ndf 18251   curry_F ccurf 18291  Δ_funccdiag 18293

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194  ax-pre-mulgt0 11195

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-tp 4599  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-1st 7995  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8703  df-map 8835  df-ixp 8905  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11461  df-neg 11462  df-nn 12252  df-2 12321  df-3 12322  df-4 12323  df-5 12324  df-6 12325  df-7 12326  df-8 12327  df-9 12328  df-n0 12523  df-z 12610  df-dec 12730  df-uz 12881  df-fz 13554  df-struct 17232  df-slot 17267  df-ndx 17279  df-base 17295  df-hom 17359  df-cco 17360  df-cat 17749  df-cid 17750  df-func 17940  df-idfu 17941  df-nat 18028  df-fuc 18029  df-xpc 18253  df-1stf 18254  df-2ndf 18255  df-curf 18295  df-diag 18297

This theorem is used by: (None)