Theorem curf2cl 17351

Description: The curry functor at a morphism is a natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017.)

Hypotheses

Ref	Expression
curf2.g	⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)
curf2.a	⊢ 𝐴 = (Base‘𝐶)
curf2.c	⊢ (𝜑 → 𝐶 ∈ Cat)
curf2.d	⊢ (𝜑 → 𝐷 ∈ Cat)
curf2.f	⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
curf2.b	⊢ 𝐵 = (Base‘𝐷)
curf2.h	⊢ 𝐻 = (Hom ‘𝐶)
curf2.i	⊢ 𝐼 = (Id‘𝐷)
curf2.x	⊢ (𝜑 → 𝑋 ∈ 𝐴)
curf2.y	⊢ (𝜑 → 𝑌 ∈ 𝐴)
curf2.k	⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))
curf2.l	⊢ 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)
curf2.n	⊢ 𝑁 = (𝐷 Nat 𝐸)

Assertion

Ref	Expression
curf2cl	⊢ (𝜑 → 𝐿 ∈ (((1st ‘𝐺)‘𝑋)𝑁((1st ‘𝐺)‘𝑌)))

Proof of Theorem curf2cl

Dummy variables 𝑧 𝑤 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		curf2.g	. . . 4 ⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)
2		curf2.a	. . . 4 ⊢ 𝐴 = (Base‘𝐶)
3		curf2.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Cat)
4		curf2.d	. . . 4 ⊢ (𝜑 → 𝐷 ∈ Cat)
5		curf2.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
6		curf2.b	. . . 4 ⊢ 𝐵 = (Base‘𝐷)
7		curf2.h	. . . 4 ⊢ 𝐻 = (Hom ‘𝐶)
8		curf2.i	. . . 4 ⊢ 𝐼 = (Id‘𝐷)
9		curf2.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
10		curf2.y	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝐴)
11		curf2.k	. . . 4 ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))
12		curf2.l	. . . 4 ⊢ 𝐿 = ((𝑋(2nd ‘𝐺)𝑌)‘𝐾)
13	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	curf2 17349	. . 3 ⊢ (𝜑 → 𝐿 = (𝑧 ∈ 𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧))))
14		eqid 2780	. . . . . . . . . 10 ⊢ (𝐶 ×c 𝐷) = (𝐶 ×c 𝐷)
15	14, 2, 6	xpcbas 17298	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷))
16		eqid 2780	. . . . . . . . 9 ⊢ (Hom ‘(𝐶 ×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷))
17		eqid 2780	. . . . . . . . 9 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
18		relfunc 17002	. . . . . . . . . . 11 ⊢ Rel ((𝐶 ×c 𝐷) Func 𝐸)
19		1st2ndbr 7559	. . . . . . . . . . 11 ⊢ ((Rel ((𝐶 ×c 𝐷) Func 𝐸) ∧ 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
20	18, 5, 19	sylancr 579	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
21	20	adantr 473	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
22		opelxpi 5448	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
23	9, 22	sylan 572	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
24		opelxpi 5448	. . . . . . . . . 10 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
25	10, 24	sylan 572	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
26	15, 16, 17, 21, 23, 25	funcf2 17008	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩):(⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩)⟶(((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
27		eqid 2780	. . . . . . . . . 10 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
28	9	adantr 473	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑋 ∈ 𝐴)
29		simpr 477	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵)
30	10	adantr 473	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑌 ∈ 𝐴)
31	14, 2, 6, 7, 27, 28, 29, 30, 29, 16	xpchom2 17306	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩) = ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
32	31	feq2d 6335	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩):(⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩)⟶(((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)) ↔ (⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩):((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧))⟶(((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩))))
33	26, 32	mpbid 224	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩):((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧))⟶(((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
34	11	adantr 473	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐾 ∈ (𝑋𝐻𝑌))
35	4	adantr 473	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐷 ∈ Cat)
36	6, 27, 8, 35, 29	catidcl 16823	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐼‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧))
37	33, 34, 36	fovrnd 7142	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
38	3	adantr 473	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐶 ∈ Cat)
39	5	adantr 473	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
40		eqid 2780	. . . . . . . . 9 ⊢ ((1st ‘𝐺)‘𝑋) = ((1st ‘𝐺)‘𝑋)
41	1, 2, 38, 35, 39, 6, 28, 40, 29	curf11 17346	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧) = (𝑋(1st ‘𝐹)𝑧))
42		df-ov 6985	. . . . . . . 8 ⊢ (𝑋(1st ‘𝐹)𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)
43	41, 42	syl6eq 2832	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩))
44		eqid 2780	. . . . . . . . 9 ⊢ ((1st ‘𝐺)‘𝑌) = ((1st ‘𝐺)‘𝑌)
45	1, 2, 38, 35, 39, 6, 30, 44, 29	curf11 17346	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧) = (𝑌(1st ‘𝐹)𝑧))
46		df-ov 6985	. . . . . . . 8 ⊢ (𝑌(1st ‘𝐹)𝑧) = ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)
47	45, 46	syl6eq 2832	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧) = ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩))
48	43, 47	oveq12d 7000	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)) = (((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
49	37, 48	eleqtrrd 2871	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)))
50	49	ralrimiva 3134	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)))
51	6	fvexi 6518	. . . . 5 ⊢ 𝐵 ∈ V
52		mptelixpg 8302	. . . . 5 ⊢ (𝐵 ∈ V → ((𝑧 ∈ 𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧))) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧))))
53	51, 52	ax-mp 5	. . . 4 ⊢ ((𝑧 ∈ 𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧))) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)))
54	50, 53	sylibr 226	. . 3 ⊢ (𝜑 → (𝑧 ∈ 𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧))) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)))
55	13, 54	eqeltrd 2868	. 2 ⊢ (𝜑 → 𝐿 ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)))
56		eqid 2780	. . . . . . . . . 10 ⊢ (Id‘𝐶) = (Id‘𝐶)
57	3	adantr 473	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐶 ∈ Cat)
58	9	adantr 473	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑋 ∈ 𝐴)
59		eqid 2780	. . . . . . . . . 10 ⊢ (comp‘𝐶) = (comp‘𝐶)
60	10	adantr 473	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑌 ∈ 𝐴)
61	11	adantr 473	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐾 ∈ (𝑋𝐻𝑌))
62	2, 7, 56, 57, 58, 59, 60, 61	catrid 16825	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) = 𝐾)
63	2, 7, 56, 57, 58, 59, 60, 61	catlid 16824	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾) = 𝐾)
64	62, 63	eqtr4d 2819	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) = (((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾))
65	4	adantr 473	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐷 ∈ Cat)
66		simpr1 1175	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑧 ∈ 𝐵)
67		eqid 2780	. . . . . . . . . 10 ⊢ (comp‘𝐷) = (comp‘𝐷)
68		simpr2 1176	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑤 ∈ 𝐵)
69		simpr3 1177	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))
70	6, 27, 8, 65, 66, 67, 68, 69	catlid 16824	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓) = 𝑓)
71	6, 27, 8, 65, 66, 67, 68, 69	catrid 16825	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧)) = 𝑓)
72	70, 71	eqtr4d 2819	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓) = (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧)))
73	64, 72	opeq12d 4690	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨(𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)), ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓)⟩ = ⟨(((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾), (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧))⟩)
74		eqid 2780	. . . . . . . 8 ⊢ (comp‘(𝐶 ×c 𝐷)) = (comp‘(𝐶 ×c 𝐷))
75	2, 7, 56, 57, 58	catidcl 16823	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑋) ∈ (𝑋𝐻𝑋))
76	6, 27, 8, 65, 68	catidcl 16823	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐼‘𝑤) ∈ (𝑤(Hom ‘𝐷)𝑤))
77	14, 2, 6, 7, 27, 58, 66, 58, 68, 59, 67, 74, 60, 68, 75, 69, 61, 76	xpcco2 17307	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩) = ⟨(𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)), ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓)⟩)
78	36	3ad2antr1 1169	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐼‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧))
79	2, 7, 56, 57, 60	catidcl 16823	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑌) ∈ (𝑌𝐻𝑌))
80	14, 2, 6, 7, 27, 58, 66, 60, 66, 59, 67, 74, 60, 68, 61, 78, 79, 69	xpcco2 17307	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩) = ⟨(((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾), (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧))⟩)
81	73, 77, 80	3eqtr4d 2826	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩) = (⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩))
82	81	fveq2d 6508	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩)))
83		eqid 2780	. . . . . 6 ⊢ (comp‘𝐸) = (comp‘𝐸)
84	20	adantr 473	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
85	23	3ad2antr1 1169	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
86	58, 68	opelxpd 5449	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑤⟩ ∈ (𝐴 × 𝐵))
87	60, 68	opelxpd 5449	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑌, 𝑤⟩ ∈ (𝐴 × 𝐵))
88	75, 69	opelxpd 5449	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑓⟩ ∈ ((𝑋𝐻𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
89	14, 2, 6, 7, 27, 58, 66, 58, 68, 16	xpchom2 17306	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩) = ((𝑋𝐻𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
90	88, 89	eleqtrrd 2871	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑓⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩))
91	61, 76	opelxpd 5449	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑤)⟩ ∈ ((𝑋𝐻𝑌) × (𝑤(Hom ‘𝐷)𝑤)))
92	14, 2, 6, 7, 27, 58, 68, 60, 68, 16	xpchom2 17306	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑤⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩) = ((𝑋𝐻𝑌) × (𝑤(Hom ‘𝐷)𝑤)))
93	91, 92	eleqtrrd 2871	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑤)⟩ ∈ (⟨𝑋, 𝑤⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩))
94	15, 16, 74, 83, 84, 85, 86, 87, 90, 93	funcco 17011	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = (((⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)))
95	25	3ad2antr1 1169	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
96	61, 78	opelxpd 5449	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑧)⟩ ∈ ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
97	14, 2, 6, 7, 27, 58, 66, 60, 66, 16	xpchom2 17306	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩) = ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
98	96, 97	eleqtrrd 2871	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑧)⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩))
99	79, 69	opelxpd 5449	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑌), 𝑓⟩ ∈ ((𝑌𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑤)))
100	14, 2, 6, 7, 27, 60, 66, 60, 68, 16	xpchom2 17306	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑌, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩) = ((𝑌𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑤)))
101	99, 100	eleqtrrd 2871	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑌), 𝑓⟩ ∈ (⟨𝑌, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩))
102	15, 16, 74, 83, 84, 85, 95, 87, 98, 101	funcco 17011	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩)) = (((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)))
103	82, 94, 102	3eqtr3d 2824	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = (((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)))
104	5	adantr 473	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
105	1, 2, 57, 65, 104, 6, 58, 40, 66	curf11 17346	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧) = (𝑋(1st ‘𝐹)𝑧))
106	105, 42	syl6eq 2832	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩))
107	1, 2, 57, 65, 104, 6, 58, 40, 68	curf11 17346	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤) = (𝑋(1st ‘𝐹)𝑤))
108		df-ov 6985	. . . . . . . 8 ⊢ (𝑋(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)
109	107, 108	syl6eq 2832	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤) = ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))
110	106, 109	opeq12d 4690	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤)⟩ = ⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩)
111	1, 2, 57, 65, 104, 6, 60, 44, 68	curf11 17346	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤) = (𝑌(1st ‘𝐹)𝑤))
112		df-ov 6985	. . . . . . 7 ⊢ (𝑌(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘⟨𝑌, 𝑤⟩)
113	111, 112	syl6eq 2832	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤) = ((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))
114	110, 113	oveq12d 7000	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤)) = (⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩)))
115	1, 2, 57, 65, 104, 6, 7, 8, 58, 60, 61, 12, 68	curf2val 17350	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑤) = (𝐾(⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)(𝐼‘𝑤)))
116		df-ov 6985	. . . . . 6 ⊢ (𝐾(⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)(𝐼‘𝑤)) = ((⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩)
117	115, 116	syl6eq 2832	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑤) = ((⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩))
118	1, 2, 57, 65, 104, 6, 58, 40, 66, 27, 56, 68, 69	curf12 17347	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st ‘𝐺)‘𝑋))𝑤)‘𝑓) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)𝑓))
119		df-ov 6985	. . . . . 6 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)𝑓) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)
120	118, 119	syl6eq 2832	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st ‘𝐺)‘𝑋))𝑤)‘𝑓) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩))
121	114, 117, 120	oveq123d 7003	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐿‘𝑤)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))((𝑧(2nd ‘((1st ‘𝐺)‘𝑋))𝑤)‘𝑓)) = (((⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)))
122	1, 2, 57, 65, 104, 6, 60, 44, 66	curf11 17346	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧) = (𝑌(1st ‘𝐹)𝑧))
123	122, 46	syl6eq 2832	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧) = ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩))
124	106, 123	opeq12d 4690	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)⟩ = ⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩)
125	124, 113	oveq12d 7000	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤)) = (⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩)))
126	1, 2, 57, 65, 104, 6, 60, 44, 66, 27, 56, 68, 69	curf12 17347	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓) = (((Id‘𝐶)‘𝑌)(⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)𝑓))
127		df-ov 6985	. . . . . 6 ⊢ (((Id‘𝐶)‘𝑌)(⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)𝑓) = ((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)
128	126, 127	syl6eq 2832	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓) = ((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩))
129	1, 2, 57, 65, 104, 6, 7, 8, 58, 60, 61, 12, 66	curf2val 17350	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑧) = (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)))
130		df-ov 6985	. . . . . 6 ⊢ (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)
131	129, 130	syl6eq 2832	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑧) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩))
132	125, 128, 131	oveq123d 7003	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧)) = (((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)))
133	103, 121, 132	3eqtr4d 2826	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐿‘𝑤)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))((𝑧(2nd ‘((1st ‘𝐺)‘𝑋))𝑤)‘𝑓)) = (((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧)))
134	133	ralrimivvva 3144	. 2 ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤)((𝐿‘𝑤)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))((𝑧(2nd ‘((1st ‘𝐺)‘𝑋))𝑤)‘𝑓)) = (((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧)))
135		curf2.n	. . 3 ⊢ 𝑁 = (𝐷 Nat 𝐸)
136	1, 2, 3, 4, 5, 6, 9, 40	curf1cl 17348	. . 3 ⊢ (𝜑 → ((1st ‘𝐺)‘𝑋) ∈ (𝐷 Func 𝐸))
137	1, 2, 3, 4, 5, 6, 10, 44	curf1cl 17348	. . 3 ⊢ (𝜑 → ((1st ‘𝐺)‘𝑌) ∈ (𝐷 Func 𝐸))
138	135, 6, 27, 17, 83, 136, 137	isnat2 17088	. 2 ⊢ (𝜑 → (𝐿 ∈ (((1st ‘𝐺)‘𝑋)𝑁((1st ‘𝐺)‘𝑌)) ↔ (𝐿 ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)) ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤)((𝐿‘𝑤)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))((𝑧(2nd ‘((1st ‘𝐺)‘𝑋))𝑤)‘𝑓)) = (((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧)))))
139	55, 134, 138	mpbir2and 701	1 ⊢ (𝜑 → 𝐿 ∈ (((1st ‘𝐺)‘𝑋)𝑁((1st ‘𝐺)‘𝑌)))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   ∧ w3a 1069   = wceq 1508   ∈ wcel 2051  ∀wral 3090  Vcvv 3417  ⟨cop 4450   class class class wbr 4934   ↦ cmpt 5013   × cxp 5409  Rel wrel 5416  ⟶wf 6189  ‘cfv 6193  (class class class)co 6982  1^st c1st 7505  2^nd c2nd 7506  Xcixp 8265  Basecbs 16345  Hom chom 16438  compcco 16439  Catccat 16805  Idccid 16806   Func cfunc 16994   Nat cnat 17081   ×_c cxpc 17288   curry_F ccurf 17330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2752  ax-rep 5053  ax-sep 5064  ax-nul 5071  ax-pow 5123  ax-pr 5190  ax-un 7285  ax-cnex 10397  ax-resscn 10398  ax-1cn 10399  ax-icn 10400  ax-addcl 10401  ax-addrcl 10402  ax-mulcl 10403  ax-mulrcl 10404  ax-mulcom 10405  ax-addass 10406  ax-mulass 10407  ax-distr 10408  ax-i2m1 10409  ax-1ne0 10410  ax-1rid 10411  ax-rnegex 10412  ax-rrecex 10413  ax-cnre 10414  ax-pre-lttri 10415  ax-pre-lttrn 10416  ax-pre-ltadd 10417  ax-pre-mulgt0 10418

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-fal 1521  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2551  df-eu 2589  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3419  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-pss 3847  df-nul 4182  df-if 4354  df-pw 4427  df-sn 4445  df-pr 4447  df-tp 4449  df-op 4451  df-uni 4718  df-int 4755  df-iun 4799  df-br 4935  df-opab 4997  df-mpt 5014  df-tr 5036  df-id 5316  df-eprel 5321  df-po 5330  df-so 5331  df-fr 5370  df-we 5372  df-xp 5417  df-rel 5418  df-cnv 5419  df-co 5420  df-dm 5421  df-rn 5422  df-res 5423  df-ima 5424  df-pred 5991  df-ord 6037  df-on 6038  df-lim 6039  df-suc 6040  df-iota 6157  df-fun 6195  df-fn 6196  df-f 6197  df-f1 6198  df-fo 6199  df-f1o 6200  df-fv 6201  df-riota 6943  df-ov 6985  df-oprab 6986  df-mpo 6987  df-om 7403  df-1st 7507  df-2nd 7508  df-wrecs 7756  df-recs 7818  df-rdg 7856  df-1o 7911  df-oadd 7915  df-er 8095  df-map 8214  df-ixp 8266  df-en 8313  df-dom 8314  df-sdom 8315  df-fin 8316  df-pnf 10482  df-mnf 10483  df-xr 10484  df-ltxr 10485  df-le 10486  df-sub 10678  df-neg 10679  df-nn 11446  df-2 11509  df-3 11510  df-4 11511  df-5 11512  df-6 11513  df-7 11514  df-8 11515  df-9 11516  df-n0 11714  df-z 11800  df-dec 11918  df-uz 12065  df-fz 12715  df-struct 16347  df-ndx 16348  df-slot 16349  df-base 16351  df-hom 16451  df-cco 16452  df-cat 16809  df-cid 16810  df-func 16998  df-nat 17083  df-xpc 17292  df-curf 17334

This theorem is referenced by:  curfcl  17352