curf2cl - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > curf2cl		Structured version Visualization version GIF version

Theorem curf2cl 17865

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

**Hypotheses**
Ref	Expression
curf2.g	⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curry_F 𝐹)
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	⊢ 𝐿 = ((𝑋(2^nd ‘𝐺)𝑌)‘𝐾)
curf2.n	⊢ 𝑁 = (𝐷 Nat 𝐸)

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

Proof of Theorem curf2cl Dummy variables 𝑧 𝑤 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		curf2.g	. . . 4 ⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curry_F 𝐹)
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 ⊢ 𝐿 = ((𝑋(2^nd ‘𝐺)𝑌)‘𝐾)
13	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	curf2 17863	. . 3 ⊢ (𝜑 → 𝐿 = (𝑧 ∈ 𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧))))
14		eqid 2738	. . . . . . . . . 10 ⊢ (𝐶 ×_c 𝐷) = (𝐶 ×_c 𝐷)
15	14, 2, 6	xpcbas 17811	. . . . . . . . 9 ⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×_c 𝐷))
16		eqid 2738	. . . . . . . . 9 ⊢ (Hom ‘(𝐶 ×_c 𝐷)) = (Hom ‘(𝐶 ×_c 𝐷))
17		eqid 2738	. . . . . . . . 9 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
18		relfunc 17493	. . . . . . . . . . 11 ⊢ Rel ((𝐶 ×_c 𝐷) Func 𝐸)
19		1st2ndbr 7856	. . . . . . . . . . 11 ⊢ ((Rel ((𝐶 ×_c 𝐷) Func 𝐸) ∧ 𝐹 ∈ ((𝐶 ×_c 𝐷) Func 𝐸)) → (1^st ‘𝐹)((𝐶 ×_c 𝐷) Func 𝐸)(2^nd ‘𝐹))
20	18, 5, 19	sylancr 586	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘𝐹)((𝐶 ×_c 𝐷) Func 𝐸)(2^nd ‘𝐹))
21	20	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (1^st ‘𝐹)((𝐶 ×_c 𝐷) Func 𝐸)(2^nd ‘𝐹))
22		opelxpi 5617	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
23	9, 22	sylan 579	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
24		opelxpi 5617	. . . . . . . . . 10 ⊢ ((𝑌 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
25	10, 24	sylan 579	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
26	15, 16, 17, 21, 23, 25	funcf2 17499	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩):(⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑧⟩)⟶(((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1^st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
27		eqid 2738	. . . . . . . . . 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 17819	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑧⟩) = ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
32	31	feq2d 6570	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩):(⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑧⟩)⟶(((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1^st ‘𝐹)‘⟨𝑌, 𝑧⟩)) ↔ (⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩):((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧))⟶(((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1^st ‘𝐹)‘⟨𝑌, 𝑧⟩))))
33	26, 32	mpbid 231	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩):((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧))⟶(((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1^st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
34	11	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐾 ∈ (𝑋𝐻𝑌))
35	4	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐷 ∈ Cat)
36	6, 27, 8, 35, 29	catidcl 17308	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐼‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧))
37	33, 34, 36	fovrnd 7422	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐾(⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1^st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
38	3	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐶 ∈ Cat)
39	5	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐹 ∈ ((𝐶 ×_c 𝐷) Func 𝐸))
40		eqid 2738	. . . . . . . . 9 ⊢ ((1^st ‘𝐺)‘𝑋) = ((1^st ‘𝐺)‘𝑋)
41	1, 2, 38, 35, 39, 6, 28, 40, 29	curf11 17860	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧) = (𝑋(1^st ‘𝐹)𝑧))
42		df-ov 7258	. . . . . . . 8 ⊢ (𝑋(1^st ‘𝐹)𝑧) = ((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩)
43	41, 42	eqtrdi 2795	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧) = ((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩))
44		eqid 2738	. . . . . . . . 9 ⊢ ((1^st ‘𝐺)‘𝑌) = ((1^st ‘𝐺)‘𝑌)
45	1, 2, 38, 35, 39, 6, 30, 44, 29	curf11 17860	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧) = (𝑌(1^st ‘𝐹)𝑧))
46		df-ov 7258	. . . . . . . 8 ⊢ (𝑌(1^st ‘𝐹)𝑧) = ((1^st ‘𝐹)‘⟨𝑌, 𝑧⟩)
47	45, 46	eqtrdi 2795	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧) = ((1^st ‘𝐹)‘⟨𝑌, 𝑧⟩))
48	43, 47	oveq12d 7273	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧)) = (((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1^st ‘𝐹)‘⟨𝑌, 𝑧⟩)))
49	37, 48	eleqtrrd 2842	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐾(⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧)))
50	49	ralrimiva 3107	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 (𝐾(⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧)))
51	6	fvexi 6770	. . . . 5 ⊢ 𝐵 ∈ V
52		mptelixpg 8681	. . . . 5 ⊢ (𝐵 ∈ V → ((𝑧 ∈ 𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧))) ∈ X𝑧 ∈ 𝐵 (((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝐾(⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧))))
53	51, 52	ax-mp 5	. . . 4 ⊢ ((𝑧 ∈ 𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧))) ∈ X𝑧 ∈ 𝐵 (((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝐾(⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) ∈ (((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧)))
54	50, 53	sylibr 233	. . 3 ⊢ (𝜑 → (𝑧 ∈ 𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧))) ∈ X𝑧 ∈ 𝐵 (((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧)))
55	13, 54	eqeltrd 2839	. 2 ⊢ (𝜑 → 𝐿 ∈ X𝑧 ∈ 𝐵 (((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧)))
56		eqid 2738	. . . . . . . . . 10 ⊢ (Id‘𝐶) = (Id‘𝐶)
57	3	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐶 ∈ Cat)
58	9	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑋 ∈ 𝐴)
59		eqid 2738	. . . . . . . . . 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 17310	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) = 𝐾)
63	2, 7, 56, 57, 58, 59, 60, 61	catlid 17309	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾) = 𝐾)
64	62, 63	eqtr4d 2781	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) = (((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾))
65	4	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐷 ∈ Cat)
66		simpr1 1192	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑧 ∈ 𝐵)
67		eqid 2738	. . . . . . . . . 10 ⊢ (comp‘𝐷) = (comp‘𝐷)
68		simpr2 1193	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑤 ∈ 𝐵)
69		simpr3 1194	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))
70	6, 27, 8, 65, 66, 67, 68, 69	catlid 17309	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓) = 𝑓)
71	6, 27, 8, 65, 66, 67, 68, 69	catrid 17310	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧)) = 𝑓)
72	70, 71	eqtr4d 2781	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓) = (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧)))
73	64, 72	opeq12d 4809	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨(𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)), ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓)⟩ = ⟨(((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾), (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧))⟩)
74		eqid 2738	. . . . . . . 8 ⊢ (comp‘(𝐶 ×_c 𝐷)) = (comp‘(𝐶 ×_c 𝐷))
75	2, 7, 56, 57, 58	catidcl 17308	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑋) ∈ (𝑋𝐻𝑋))
76	6, 27, 8, 65, 68	catidcl 17308	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐼‘𝑤) ∈ (𝑤(Hom ‘𝐷)𝑤))
77	14, 2, 6, 7, 27, 58, 66, 58, 68, 59, 67, 74, 60, 68, 75, 69, 61, 76	xpcco2 17820	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩) = ⟨(𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)), ((𝐼‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓)⟩)
78	36	3ad2antr1 1186	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐼‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧))
79	2, 7, 56, 57, 60	catidcl 17308	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑌) ∈ (𝑌𝐻𝑌))
80	14, 2, 6, 7, 27, 58, 66, 60, 66, 59, 67, 74, 60, 68, 61, 78, 79, 69	xpcco2 17820	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩) = ⟨(((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾), (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼‘𝑧))⟩)
81	73, 77, 80	3eqtr4d 2788	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩) = (⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩))
82	81	fveq2d 6760	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = ((⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩)))
83		eqid 2738	. . . . . 6 ⊢ (comp‘𝐸) = (comp‘𝐸)
84	20	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (1^st ‘𝐹)((𝐶 ×_c 𝐷) Func 𝐸)(2^nd ‘𝐹))
85	23	3ad2antr1 1186	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
86	58, 68	opelxpd 5618	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑤⟩ ∈ (𝐴 × 𝐵))
87	60, 68	opelxpd 5618	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑌, 𝑤⟩ ∈ (𝐴 × 𝐵))
88	75, 69	opelxpd 5618	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑓⟩ ∈ ((𝑋𝐻𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
89	14, 2, 6, 7, 27, 58, 66, 58, 68, 16	xpchom2 17819	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×_c 𝐷))⟨𝑋, 𝑤⟩) = ((𝑋𝐻𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
90	88, 89	eleqtrrd 2842	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑓⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×_c 𝐷))⟨𝑋, 𝑤⟩))
91	61, 76	opelxpd 5618	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑤)⟩ ∈ ((𝑋𝐻𝑌) × (𝑤(Hom ‘𝐷)𝑤)))
92	14, 2, 6, 7, 27, 58, 68, 60, 68, 16	xpchom2 17819	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑤⟩(Hom ‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑤⟩) = ((𝑋𝐻𝑌) × (𝑤(Hom ‘𝐷)𝑤)))
93	91, 92	eleqtrrd 2842	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑤)⟩ ∈ (⟨𝑋, 𝑤⟩(Hom ‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑤⟩))
94	15, 16, 74, 83, 84, 85, 86, 87, 90, 93	funcco 17502	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨𝐾, (𝐼‘𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = (((⟨𝑋, 𝑤⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩)(⟨((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1^st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1^st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)))
95	25	3ad2antr1 1186	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
96	61, 78	opelxpd 5618	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑧)⟩ ∈ ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
97	14, 2, 6, 7, 27, 58, 66, 60, 66, 16	xpchom2 17819	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑧⟩) = ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
98	96, 97	eleqtrrd 2842	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼‘𝑧)⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑧⟩))
99	79, 69	opelxpd 5618	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑌), 𝑓⟩ ∈ ((𝑌𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑤)))
100	14, 2, 6, 7, 27, 60, 66, 60, 68, 16	xpchom2 17819	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑌, 𝑧⟩(Hom ‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑤⟩) = ((𝑌𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑤)))
101	99, 100	eleqtrrd 2842	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑌), 𝑓⟩ ∈ (⟨𝑌, 𝑧⟩(Hom ‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑤⟩))
102	15, 16, 74, 83, 84, 85, 95, 87, 98, 101	funcco 17502	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×_c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼‘𝑧)⟩)) = (((⟨𝑌, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1^st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1^st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)))
103	82, 94, 102	3eqtr3d 2786	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((⟨𝑋, 𝑤⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩)(⟨((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1^st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1^st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = (((⟨𝑌, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1^st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1^st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)))
104	5	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐹 ∈ ((𝐶 ×_c 𝐷) Func 𝐸))
105	1, 2, 57, 65, 104, 6, 58, 40, 66	curf11 17860	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧) = (𝑋(1^st ‘𝐹)𝑧))
106	105, 42	eqtrdi 2795	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧) = ((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩))
107	1, 2, 57, 65, 104, 6, 58, 40, 68	curf11 17860	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑤) = (𝑋(1^st ‘𝐹)𝑤))
108		df-ov 7258	. . . . . . . 8 ⊢ (𝑋(1^st ‘𝐹)𝑤) = ((1^st ‘𝐹)‘⟨𝑋, 𝑤⟩)
109	107, 108	eqtrdi 2795	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑤) = ((1^st ‘𝐹)‘⟨𝑋, 𝑤⟩))
110	106, 109	opeq12d 4809	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧), ((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑤)⟩ = ⟨((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1^st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩)
111	1, 2, 57, 65, 104, 6, 60, 44, 68	curf11 17860	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑤) = (𝑌(1^st ‘𝐹)𝑤))
112		df-ov 7258	. . . . . . 7 ⊢ (𝑌(1^st ‘𝐹)𝑤) = ((1^st ‘𝐹)‘⟨𝑌, 𝑤⟩)
113	111, 112	eqtrdi 2795	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑤) = ((1^st ‘𝐹)‘⟨𝑌, 𝑤⟩))
114	110, 113	oveq12d 7273	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧), ((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑤)) = (⟨((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1^st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1^st ‘𝐹)‘⟨𝑌, 𝑤⟩)))
115	1, 2, 57, 65, 104, 6, 7, 8, 58, 60, 61, 12, 68	curf2val 17864	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑤) = (𝐾(⟨𝑋, 𝑤⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)(𝐼‘𝑤)))
116		df-ov 7258	. . . . . 6 ⊢ (𝐾(⟨𝑋, 𝑤⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)(𝐼‘𝑤)) = ((⟨𝑋, 𝑤⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩)
117	115, 116	eqtrdi 2795	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑤) = ((⟨𝑋, 𝑤⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩))
118	1, 2, 57, 65, 104, 6, 58, 40, 66, 27, 56, 68, 69	curf12 17861	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2^nd ‘((1^st ‘𝐺)‘𝑋))𝑤)‘𝑓) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑋, 𝑤⟩)𝑓))
119		df-ov 7258	. . . . . 6 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑋, 𝑤⟩)𝑓) = ((⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)
120	118, 119	eqtrdi 2795	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2^nd ‘((1^st ‘𝐺)‘𝑋))𝑤)‘𝑓) = ((⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩))
121	114, 117, 120	oveq123d 7276	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐿‘𝑤)(⟨((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧), ((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑤))((𝑧(2^nd ‘((1^st ‘𝐺)‘𝑋))𝑤)‘𝑓)) = (((⟨𝑋, 𝑤⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼‘𝑤)⟩)(⟨((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1^st ‘𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1^st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)))
122	1, 2, 57, 65, 104, 6, 60, 44, 66	curf11 17860	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧) = (𝑌(1^st ‘𝐹)𝑧))
123	122, 46	eqtrdi 2795	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧) = ((1^st ‘𝐹)‘⟨𝑌, 𝑧⟩))
124	106, 123	opeq12d 4809	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧), ((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧)⟩ = ⟨((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1^st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩)
125	124, 113	oveq12d 7273	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧), ((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑤)) = (⟨((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1^st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1^st ‘𝐹)‘⟨𝑌, 𝑤⟩)))
126	1, 2, 57, 65, 104, 6, 60, 44, 66, 27, 56, 68, 69	curf12 17861	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2^nd ‘((1^st ‘𝐺)‘𝑌))𝑤)‘𝑓) = (((Id‘𝐶)‘𝑌)(⟨𝑌, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)𝑓))
127		df-ov 7258	. . . . . 6 ⊢ (((Id‘𝐶)‘𝑌)(⟨𝑌, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)𝑓) = ((⟨𝑌, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)
128	126, 127	eqtrdi 2795	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2^nd ‘((1^st ‘𝐺)‘𝑌))𝑤)‘𝑓) = ((⟨𝑌, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩))
129	1, 2, 57, 65, 104, 6, 7, 8, 58, 60, 61, 12, 66	curf2val 17864	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑧) = (𝐾(⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)))
130		df-ov 7258	. . . . . 6 ⊢ (𝐾(⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩)(𝐼‘𝑧)) = ((⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)
131	129, 130	eqtrdi 2795	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑧) = ((⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩))
132	125, 128, 131	oveq123d 7276	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((𝑧(2^nd ‘((1^st ‘𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧), ((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧)) = (((⟨𝑌, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1^st ‘𝐹)‘⟨𝑋, 𝑧⟩), ((1^st ‘𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1^st ‘𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2^nd ‘𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼‘𝑧)⟩)))
133	103, 121, 132	3eqtr4d 2788	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐿‘𝑤)(⟨((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧), ((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑤))((𝑧(2^nd ‘((1^st ‘𝐺)‘𝑋))𝑤)‘𝑓)) = (((𝑧(2^nd ‘((1^st ‘𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧), ((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧)))
134	133	ralrimivvva 3115	. 2 ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤)((𝐿‘𝑤)(⟨((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧), ((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑤))((𝑧(2^nd ‘((1^st ‘𝐺)‘𝑋))𝑤)‘𝑓)) = (((𝑧(2^nd ‘((1^st ‘𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧), ((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧)))
135		curf2.n	. . 3 ⊢ 𝑁 = (𝐷 Nat 𝐸)
136	1, 2, 3, 4, 5, 6, 9, 40	curf1cl 17862	. . 3 ⊢ (𝜑 → ((1^st ‘𝐺)‘𝑋) ∈ (𝐷 Func 𝐸))
137	1, 2, 3, 4, 5, 6, 10, 44	curf1cl 17862	. . 3 ⊢ (𝜑 → ((1^st ‘𝐺)‘𝑌) ∈ (𝐷 Func 𝐸))
138	135, 6, 27, 17, 83, 136, 137	isnat2 17580	. 2 ⊢ (𝜑 → (𝐿 ∈ (((1^st ‘𝐺)‘𝑋)𝑁((1^st ‘𝐺)‘𝑌)) ↔ (𝐿 ∈ X𝑧 ∈ 𝐵 (((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧)) ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤)((𝐿‘𝑤)(⟨((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧), ((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑤))((𝑧(2^nd ‘((1^st ‘𝐺)‘𝑋))𝑤)‘𝑓)) = (((𝑧(2^nd ‘((1^st ‘𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1^st ‘((1^st ‘𝐺)‘𝑋))‘𝑧), ((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1^st ‘((1^st ‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧)))))
139	55, 134, 138	mpbir2and 709	1 ⊢ (𝜑 → 𝐿 ∈ (((1^st ‘𝐺)‘𝑋)𝑁((1^st ‘𝐺)‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ∀wral 3063 Vcvv 3422 ⟨cop 4564 class class class wbr 5070 ↦ cmpt 5153 × cxp 5578 Rel wrel 5585 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 1^st c1st 7802 2^nd c2nd 7803 Xcixp 8643 Basecbs 16840 Hom chom 16899 compcco 16900 Catccat 17290 Idccid 17291 Func cfunc 17485 Nat cnat 17573 ×_c cxpc 17801 curry_F ccurf 17844

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-er 8456 df-map 8575 df-ixp 8644 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-z 12250 df-dec 12367 df-uz 12512 df-fz 13169 df-struct 16776 df-slot 16811 df-ndx 16823 df-base 16841 df-hom 16912 df-cco 16913 df-cat 17294 df-cid 17295 df-func 17489 df-nat 17575 df-xpc 17805 df-curf 17848

This theorem is referenced by: curfcl 17866

W3C validator