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

Theorem curf2cl 16993
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.
StepHypRef 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𝐺)𝑌)‘𝐾)
131, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12curf2 16991 . . 3 (𝜑𝐿 = (𝑧𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧))))
14 eqid 2724 . . . . . . . . . 10 (𝐶 ×c 𝐷) = (𝐶 ×c 𝐷)
1514, 2, 6xpcbas 16940 . . . . . . . . 9 (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷))
16 eqid 2724 . . . . . . . . 9 (Hom ‘(𝐶 ×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷))
17 eqid 2724 . . . . . . . . 9 (Hom ‘𝐸) = (Hom ‘𝐸)
18 relfunc 16644 . . . . . . . . . . 11 Rel ((𝐶 ×c 𝐷) Func 𝐸)
19 1st2ndbr 7336 . . . . . . . . . . 11 ((Rel ((𝐶 ×c 𝐷) Func 𝐸) ∧ 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
2018, 5, 19sylancr 698 . . . . . . . . . 10 (𝜑 → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
2120adantr 472 . . . . . . . . 9 ((𝜑𝑧𝐵) → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
22 opelxpi 5257 . . . . . . . . . 10 ((𝑋𝐴𝑧𝐵) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
239, 22sylan 489 . . . . . . . . 9 ((𝜑𝑧𝐵) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
24 opelxpi 5257 . . . . . . . . . 10 ((𝑌𝐴𝑧𝐵) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
2510, 24sylan 489 . . . . . . . . 9 ((𝜑𝑧𝐵) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
2615, 16, 17, 21, 23, 25funcf2 16650 . . . . . . . 8 ((𝜑𝑧𝐵) → (⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩):(⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩)⟶(((1st𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st𝐹)‘⟨𝑌, 𝑧⟩)))
27 eqid 2724 . . . . . . . . . 10 (Hom ‘𝐷) = (Hom ‘𝐷)
289adantr 472 . . . . . . . . . 10 ((𝜑𝑧𝐵) → 𝑋𝐴)
29 simpr 479 . . . . . . . . . 10 ((𝜑𝑧𝐵) → 𝑧𝐵)
3010adantr 472 . . . . . . . . . 10 ((𝜑𝑧𝐵) → 𝑌𝐴)
3114, 2, 6, 7, 27, 28, 29, 30, 29, 16xpchom2 16948 . . . . . . . . 9 ((𝜑𝑧𝐵) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩) = ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
3231feq2d 6144 . . . . . . . 8 ((𝜑𝑧𝐵) → ((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩):(⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩)⟶(((1st𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st𝐹)‘⟨𝑌, 𝑧⟩)) ↔ (⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩):((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧))⟶(((1st𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st𝐹)‘⟨𝑌, 𝑧⟩))))
3326, 32mpbid 222 . . . . . . 7 ((𝜑𝑧𝐵) → (⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩):((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧))⟶(((1st𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st𝐹)‘⟨𝑌, 𝑧⟩)))
3411adantr 472 . . . . . . 7 ((𝜑𝑧𝐵) → 𝐾 ∈ (𝑋𝐻𝑌))
354adantr 472 . . . . . . . 8 ((𝜑𝑧𝐵) → 𝐷 ∈ Cat)
366, 27, 8, 35, 29catidcl 16465 . . . . . . 7 ((𝜑𝑧𝐵) → (𝐼𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧))
3733, 34, 36fovrnd 6923 . . . . . 6 ((𝜑𝑧𝐵) → (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧)) ∈ (((1st𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st𝐹)‘⟨𝑌, 𝑧⟩)))
383adantr 472 . . . . . . . . 9 ((𝜑𝑧𝐵) → 𝐶 ∈ Cat)
395adantr 472 . . . . . . . . 9 ((𝜑𝑧𝐵) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
40 eqid 2724 . . . . . . . . 9 ((1st𝐺)‘𝑋) = ((1st𝐺)‘𝑋)
411, 2, 38, 35, 39, 6, 28, 40, 29curf11 16988 . . . . . . . 8 ((𝜑𝑧𝐵) → ((1st ‘((1st𝐺)‘𝑋))‘𝑧) = (𝑋(1st𝐹)𝑧))
42 df-ov 6768 . . . . . . . 8 (𝑋(1st𝐹)𝑧) = ((1st𝐹)‘⟨𝑋, 𝑧⟩)
4341, 42syl6eq 2774 . . . . . . 7 ((𝜑𝑧𝐵) → ((1st ‘((1st𝐺)‘𝑋))‘𝑧) = ((1st𝐹)‘⟨𝑋, 𝑧⟩))
44 eqid 2724 . . . . . . . . 9 ((1st𝐺)‘𝑌) = ((1st𝐺)‘𝑌)
451, 2, 38, 35, 39, 6, 30, 44, 29curf11 16988 . . . . . . . 8 ((𝜑𝑧𝐵) → ((1st ‘((1st𝐺)‘𝑌))‘𝑧) = (𝑌(1st𝐹)𝑧))
46 df-ov 6768 . . . . . . . 8 (𝑌(1st𝐹)𝑧) = ((1st𝐹)‘⟨𝑌, 𝑧⟩)
4745, 46syl6eq 2774 . . . . . . 7 ((𝜑𝑧𝐵) → ((1st ‘((1st𝐺)‘𝑌))‘𝑧) = ((1st𝐹)‘⟨𝑌, 𝑧⟩))
4843, 47oveq12d 6783 . . . . . 6 ((𝜑𝑧𝐵) → (((1st ‘((1st𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑧)) = (((1st𝐹)‘⟨𝑋, 𝑧⟩)(Hom ‘𝐸)((1st𝐹)‘⟨𝑌, 𝑧⟩)))
4937, 48eleqtrrd 2806 . . . . 5 ((𝜑𝑧𝐵) → (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧)) ∈ (((1st ‘((1st𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑧)))
5049ralrimiva 3068 . . . 4 (𝜑 → ∀𝑧𝐵 (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧)) ∈ (((1st ‘((1st𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑧)))
51 fvex 6314 . . . . . 6 (Base‘𝐷) ∈ V
526, 51eqeltri 2799 . . . . 5 𝐵 ∈ V
53 mptelixpg 8062 . . . . 5 (𝐵 ∈ V → ((𝑧𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧))) ∈ X𝑧𝐵 (((1st ‘((1st𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑧)) ↔ ∀𝑧𝐵 (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧)) ∈ (((1st ‘((1st𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑧))))
5452, 53ax-mp 5 . . . 4 ((𝑧𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧))) ∈ X𝑧𝐵 (((1st ‘((1st𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑧)) ↔ ∀𝑧𝐵 (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧)) ∈ (((1st ‘((1st𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑧)))
5550, 54sylibr 224 . . 3 (𝜑 → (𝑧𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧))) ∈ X𝑧𝐵 (((1st ‘((1st𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑧)))
5613, 55eqeltrd 2803 . 2 (𝜑𝐿X𝑧𝐵 (((1st ‘((1st𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑧)))
57 eqid 2724 . . . . . . . . . 10 (Id‘𝐶) = (Id‘𝐶)
583adantr 472 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐶 ∈ Cat)
599adantr 472 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑋𝐴)
60 eqid 2724 . . . . . . . . . 10 (comp‘𝐶) = (comp‘𝐶)
6110adantr 472 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑌𝐴)
6211adantr 472 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐾 ∈ (𝑋𝐻𝑌))
632, 7, 57, 58, 59, 60, 61, 62catrid 16467 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) = 𝐾)
642, 7, 57, 58, 59, 60, 61, 62catlid 16466 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾) = 𝐾)
6563, 64eqtr4d 2761 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) = (((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾))
664adantr 472 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐷 ∈ Cat)
67 simpr1 1210 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑧𝐵)
68 eqid 2724 . . . . . . . . . 10 (comp‘𝐷) = (comp‘𝐷)
69 simpr2 1212 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑤𝐵)
70 simpr3 1214 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))
716, 27, 8, 66, 67, 68, 69, 70catlid 16466 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐼𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓) = 𝑓)
726, 27, 8, 66, 67, 68, 69, 70catrid 16467 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼𝑧)) = 𝑓)
7371, 72eqtr4d 2761 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐼𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓) = (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼𝑧)))
7465, 73opeq12d 4517 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨(𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)), ((𝐼𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓)⟩ = ⟨(((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾), (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼𝑧))⟩)
75 eqid 2724 . . . . . . . 8 (comp‘(𝐶 ×c 𝐷)) = (comp‘(𝐶 ×c 𝐷))
762, 7, 57, 58, 59catidcl 16465 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑋) ∈ (𝑋𝐻𝑋))
776, 27, 8, 66, 69catidcl 16465 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐼𝑤) ∈ (𝑤(Hom ‘𝐷)𝑤))
7814, 2, 6, 7, 27, 59, 67, 59, 69, 60, 68, 75, 61, 69, 76, 70, 62, 77xpcco2 16949 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝐾, (𝐼𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩) = ⟨(𝐾(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)), ((𝐼𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐷)𝑤)𝑓)⟩)
79363ad2antr1 1180 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐼𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧))
802, 7, 57, 58, 61catidcl 16465 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑌) ∈ (𝑌𝐻𝑌))
8114, 2, 6, 7, 27, 59, 67, 61, 67, 60, 68, 75, 61, 69, 62, 79, 80, 70xpcco2 16949 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼𝑧)⟩) = ⟨(((Id‘𝐶)‘𝑌)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑌)𝐾), (𝑓(⟨𝑧, 𝑧⟩(comp‘𝐷)𝑤)(𝐼𝑧))⟩)
8274, 78, 813eqtr4d 2768 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝐾, (𝐼𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩) = (⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼𝑧)⟩))
8382fveq2d 6308 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑤⟩)‘(⟨𝐾, (𝐼𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = ((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼𝑧)⟩)))
84 eqid 2724 . . . . . 6 (comp‘𝐸) = (comp‘𝐸)
8520adantr 472 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
86233ad2antr1 1180 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
87 opelxpi 5257 . . . . . . 7 ((𝑋𝐴𝑤𝐵) → ⟨𝑋, 𝑤⟩ ∈ (𝐴 × 𝐵))
8859, 69, 87syl2anc 696 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑤⟩ ∈ (𝐴 × 𝐵))
89 opelxpi 5257 . . . . . . 7 ((𝑌𝐴𝑤𝐵) → ⟨𝑌, 𝑤⟩ ∈ (𝐴 × 𝐵))
9061, 69, 89syl2anc 696 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑌, 𝑤⟩ ∈ (𝐴 × 𝐵))
91 opelxpi 5257 . . . . . . . 8 ((((Id‘𝐶)‘𝑋) ∈ (𝑋𝐻𝑋) ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤)) → ⟨((Id‘𝐶)‘𝑋), 𝑓⟩ ∈ ((𝑋𝐻𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
9276, 70, 91syl2anc 696 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑓⟩ ∈ ((𝑋𝐻𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
9314, 2, 6, 7, 27, 59, 67, 59, 69, 16xpchom2 16948 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩) = ((𝑋𝐻𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
9492, 93eleqtrrd 2806 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑓⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩))
95 opelxpi 5257 . . . . . . . 8 ((𝐾 ∈ (𝑋𝐻𝑌) ∧ (𝐼𝑤) ∈ (𝑤(Hom ‘𝐷)𝑤)) → ⟨𝐾, (𝐼𝑤)⟩ ∈ ((𝑋𝐻𝑌) × (𝑤(Hom ‘𝐷)𝑤)))
9662, 77, 95syl2anc 696 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼𝑤)⟩ ∈ ((𝑋𝐻𝑌) × (𝑤(Hom ‘𝐷)𝑤)))
9714, 2, 6, 7, 27, 59, 69, 61, 69, 16xpchom2 16948 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑤⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩) = ((𝑋𝐻𝑌) × (𝑤(Hom ‘𝐷)𝑤)))
9896, 97eleqtrrd 2806 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼𝑤)⟩ ∈ (⟨𝑋, 𝑤⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩))
9915, 16, 75, 84, 85, 86, 88, 90, 94, 98funcco 16653 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑤⟩)‘(⟨𝐾, (𝐼𝑤)⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑋, 𝑤⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = (((⟨𝑋, 𝑤⟩(2nd𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼𝑤)⟩)(⟨((1st𝐹)‘⟨𝑋, 𝑧⟩), ((1st𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)))
100253ad2antr1 1180 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑌, 𝑧⟩ ∈ (𝐴 × 𝐵))
101 opelxpi 5257 . . . . . . . 8 ((𝐾 ∈ (𝑋𝐻𝑌) ∧ (𝐼𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧)) → ⟨𝐾, (𝐼𝑧)⟩ ∈ ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
10262, 79, 101syl2anc 696 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼𝑧)⟩ ∈ ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
10314, 2, 6, 7, 27, 59, 67, 61, 67, 16xpchom2 16948 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩) = ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧)))
104102, 103eleqtrrd 2806 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝐾, (𝐼𝑧)⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑧⟩))
105 opelxpi 5257 . . . . . . . 8 ((((Id‘𝐶)‘𝑌) ∈ (𝑌𝐻𝑌) ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤)) → ⟨((Id‘𝐶)‘𝑌), 𝑓⟩ ∈ ((𝑌𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑤)))
10680, 70, 105syl2anc 696 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑌), 𝑓⟩ ∈ ((𝑌𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑤)))
10714, 2, 6, 7, 27, 61, 67, 61, 69, 16xpchom2 16948 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑌, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩) = ((𝑌𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑤)))
108106, 107eleqtrrd 2806 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑌), 𝑓⟩ ∈ (⟨𝑌, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩))
10915, 16, 75, 84, 85, 86, 100, 90, 104, 108funcco 16653 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑌), 𝑓⟩(⟨⟨𝑋, 𝑧⟩, ⟨𝑌, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑌, 𝑤⟩)⟨𝐾, (𝐼𝑧)⟩)) = (((⟨𝑌, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1st𝐹)‘⟨𝑋, 𝑧⟩), ((1st𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼𝑧)⟩)))
11083, 99, 1093eqtr3d 2766 . . . 4 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((⟨𝑋, 𝑤⟩(2nd𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼𝑤)⟩)(⟨((1st𝐹)‘⟨𝑋, 𝑧⟩), ((1st𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)) = (((⟨𝑌, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1st𝐹)‘⟨𝑋, 𝑧⟩), ((1st𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼𝑧)⟩)))
1115adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
1121, 2, 58, 66, 111, 6, 59, 40, 67curf11 16988 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st𝐺)‘𝑋))‘𝑧) = (𝑋(1st𝐹)𝑧))
113112, 42syl6eq 2774 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st𝐺)‘𝑋))‘𝑧) = ((1st𝐹)‘⟨𝑋, 𝑧⟩))
1141, 2, 58, 66, 111, 6, 59, 40, 69curf11 16988 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st𝐺)‘𝑋))‘𝑤) = (𝑋(1st𝐹)𝑤))
115 df-ov 6768 . . . . . . . 8 (𝑋(1st𝐹)𝑤) = ((1st𝐹)‘⟨𝑋, 𝑤⟩)
116114, 115syl6eq 2774 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st𝐺)‘𝑋))‘𝑤) = ((1st𝐹)‘⟨𝑋, 𝑤⟩))
117113, 116opeq12d 4517 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1st ‘((1st𝐺)‘𝑋))‘𝑧), ((1st ‘((1st𝐺)‘𝑋))‘𝑤)⟩ = ⟨((1st𝐹)‘⟨𝑋, 𝑧⟩), ((1st𝐹)‘⟨𝑋, 𝑤⟩)⟩)
1181, 2, 58, 66, 111, 6, 61, 44, 69curf11 16988 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st𝐺)‘𝑌))‘𝑤) = (𝑌(1st𝐹)𝑤))
119 df-ov 6768 . . . . . . 7 (𝑌(1st𝐹)𝑤) = ((1st𝐹)‘⟨𝑌, 𝑤⟩)
120118, 119syl6eq 2774 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st𝐺)‘𝑌))‘𝑤) = ((1st𝐹)‘⟨𝑌, 𝑤⟩))
121117, 120oveq12d 6783 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((1st ‘((1st𝐺)‘𝑋))‘𝑧), ((1st ‘((1st𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑤)) = (⟨((1st𝐹)‘⟨𝑋, 𝑧⟩), ((1st𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑌, 𝑤⟩)))
1221, 2, 58, 66, 111, 6, 7, 8, 59, 61, 62, 12, 69curf2val 16992 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿𝑤) = (𝐾(⟨𝑋, 𝑤⟩(2nd𝐹)⟨𝑌, 𝑤⟩)(𝐼𝑤)))
123 df-ov 6768 . . . . . 6 (𝐾(⟨𝑋, 𝑤⟩(2nd𝐹)⟨𝑌, 𝑤⟩)(𝐼𝑤)) = ((⟨𝑋, 𝑤⟩(2nd𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼𝑤)⟩)
124122, 123syl6eq 2774 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿𝑤) = ((⟨𝑋, 𝑤⟩(2nd𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼𝑤)⟩))
1251, 2, 58, 66, 111, 6, 59, 40, 67, 27, 57, 69, 70curf12 16989 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st𝐺)‘𝑋))𝑤)‘𝑓) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)𝑓))
126 df-ov 6768 . . . . . 6 (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)𝑓) = ((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)
127125, 126syl6eq 2774 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st𝐺)‘𝑋))𝑤)‘𝑓) = ((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩))
128121, 124, 127oveq123d 6786 . . . 4 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐿𝑤)(⟨((1st ‘((1st𝐺)‘𝑋))‘𝑧), ((1st ‘((1st𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑤))((𝑧(2nd ‘((1st𝐺)‘𝑋))𝑤)‘𝑓)) = (((⟨𝑋, 𝑤⟩(2nd𝐹)⟨𝑌, 𝑤⟩)‘⟨𝐾, (𝐼𝑤)⟩)(⟨((1st𝐹)‘⟨𝑋, 𝑧⟩), ((1st𝐹)‘⟨𝑋, 𝑤⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑓⟩)))
1291, 2, 58, 66, 111, 6, 61, 44, 67curf11 16988 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st𝐺)‘𝑌))‘𝑧) = (𝑌(1st𝐹)𝑧))
130129, 46syl6eq 2774 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘((1st𝐺)‘𝑌))‘𝑧) = ((1st𝐹)‘⟨𝑌, 𝑧⟩))
131113, 130opeq12d 4517 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1st ‘((1st𝐺)‘𝑋))‘𝑧), ((1st ‘((1st𝐺)‘𝑌))‘𝑧)⟩ = ⟨((1st𝐹)‘⟨𝑋, 𝑧⟩), ((1st𝐹)‘⟨𝑌, 𝑧⟩)⟩)
132131, 120oveq12d 6783 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((1st ‘((1st𝐺)‘𝑋))‘𝑧), ((1st ‘((1st𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑤)) = (⟨((1st𝐹)‘⟨𝑋, 𝑧⟩), ((1st𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑌, 𝑤⟩)))
1331, 2, 58, 66, 111, 6, 61, 44, 67, 27, 57, 69, 70curf12 16989 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st𝐺)‘𝑌))𝑤)‘𝑓) = (((Id‘𝐶)‘𝑌)(⟨𝑌, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑤⟩)𝑓))
134 df-ov 6768 . . . . . 6 (((Id‘𝐶)‘𝑌)(⟨𝑌, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑤⟩)𝑓) = ((⟨𝑌, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)
135133, 134syl6eq 2774 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st𝐺)‘𝑌))𝑤)‘𝑓) = ((⟨𝑌, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩))
1361, 2, 58, 66, 111, 6, 7, 8, 59, 61, 62, 12, 67curf2val 16992 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿𝑧) = (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧)))
137 df-ov 6768 . . . . . 6 (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧)) = ((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼𝑧)⟩)
138136, 137syl6eq 2774 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿𝑧) = ((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼𝑧)⟩))
139132, 135, 138oveq123d 6786 . . . 4 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((𝑧(2nd ‘((1st𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1st ‘((1st𝐺)‘𝑋))‘𝑧), ((1st ‘((1st𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑤))(𝐿𝑧)) = (((⟨𝑌, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑌), 𝑓⟩)(⟨((1st𝐹)‘⟨𝑋, 𝑧⟩), ((1st𝐹)‘⟨𝑌, 𝑧⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑌, 𝑤⟩))((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)‘⟨𝐾, (𝐼𝑧)⟩)))
140110, 128, 1393eqtr4d 2768 . . 3 ((𝜑 ∧ (𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐿𝑤)(⟨((1st ‘((1st𝐺)‘𝑋))‘𝑧), ((1st ‘((1st𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑤))((𝑧(2nd ‘((1st𝐺)‘𝑋))𝑤)‘𝑓)) = (((𝑧(2nd ‘((1st𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1st ‘((1st𝐺)‘𝑋))‘𝑧), ((1st ‘((1st𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑤))(𝐿𝑧)))
141140ralrimivvva 3074 . 2 (𝜑 → ∀𝑧𝐵𝑤𝐵𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤)((𝐿𝑤)(⟨((1st ‘((1st𝐺)‘𝑋))‘𝑧), ((1st ‘((1st𝐺)‘𝑋))‘𝑤)⟩(comp‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑤))((𝑧(2nd ‘((1st𝐺)‘𝑋))𝑤)‘𝑓)) = (((𝑧(2nd ‘((1st𝐺)‘𝑌))𝑤)‘𝑓)(⟨((1st ‘((1st𝐺)‘𝑋))‘𝑧), ((1st ‘((1st𝐺)‘𝑌))‘𝑧)⟩(comp‘𝐸)((1st ‘((1st𝐺)‘𝑌))‘𝑤))(𝐿𝑧)))
142 curf2.n . . 3 𝑁 = (𝐷 Nat 𝐸)
1431, 2, 3, 4, 5, 6, 9, 40curf1cl 16990 . . 3 (𝜑 → ((1st𝐺)‘𝑋) ∈ (𝐷 Func 𝐸))
1441, 2, 3, 4, 5, 6, 10, 44curf1cl 16990 . . 3 (𝜑 → ((1st𝐺)‘𝑌) ∈ (𝐷 Func 𝐸))
145142, 6, 27, 17, 84, 143, 144isnat2 16730 . 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𝐺)‘𝑌))‘𝑤))(𝐿𝑧)))))
14656, 141, 145mpbir2and 995 1 (𝜑𝐿 ∈ (((1st𝐺)‘𝑋)𝑁((1st𝐺)‘𝑌)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1596  wcel 2103  wral 3014  Vcvv 3304  cop 4291   class class class wbr 4760  cmpt 4837   × cxp 5216  Rel wrel 5223  wf 5997  cfv 6001  (class class class)co 6765  1st c1st 7283  2nd c2nd 7284  Xcixp 8025  Basecbs 15980  Hom chom 16075  compcco 16076  Catccat 16447  Idccid 16448   Func cfunc 16636   Nat cnat 16723   ×c cxpc 16930   curryF ccurf 16972
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-fal 1602  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-int 4584  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-1o 7680  df-oadd 7684  df-er 7862  df-map 7976  df-ixp 8026  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-nn 11134  df-2 11192  df-3 11193  df-4 11194  df-5 11195  df-6 11196  df-7 11197  df-8 11198  df-9 11199  df-n0 11406  df-z 11491  df-dec 11607  df-uz 11801  df-fz 12441  df-struct 15982  df-ndx 15983  df-slot 15984  df-base 15986  df-hom 16089  df-cco 16090  df-cat 16451  df-cid 16452  df-func 16640  df-nat 16725  df-xpc 16934  df-curf 16976
This theorem is referenced by:  curfcl  16994
  Copyright terms: Public domain W3C validator