Theorem curf2cl 18241

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 18239	. . 3 ⊢ (𝜑 → 𝐿 = (𝑧 ∈ 𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧))))
14		eqid 2735	. . . . . . . . . 10 ⊢ (𝐶 ×c 𝐷) = (𝐶 ×c 𝐷)
15	14, 2, 6	xpcbas 18188	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷))
16		eqid 2735	. . . . . . . . 9 ⊢ (Hom ‘(𝐶 ×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷))
17		eqid 2735	. . . . . . . . 9 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
18		relfunc 17873	. . . . . . . . . . 11 ⊢ Rel ((𝐶 ×c 𝐷) Func 𝐸)
19		1st2ndbr 8039	. . . . . . . . . . 11 ⊢ ((Rel ((𝐶 ×c 𝐷) Func 𝐸) ∧ 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
20	18, 5, 19	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
21	20	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
22		opelxpi 5691	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
23	9, 22	sylan 580	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
24		opelxpi 5691	. . . . . . . . . 10 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
25	10, 24	sylan 580	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
26	15, 16, 17, 21, 23, 25	funcf2 17879	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩):(⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩)⟶(((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
27		eqid 2735	. . . . . . . . . 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 18196	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩) = ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
32	31	feq2d 6691	. . . . . . . 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 17692	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐼‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧))
37	33, 34, 36	fovcdmd 7577	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
38	3	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐶 ∈ Cat)
39	5	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
40		eqid 2735	. . . . . . . . 9 ⊢ ((1st ‘𝐺)‘𝑋) = ((1st ‘𝐺)‘𝑋)
41	1, 2, 38, 35, 39, 6, 28, 40, 29	curf11 18236	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧) = (𝑋(1st ‘𝐹)𝑧))
42		df-ov 7406	. . . . . . . 8 ⊢ (𝑋(1st ‘𝐹)𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)
43	41, 42	eqtrdi 2786	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩))
44		eqid 2735	. . . . . . . . 9 ⊢ ((1st ‘𝐺)‘𝑌) = ((1st ‘𝐺)‘𝑌)
45	1, 2, 38, 35, 39, 6, 30, 44, 29	curf11 18236	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧) = (𝑌(1st ‘𝐹)𝑧))
46		df-ov 7406	. . . . . . . 8 ⊢ (𝑌(1st ‘𝐹)𝑧) = ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)
47	45, 46	eqtrdi 2786	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧) = ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩))
48	43, 47	oveq12d 7421	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)) = (((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
49	37, 48	eleqtrrd 2837	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)))
50	49	ralrimiva 3132	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)))
51	6	fvexi 6889	. . . . 5 ⊢ 𝐵 ∈ V
52		mptelixpg 8947	. . . . 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 2834	. 2 ⊢ (𝜑 → 𝐿 ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)))
56		eqid 2735	. . . . . . . . . 10 ⊢ (Id‘𝐶) = (Id‘𝐶)
57	3	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐶 ∈ Cat)
58	9	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑋 ∈ 𝐴)
59		eqid 2735	. . . . . . . . . 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 17694	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) = 𝐾)
63	2, 7, 56, 57, 58, 59, 60, 61	catlid 17693	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾) = 𝐾)
64	62, 63	eqtr4d 2773	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) = (((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾))
65	4	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐷 ∈ Cat)
66		simpr1 1195	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑧 ∈ 𝐵)
67		eqid 2735	. . . . . . . . . 10 ⊢ (comp‘𝐷) = (comp‘𝐷)
68		simpr2 1196	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑤 ∈ 𝐵)
69		simpr3 1197	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))
70	6, 27, 8, 65, 66, 67, 68, 69	catlid 17693	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓) = 𝑓)
71	6, 27, 8, 65, 66, 67, 68, 69	catrid 17694	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧)) = 𝑓)
72	70, 71	eqtr4d 2773	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓) = (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧)))
73	64, 72	opeq12d 4857	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨(𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)), ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓)⟩ = ⟨(((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾), (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧))⟩)
74		eqid 2735	. . . . . . . 8 ⊢ (comp‘(𝐶 ×c 𝐷)) = (comp‘(𝐶 ×c 𝐷))
75	2, 7, 56, 57, 58	catidcl 17692	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑋) ∈ (𝑋𝐻𝑋))
76	6, 27, 8, 65, 68	catidcl 17692	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐼‘𝑤) ∈ (𝑤(Hom ‘𝐷)𝑤))
77	14, 2, 6, 7, 27, 58, 66, 58, 68, 59, 67, 74, 60, 68, 75, 69, 61, 76	xpcco2 18197	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩) = ⟨(𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)), ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓)⟩)
78	36	3ad2antr1 1189	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐼‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧))
79	2, 7, 56, 57, 60	catidcl 17692	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑌) ∈ (𝑌𝐻𝑌))
80	14, 2, 6, 7, 27, 58, 66, 60, 66, 59, 67, 74, 60, 68, 61, 78, 79, 69	xpcco2 18197	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩) = ⟨(((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾), (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧))⟩)
81	73, 77, 80	3eqtr4d 2780	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩) = (⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩))
82	81	fveq2d 6879	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩)))
83		eqid 2735	. . . . . 6 ⊢ (comp‘𝐸) = (comp‘𝐸)
84	20	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
85	23	3ad2antr1 1189	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
86	58, 68	opelxpd 5693	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑤⟩ ∈ (𝐴 × 𝐵))
87	60, 68	opelxpd 5693	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑌, 𝑤⟩ ∈ (𝐴 × 𝐵))
88	75, 69	opelxpd 5693	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑓⟩ ∈ ((𝑋𝐻𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
89	14, 2, 6, 7, 27, 58, 66, 58, 68, 16	xpchom2 18196	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩) = ((𝑋𝐻𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
90	88, 89	eleqtrrd 2837	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑓⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩))
91	61, 76	opelxpd 5693	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑤)⟩ ∈ ((𝑋𝐻𝑌) × (𝑤(Hom ‘𝐷)𝑤)))
92	14, 2, 6, 7, 27, 58, 68, 60, 68, 16	xpchom2 18196	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑤⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩) = ((𝑋𝐻𝑌) × (𝑤(Hom ‘𝐷)𝑤)))
93	91, 92	eleqtrrd 2837	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑤)⟩ ∈ (⟨𝑋, 𝑤⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩))
94	15, 16, 74, 83, 84, 85, 86, 87, 90, 93	funcco 17882	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = (((⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)))
95	25	3ad2antr1 1189	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
96	61, 78	opelxpd 5693	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑧)⟩ ∈ ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
97	14, 2, 6, 7, 27, 58, 66, 60, 66, 16	xpchom2 18196	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩) = ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
98	96, 97	eleqtrrd 2837	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑧)⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩))
99	79, 69	opelxpd 5693	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑌), 𝑓⟩ ∈ ((𝑌𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑤)))
100	14, 2, 6, 7, 27, 60, 66, 60, 68, 16	xpchom2 18196	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑌, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩) = ((𝑌𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑤)))
101	99, 100	eleqtrrd 2837	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑌), 𝑓⟩ ∈ (⟨𝑌, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩))
102	15, 16, 74, 83, 84, 85, 95, 87, 98, 101	funcco 17882	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩)) = (((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)))
103	82, 94, 102	3eqtr3d 2778	. . . 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 18236	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧) = (𝑋(1st ‘𝐹)𝑧))
106	105, 42	eqtrdi 2786	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩))
107	1, 2, 57, 65, 104, 6, 58, 40, 68	curf11 18236	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤) = (𝑋(1st ‘𝐹)𝑤))
108		df-ov 7406	. . . . . . . 8 ⊢ (𝑋(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)
109	107, 108	eqtrdi 2786	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤) = ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))
110	106, 109	opeq12d 4857	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤)⟩ = ⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩)
111	1, 2, 57, 65, 104, 6, 60, 44, 68	curf11 18236	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤) = (𝑌(1st ‘𝐹)𝑤))
112		df-ov 7406	. . . . . . 7 ⊢ (𝑌(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘⟨𝑌, 𝑤⟩)
113	111, 112	eqtrdi 2786	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤) = ((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))
114	110, 113	oveq12d 7421	. . . . 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 18240	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑤) = (𝐾(⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)(𝐼‘𝑤)))
116		df-ov 7406	. . . . . 6 ⊢ (𝐾(⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)(𝐼‘𝑤)) = ((⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩)
117	115, 116	eqtrdi 2786	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑤) = ((⟨𝑋, 𝑤⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩))
118	1, 2, 57, 65, 104, 6, 58, 40, 66, 27, 56, 68, 69	curf12 18237	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st ‘𝐺)‘𝑋))𝑤)‘𝑓) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)𝑓))
119		df-ov 7406	. . . . . 6 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)𝑓) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)
120	118, 119	eqtrdi 2786	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st ‘𝐺)‘𝑋))𝑤)‘𝑓) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩))
121	114, 117, 120	oveq123d 7424	. . . 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 18236	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧) = (𝑌(1st ‘𝐹)𝑧))
123	122, 46	eqtrdi 2786	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧) = ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩))
124	106, 123	opeq12d 4857	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)⟩ = ⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩)
125	124, 113	oveq12d 7421	. . . . 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 18237	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓) = (((Id‘𝐶)‘𝑌)(⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)𝑓))
127		df-ov 7406	. . . . . 6 ⊢ (((Id‘𝐶)‘𝑌)(⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)𝑓) = ((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)
128	126, 127	eqtrdi 2786	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓) = ((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩))
129	1, 2, 57, 65, 104, 6, 7, 8, 58, 60, 61, 12, 66	curf2val 18240	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑧) = (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)))
130		df-ov 7406	. . . . . 6 ⊢ (𝐾(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)
131	129, 130	eqtrdi 2786	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑧) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩))
132	125, 128, 131	oveq123d 7424	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧)) = (((⟨𝑌, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)))
133	103, 121, 132	3eqtr4d 2780	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐿‘𝑤)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))((𝑧(2nd ‘((1st ‘𝐺)‘𝑋))𝑤)‘𝑓)) = (((𝑧(2nd ‘((1st ‘𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1st ‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st ‘𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1st ‘((1st ‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧)))
134	133	ralrimivvva 3190	. 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 18238	. . 3 ⊢ (𝜑 → ((1st ‘𝐺)‘𝑋) ∈ (𝐷 Func 𝐸))
137	1, 2, 3, 4, 5, 6, 10, 44	curf1cl 18238	. . 3 ⊢ (𝜑 → ((1st ‘𝐺)‘𝑌) ∈ (𝐷 Func 𝐸))
138	135, 6, 27, 17, 83, 136, 137	isnat2 17962	. 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 713	1 ⊢ (𝜑 → 𝐿 ∈ (((1st ‘𝐺)‘𝑋)𝑁((1st ‘𝐺)‘𝑌)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108  ∀wral 3051  Vcvv 3459  ⟨cop 4607   class class class wbr 5119   ↦ cmpt 5201   × cxp 5652  Rel wrel 5659  ⟶wf 6526  ‘cfv 6530  (class class class)co 7403  1^st c1st 7984  2^nd c2nd 7985  Xcixp 8909  Basecbs 17226  Hom chom 17280  compcco 17281  Catccat 17674  Idccid 17675   Func cfunc 17865   Nat cnat 17955   ×_c cxpc 18178   curry_F ccurf 18220

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-tp 4606  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-om 7860  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-er 8717  df-map 8840  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-nn 12239  df-2 12301  df-3 12302  df-4 12303  df-5 12304  df-6 12305  df-7 12306  df-8 12307  df-9 12308  df-n0 12500  df-z 12587  df-dec 12707  df-uz 12851  df-fz 13523  df-struct 17164  df-slot 17199  df-ndx 17211  df-base 17227  df-hom 17293  df-cco 17294  df-cat 17678  df-cid 17679  df-func 17869  df-nat 17957  df-xpc 18182  df-curf 18224

This theorem is referenced by:  curfcl  18242  tposcurf2cl  49161