Theorem curf2cl 18188

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 18186	. . 3 ⊢ (𝜑 → 𝐿 = (𝑧 ∈ 𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧))))
14		eqid 2737	. . . . . . . . . 10 ⊢ (𝐶 ×c 𝐷) = (𝐶 ×c 𝐷)
15	14, 2, 6	xpcbas 18135	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷))
16		eqid 2737	. . . . . . . . 9 ⊢ (Hom ‘(𝐶 ×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷))
17		eqid 2737	. . . . . . . . 9 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
18		relfunc 17820	. . . . . . . . . . 11 ⊢ Rel ((𝐶 ×c 𝐷) Func 𝐸)
19		1st2ndbr 7988	. . . . . . . . . . 11 ⊢ ((Rel ((𝐶 ×c 𝐷) Func 𝐸) ∧ 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
20	18, 5, 19	sylancr 588	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
21	20	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
22		opelxpi 5661	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
23	9, 22	sylan 581	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
24		opelxpi 5661	. . . . . . . . . 10 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
25	10, 24	sylan 581	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
26	15, 16, 17, 21, 23, 25	funcf2 17826	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩):(⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩)⟶(((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
27		eqid 2737	. . . . . . . . . 10 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
28	9	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑋 ∈ 𝐴)
29		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵)
30	10	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑌 ∈ 𝐴)
31	14, 2, 6, 7, 27, 28, 29, 30, 29, 16	xpchom2 18143	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩) = ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
32	31	feq2d 6646	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩):(⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩)⟶(((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)) ↔ (⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩):((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧))⟶(((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩))))
33	26, 32	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩):((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧))⟶(((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
34	11	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐾 ∈ (𝑋𝐻𝑌))
35	4	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐷 ∈ Cat)
36	6, 27, 8, 35, 29	catidcl 17639	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐼‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧))
37	33, 34, 36	fovcdmd 7532	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
38	3	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐶 ∈ Cat)
39	5	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
40		eqid 2737	. . . . . . . . 9 ⊢ ((1st ‘𝐺)‘𝑋) = ((1st ‘𝐺)‘𝑋)
41	1, 2, 38, 35, 39, 6, 28, 40, 29	curf11 18183	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧) = (𝑋(1st ‘𝐹)𝑧))
42		df-ov 7363	. . . . . . . 8 ⊢ (𝑋(1st ‘𝐹)𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)
43	41, 42	eqtrdi 2788	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩))
44		eqid 2737	. . . . . . . . 9 ⊢ ((1st ‘𝐺)‘𝑌) = ((1st ‘𝐺)‘𝑌)
45	1, 2, 38, 35, 39, 6, 30, 44, 29	curf11 18183	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧) = (𝑌(1st ‘𝐹)𝑧))
46		df-ov 7363	. . . . . . . 8 ⊢ (𝑌(1st ‘𝐹)𝑧) = ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)
47	45, 46	eqtrdi 2788	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧) = ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩))
48	43, 47	oveq12d 7378	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)) = (((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
49	37, 48	eleqtrrd 2840	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)))
50	49	ralrimiva 3130	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)))
51	6	fvexi 6848	. . . . 5 ⊢ 𝐵 ∈ V
52		mptelixpg 8876	. . . . 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 234	. . 3 ⊢ (𝜑 → (𝑧 ∈ 𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧))) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)))
55	13, 54	eqeltrd 2837	. 2 ⊢ (𝜑 → 𝐿 ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)))
56		eqid 2737	. . . . . . . . . 10 ⊢ (Id‘𝐶) = (Id‘𝐶)
57	3	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐶 ∈ Cat)
58	9	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑋 ∈ 𝐴)
59		eqid 2737	. . . . . . . . . 10 ⊢ (comp‘𝐶) = (comp‘𝐶)
60	10	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑌 ∈ 𝐴)
61	11	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐾 ∈ (𝑋𝐻𝑌))
62	2, 7, 56, 57, 58, 59, 60, 61	catrid 17641	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) = 𝐾)
63	2, 7, 56, 57, 58, 59, 60, 61	catlid 17640	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾) = 𝐾)
64	62, 63	eqtr4d 2775	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) = (((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾))
65	4	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐷 ∈ Cat)
66		simpr1 1196	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑧 ∈ 𝐵)
67		eqid 2737	. . . . . . . . . 10 ⊢ (comp‘𝐷) = (comp‘𝐷)
68		simpr2 1197	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑤 ∈ 𝐵)
69		simpr3 1198	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))
70	6, 27, 8, 65, 66, 67, 68, 69	catlid 17640	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓) = 𝑓)
71	6, 27, 8, 65, 66, 67, 68, 69	catrid 17641	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧)) = 𝑓)
72	70, 71	eqtr4d 2775	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓) = (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧)))
73	64, 72	opeq12d 4825	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨(𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)), ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓)⟩ = ⟨(((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾), (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧))⟩)
74		eqid 2737	. . . . . . . 8 ⊢ (comp‘(𝐶 ×c 𝐷)) = (comp‘(𝐶 ×c 𝐷))
75	2, 7, 56, 57, 58	catidcl 17639	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑋) ∈ (𝑋𝐻𝑋))
76	6, 27, 8, 65, 68	catidcl 17639	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐼‘𝑤) ∈ (𝑤(Hom ‘𝐷)𝑤))
77	14, 2, 6, 7, 27, 58, 66, 58, 68, 59, 67, 74, 60, 68, 75, 69, 61, 76	xpcco2 18144	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩) = ⟨(𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)), ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓)⟩)
78	36	3ad2antr1 1190	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐼‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧))
79	2, 7, 56, 57, 60	catidcl 17639	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑌) ∈ (𝑌𝐻𝑌))
80	14, 2, 6, 7, 27, 58, 66, 60, 66, 59, 67, 74, 60, 68, 61, 78, 79, 69	xpcco2 18144	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩) = ⟨(((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾), (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧))⟩)
81	73, 77, 80	3eqtr4d 2782	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩) = (⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩))
82	81	fveq2d 6838	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩)))
83		eqid 2737	. . . . . 6 ⊢ (comp‘𝐸) = (comp‘𝐸)
84	20	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
85	23	3ad2antr1 1190	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
86	58, 68	opelxpd 5663	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑤⟩ ∈ (𝐴 × 𝐵))
87	60, 68	opelxpd 5663	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑌, 𝑤⟩ ∈ (𝐴 × 𝐵))
88	75, 69	opelxpd 5663	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑓⟩ ∈ ((𝑋𝐻𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
89	14, 2, 6, 7, 27, 58, 66, 58, 68, 16	xpchom2 18143	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩) = ((𝑋𝐻𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
90	88, 89	eleqtrrd 2840	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑓⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩))
91	61, 76	opelxpd 5663	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑤)⟩ ∈ ((𝑋𝐻𝑌) × (𝑤(Hom ‘𝐷)𝑤)))
92	14, 2, 6, 7, 27, 58, 68, 60, 68, 16	xpchom2 18143	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑤⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩) = ((𝑋𝐻𝑌) × (𝑤(Hom ‘𝐷)𝑤)))
93	91, 92	eleqtrrd 2840	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑤)⟩ ∈ (⟨𝑋, 𝑤⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩))
94	15, 16, 74, 83, 84, 85, 86, 87, 90, 93	funcco 17829	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = (((⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)))
95	25	3ad2antr1 1190	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
96	61, 78	opelxpd 5663	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑧)⟩ ∈ ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
97	14, 2, 6, 7, 27, 58, 66, 60, 66, 16	xpchom2 18143	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩) = ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
98	96, 97	eleqtrrd 2840	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑧)⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩))
99	79, 69	opelxpd 5663	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑌), 𝑓⟩ ∈ ((𝑌𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑤)))
100	14, 2, 6, 7, 27, 60, 66, 60, 68, 16	xpchom2 18143	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑌, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩) = ((𝑌𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑤)))
101	99, 100	eleqtrrd 2840	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑌), 𝑓⟩ ∈ (⟨𝑌, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩))
102	15, 16, 74, 83, 84, 85, 95, 87, 98, 101	funcco 17829	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩)) = (((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)))
103	82, 94, 102	3eqtr3d 2780	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = (((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)))
104	5	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
105	1, 2, 57, 65, 104, 6, 58, 40, 66	curf11 18183	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧) = (𝑋(1st ‘𝐹)𝑧))
106	105, 42	eqtrdi 2788	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩))
107	1, 2, 57, 65, 104, 6, 58, 40, 68	curf11 18183	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤) = (𝑋(1st ‘𝐹)𝑤))
108		df-ov 7363	. . . . . . . 8 ⊢ (𝑋(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)
109	107, 108	eqtrdi 2788	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤) = ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))
110	106, 109	opeq12d 4825	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤)⟩ = ⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩)
111	1, 2, 57, 65, 104, 6, 60, 44, 68	curf11 18183	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤) = (𝑌(1st ‘𝐹)𝑤))
112		df-ov 7363	. . . . . . 7 ⊢ (𝑌(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘⟨𝑌, 𝑤⟩)
113	111, 112	eqtrdi 2788	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤) = ((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))
114	110, 113	oveq12d 7378	. . . . 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 18187	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑤) = (𝐾(⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)(𝐼‘𝑤)))
116		df-ov 7363	. . . . . 6 ⊢ (𝐾(⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)(𝐼‘𝑤)) = ((⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩)
117	115, 116	eqtrdi 2788	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑤) = ((⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩))
118	1, 2, 57, 65, 104, 6, 58, 40, 66, 27, 56, 68, 69	curf12 18184	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st ‘𝐺)‘𝑋))𝑤)‘𝑓) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)𝑓))
119		df-ov 7363	. . . . . 6 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)𝑓) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)
120	118, 119	eqtrdi 2788	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st ‘𝐺)‘𝑋))𝑤)‘𝑓) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩))
121	114, 117, 120	oveq123d 7381	. . . 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 18183	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧) = (𝑌(1st ‘𝐹)𝑧))
123	122, 46	eqtrdi 2788	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧) = ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩))
124	106, 123	opeq12d 4825	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)⟩ = ⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩)
125	124, 113	oveq12d 7378	. . . . 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 18184	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓) = (((Id‘𝐶)‘𝑌)(⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)𝑓))
127		df-ov 7363	. . . . . 6 ⊢ (((Id‘𝐶)‘𝑌)(⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)𝑓) = ((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)
128	126, 127	eqtrdi 2788	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓) = ((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩))
129	1, 2, 57, 65, 104, 6, 7, 8, 58, 60, 61, 12, 66	curf2val 18187	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑧) = (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)))
130		df-ov 7363	. . . . . 6 ⊢ (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)
131	129, 130	eqtrdi 2788	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑧) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩))
132	125, 128, 131	oveq123d 7381	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧)) = (((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)))
133	103, 121, 132	3eqtr4d 2782	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐿‘𝑤)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))((𝑧(2nd ‘((1st ‘𝐺)‘𝑋))𝑤)‘𝑓)) = (((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧)))
134	133	ralrimivvva 3184	. 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 18185	. . 3 ⊢ (𝜑 → ((1st ‘𝐺)‘𝑋) ∈ (𝐷 Func 𝐸))
137	1, 2, 3, 4, 5, 6, 10, 44	curf1cl 18185	. . 3 ⊢ (𝜑 → ((1st ‘𝐺)‘𝑌) ∈ (𝐷 Func 𝐸))
138	135, 6, 27, 17, 83, 136, 137	isnat2 17909	. 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 714	1 ⊢ (𝜑 → 𝐿 ∈ (((1st ‘𝐺)‘𝑋)𝑁((1st ‘𝐺)‘𝑌)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3052  Vcvv 3430  ⟨cop 4574   class class class wbr 5086   ↦ cmpt 5167   × cxp 5622  Rel wrel 5629  ⟶wf 6488  ‘cfv 6492  (class class class)co 7360  1^st c1st 7933  2^nd c2nd 7934  Xcixp 8838  Basecbs 17170  Hom chom 17222  compcco 17223  Catccat 17621  Idccid 17622   Func cfunc 17812   Nat cnat 17902   ×_c cxpc 18125   curry_F ccurf 18167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-1o 8398  df-er 8636  df-map 8768  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241  df-9 12242  df-n0 12429  df-z 12516  df-dec 12636  df-uz 12780  df-fz 13453  df-struct 17108  df-slot 17143  df-ndx 17155  df-base 17171  df-hom 17235  df-cco 17236  df-cat 17625  df-cid 17626  df-func 17816  df-nat 17904  df-xpc 18129  df-curf 18171

This theorem is referenced by:  curfcl  18189  tposcurf2cl  49789