Theorem curf2cl 18253

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 18251	. . 3 ⊢ (𝜑 → 𝐿 = (𝑧 ∈ 𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧))))
14		eqid 2761	. . . . . . . . . 10 ⊢ (𝐶 ×c 𝐷) = (𝐶 ×c 𝐷)
15	14, 2, 6	xpcbas 18200	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷))
16		eqid 2761	. . . . . . . . 9 ⊢ (Hom ‘(𝐶 ×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷))
17		eqid 2761	. . . . . . . . 9 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
18		relfunc 17885	. . . . . . . . . . 11 ⊢ Rel ((𝐶 ×c 𝐷) Func 𝐸)
19		1st2ndbr 8017	. . . . . . . . . . 11 ⊢ ((Rel ((𝐶 ×c 𝐷) Func 𝐸) ∧ 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
20	18, 5, 19	sylancr 596	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
21	20	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
22		opelxpi 5680	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
23	9, 22	sylan 589	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
24		opelxpi 5680	. . . . . . . . . 10 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
25	10, 24	sylan 589	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
26	15, 16, 17, 21, 23, 25	funcf2 17891	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩):(⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩)⟶(((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
27		eqid 2761	. . . . . . . . . 10 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
28	9	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑋 ∈ 𝐴)
29		simpr 488	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵)
30	10	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑌 ∈ 𝐴)
31	14, 2, 6, 7, 27, 28, 29, 30, 29, 16	xpchom2 18208	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩) = ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
32	31	feq2d 6669	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩):(⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩)⟶(((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)) ↔ (⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩):((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧))⟶(((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩))))
33	26, 32	mpbid 234	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩):((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧))⟶(((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
34	11	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐾 ∈ (𝑋𝐻𝑌))
35	4	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐷 ∈ Cat)
36	6, 27, 8, 35, 29	catidcl 17704	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐼‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧))
37	33, 34, 36	fovcdmd 7562	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
38	3	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐶 ∈ Cat)
39	5	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
40		eqid 2761	. . . . . . . . 9 ⊢ ((1st ‘𝐺)‘𝑋) = ((1st ‘𝐺)‘𝑋)
41	1, 2, 38, 35, 39, 6, 28, 40, 29	curf11 18248	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧) = (𝑋(1st ‘𝐹)𝑧))
42		df-ov 7393	. . . . . . . 8 ⊢ (𝑋(1st ‘𝐹)𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)
43	41, 42	eqtrdi 2812	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩))
44		eqid 2761	. . . . . . . . 9 ⊢ ((1st ‘𝐺)‘𝑌) = ((1st ‘𝐺)‘𝑌)
45	1, 2, 38, 35, 39, 6, 30, 44, 29	curf11 18248	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧) = (𝑌(1st ‘𝐹)𝑧))
46		df-ov 7393	. . . . . . . 8 ⊢ (𝑌(1st ‘𝐹)𝑧) = ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)
47	45, 46	eqtrdi 2812	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧) = ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩))
48	43, 47	oveq12d 7408	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)) = (((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
49	37, 48	eleqtrrd 2864	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)))
50	49	ralrimiva 3153	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)))
51	6	fvexi 6875	. . . . 5 ⊢ 𝐵 ∈ V
52		mptelixpg 8910	. . . . 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 236	. . 3 ⊢ (𝜑 → (𝑧 ∈ 𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧))) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)))
55	13, 54	eqeltrd 2861	. 2 ⊢ (𝜑 → 𝐿 ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)))
56		eqid 2761	. . . . . . . . . 10 ⊢ (Id‘𝐶) = (Id‘𝐶)
57	3	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐶 ∈ Cat)
58	9	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑋 ∈ 𝐴)
59		eqid 2761	. . . . . . . . . 10 ⊢ (comp‘𝐶) = (comp‘𝐶)
60	10	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑌 ∈ 𝐴)
61	11	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐾 ∈ (𝑋𝐻𝑌))
62	2, 7, 56, 57, 58, 59, 60, 61	catrid 17706	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) = 𝐾)
63	2, 7, 56, 57, 58, 59, 60, 61	catlid 17705	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾) = 𝐾)
64	62, 63	eqtr4d 2799	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) = (((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾))
65	4	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐷 ∈ Cat)
66		simpr1 1207	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑧 ∈ 𝐵)
67		eqid 2761	. . . . . . . . . 10 ⊢ (comp‘𝐷) = (comp‘𝐷)
68		simpr2 1208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑤 ∈ 𝐵)
69		simpr3 1209	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))
70	6, 27, 8, 65, 66, 67, 68, 69	catlid 17705	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓) = 𝑓)
71	6, 27, 8, 65, 66, 67, 68, 69	catrid 17706	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧)) = 𝑓)
72	70, 71	eqtr4d 2799	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓) = (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧)))
73	64, 72	opeq12d 4836	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨(𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)), ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓)⟩ = ⟨(((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾), (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧))⟩)
74		eqid 2761	. . . . . . . 8 ⊢ (comp‘(𝐶 ×c 𝐷)) = (comp‘(𝐶 ×c 𝐷))
75	2, 7, 56, 57, 58	catidcl 17704	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑋) ∈ (𝑋𝐻𝑋))
76	6, 27, 8, 65, 68	catidcl 17704	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐼‘𝑤) ∈ (𝑤(Hom ‘𝐷)𝑤))
77	14, 2, 6, 7, 27, 58, 66, 58, 68, 59, 67, 74, 60, 68, 75, 69, 61, 76	xpcco2 18209	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩) = ⟨(𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)), ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓)⟩)
78	36	3ad2antr1 1201	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐼‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧))
79	2, 7, 56, 57, 60	catidcl 17704	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑌) ∈ (𝑌𝐻𝑌))
80	14, 2, 6, 7, 27, 58, 66, 60, 66, 59, 67, 74, 60, 68, 61, 78, 79, 69	xpcco2 18209	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩) = ⟨(((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾), (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧))⟩)
81	73, 77, 80	3eqtr4d 2806	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩) = (⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩))
82	81	fveq2d 6865	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩)))
83		eqid 2761	. . . . . 6 ⊢ (comp‘𝐸) = (comp‘𝐸)
84	20	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
85	23	3ad2antr1 1201	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
86	58, 68	opelxpd 5682	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑤⟩ ∈ (𝐴 × 𝐵))
87	60, 68	opelxpd 5682	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑌, 𝑤⟩ ∈ (𝐴 × 𝐵))
88	75, 69	opelxpd 5682	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑓⟩ ∈ ((𝑋𝐻𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
89	14, 2, 6, 7, 27, 58, 66, 58, 68, 16	xpchom2 18208	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩) = ((𝑋𝐻𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
90	88, 89	eleqtrrd 2864	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑓⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩))
91	61, 76	opelxpd 5682	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑤)⟩ ∈ ((𝑋𝐻𝑌) × (𝑤(Hom ‘𝐷)𝑤)))
92	14, 2, 6, 7, 27, 58, 68, 60, 68, 16	xpchom2 18208	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑤⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩) = ((𝑋𝐻𝑌) × (𝑤(Hom ‘𝐷)𝑤)))
93	91, 92	eleqtrrd 2864	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑤)⟩ ∈ (⟨𝑋, 𝑤⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩))
94	15, 16, 74, 83, 84, 85, 86, 87, 90, 93	funcco 17894	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = (((⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)))
95	25	3ad2antr1 1201	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
96	61, 78	opelxpd 5682	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑧)⟩ ∈ ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
97	14, 2, 6, 7, 27, 58, 66, 60, 66, 16	xpchom2 18208	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩) = ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
98	96, 97	eleqtrrd 2864	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑧)⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩))
99	79, 69	opelxpd 5682	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑌), 𝑓⟩ ∈ ((𝑌𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑤)))
100	14, 2, 6, 7, 27, 60, 66, 60, 68, 16	xpchom2 18208	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑌, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩) = ((𝑌𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑤)))
101	99, 100	eleqtrrd 2864	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑌), 𝑓⟩ ∈ (⟨𝑌, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩))
102	15, 16, 74, 83, 84, 85, 95, 87, 98, 101	funcco 17894	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩)) = (((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)))
103	82, 94, 102	3eqtr3d 2804	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = (((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)))
104	5	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
105	1, 2, 57, 65, 104, 6, 58, 40, 66	curf11 18248	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧) = (𝑋(1st ‘𝐹)𝑧))
106	105, 42	eqtrdi 2812	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩))
107	1, 2, 57, 65, 104, 6, 58, 40, 68	curf11 18248	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤) = (𝑋(1st ‘𝐹)𝑤))
108		df-ov 7393	. . . . . . . 8 ⊢ (𝑋(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)
109	107, 108	eqtrdi 2812	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤) = ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))
110	106, 109	opeq12d 4836	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤)⟩ = ⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩)
111	1, 2, 57, 65, 104, 6, 60, 44, 68	curf11 18248	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤) = (𝑌(1st ‘𝐹)𝑤))
112		df-ov 7393	. . . . . . 7 ⊢ (𝑌(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘⟨𝑌, 𝑤⟩)
113	111, 112	eqtrdi 2812	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤) = ((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))
114	110, 113	oveq12d 7408	. . . . 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 18252	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑤) = (𝐾(⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)(𝐼‘𝑤)))
116		df-ov 7393	. . . . . 6 ⊢ (𝐾(⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)(𝐼‘𝑤)) = ((⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩)
117	115, 116	eqtrdi 2812	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑤) = ((⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩))
118	1, 2, 57, 65, 104, 6, 58, 40, 66, 27, 56, 68, 69	curf12 18249	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st ‘𝐺)‘𝑋))𝑤)‘𝑓) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)𝑓))
119		df-ov 7393	. . . . . 6 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)𝑓) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)
120	118, 119	eqtrdi 2812	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st ‘𝐺)‘𝑋))𝑤)‘𝑓) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩))
121	114, 117, 120	oveq123d 7411	. . . 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 18248	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧) = (𝑌(1st ‘𝐹)𝑧))
123	122, 46	eqtrdi 2812	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧) = ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩))
124	106, 123	opeq12d 4836	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)⟩ = ⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩)
125	124, 113	oveq12d 7408	. . . . 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 18249	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓) = (((Id‘𝐶)‘𝑌)(⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)𝑓))
127		df-ov 7393	. . . . . 6 ⊢ (((Id‘𝐶)‘𝑌)(⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)𝑓) = ((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)
128	126, 127	eqtrdi 2812	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓) = ((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩))
129	1, 2, 57, 65, 104, 6, 7, 8, 58, 60, 61, 12, 66	curf2val 18252	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑧) = (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)))
130		df-ov 7393	. . . . . 6 ⊢ (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)
131	129, 130	eqtrdi 2812	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑧) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩))
132	125, 128, 131	oveq123d 7411	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧)) = (((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)))
133	103, 121, 132	3eqtr4d 2806	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐿‘𝑤)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))((𝑧(2nd ‘((1st ‘𝐺)‘𝑋))𝑤)‘𝑓)) = (((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧)))
134	133	ralrimivvva 3207	. 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 18250	. . 3 ⊢ (𝜑 → ((1st ‘𝐺)‘𝑋) ∈ (𝐷 Func 𝐸))
137	1, 2, 3, 4, 5, 6, 10, 44	curf1cl 18250	. . 3 ⊢ (𝜑 → ((1st ‘𝐺)‘𝑌) ∈ (𝐷 Func 𝐸))
138	135, 6, 27, 17, 83, 136, 137	isnat2 17974	. 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 723	1 ⊢ (𝜑 → 𝐿 ∈ (((1st ‘𝐺)‘𝑋)𝑁((1st ‘𝐺)‘𝑌)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141  ∀wral 3075  Vcvv 3453  ⟨cop 4585   class class class wbr 5097   ↦ cmpt 5178   × cxp 5641  Rel wrel 5648  ⟶wf 6511  ‘cfv 6515  (class class class)co 7390  1^st c1st 7962  2^nd c2nd 7963  Xcixp 8872  Basecbs 17235  Hom chom 17287  compcco 17288  Catccat 17686  Idccid 17687   Func cfunc 17877   Nat cnat 17967   ×_c cxpc 18190   curry_F ccurf 18232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5224  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-cnex 11122  ax-resscn 11123  ax-1cn 11124  ax-icn 11125  ax-addcl 11126  ax-addrcl 11127  ax-mulcl 11128  ax-mulrcl 11129  ax-mulcom 11130  ax-addass 11131  ax-mulass 11132  ax-distr 11133  ax-i2m1 11134  ax-1ne0 11135  ax-1rid 11136  ax-rnegex 11137  ax-rrecex 11138  ax-cnre 11139  ax-pre-lttri 11140  ax-pre-lttrn 11141  ax-pre-ltadd 11142  ax-pre-mulgt0 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-tp 4584  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6282  df-ord 6343  df-on 6344  df-lim 6345  df-suc 6346  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7841  df-1st 7964  df-2nd 7965  df-frecs 8255  df-wrecs 8286  df-recs 8335  df-rdg 8374  df-1o 8430  df-er 8671  df-map 8803  df-ixp 8873  df-en 8921  df-dom 8922  df-sdom 8923  df-fin 8924  df-pnf 11211  df-mnf 11212  df-xr 11213  df-ltxr 11214  df-le 11215  df-sub 11409  df-neg 11410  df-nn 12204  df-2 12273  df-3 12274  df-4 12275  df-5 12276  df-6 12277  df-7 12278  df-8 12279  df-9 12280  df-n0 12475  df-z 12562  df-dec 12682  df-uz 12833  df-fz 13506  df-struct 17173  df-slot 17208  df-ndx 17220  df-base 17236  df-hom 17300  df-cco 17301  df-cat 17690  df-cid 17691  df-func 17881  df-nat 17969  df-xpc 18194  df-curf 18236

This theorem is referenced by:  curfcl  18254  tposcurf2cl  49883