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 16692 |
. . 3
⊢ (𝜑 → 𝐿 = (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)))) |
14 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝐶 ×c
𝐷) = (𝐶 ×c 𝐷) |
15 | 14, 2, 6 | xpcbas 16641 |
. . . . . . . . 9
⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷)) |
16 | | eqid 2610 |
. . . . . . . . 9
⊢ (Hom
‘(𝐶
×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷)) |
17 | | eqid 2610 |
. . . . . . . . 9
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) |
18 | | relfunc 16345 |
. . . . . . . . . . 11
⊢ Rel
((𝐶
×c 𝐷) Func 𝐸) |
19 | | 1st2ndbr 7108 |
. . . . . . . . . . 11
⊢ ((Rel
((𝐶
×c 𝐷) Func 𝐸) ∧ 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹)) |
20 | 18, 5, 19 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘𝐹)((𝐶 ×c
𝐷) Func 𝐸)(2nd ‘𝐹)) |
21 | 20 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹)) |
22 | | opelxpi 5072 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 〈𝑋, 𝑧〉 ∈ (𝐴 × 𝐵)) |
23 | 9, 22 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 〈𝑋, 𝑧〉 ∈ (𝐴 × 𝐵)) |
24 | | opelxpi 5072 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 〈𝑌, 𝑧〉 ∈ (𝐴 × 𝐵)) |
25 | 10, 24 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 〈𝑌, 𝑧〉 ∈ (𝐴 × 𝐵)) |
26 | 15, 16, 17, 21, 23, 25 | funcf2 16351 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉):(〈𝑋, 𝑧〉(Hom ‘(𝐶 ×c 𝐷))〈𝑌, 𝑧〉)⟶(((1st ‘𝐹)‘〈𝑋, 𝑧〉)(Hom ‘𝐸)((1st ‘𝐹)‘〈𝑌, 𝑧〉))) |
27 | | eqid 2610 |
. . . . . . . . . 10
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
28 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑋 ∈ 𝐴) |
29 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵) |
30 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑌 ∈ 𝐴) |
31 | 14, 2, 6, 7, 27, 28, 29, 30, 29, 16 | xpchom2 16649 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (〈𝑋, 𝑧〉(Hom ‘(𝐶 ×c 𝐷))〈𝑌, 𝑧〉) = ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧))) |
32 | 31 | feq2d 5944 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉):(〈𝑋, 𝑧〉(Hom ‘(𝐶 ×c 𝐷))〈𝑌, 𝑧〉)⟶(((1st ‘𝐹)‘〈𝑋, 𝑧〉)(Hom ‘𝐸)((1st ‘𝐹)‘〈𝑌, 𝑧〉)) ↔ (〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉):((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧))⟶(((1st ‘𝐹)‘〈𝑋, 𝑧〉)(Hom ‘𝐸)((1st ‘𝐹)‘〈𝑌, 𝑧〉)))) |
33 | 26, 32 | mpbid 221 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉):((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧))⟶(((1st ‘𝐹)‘〈𝑋, 𝑧〉)(Hom ‘𝐸)((1st ‘𝐹)‘〈𝑌, 𝑧〉))) |
34 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐾 ∈ (𝑋𝐻𝑌)) |
35 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐷 ∈ Cat) |
36 | 6, 27, 8, 35, 29 | catidcl 16166 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐼‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧)) |
37 | 33, 34, 36 | fovrnd 6704 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)) ∈ (((1st ‘𝐹)‘〈𝑋, 𝑧〉)(Hom ‘𝐸)((1st ‘𝐹)‘〈𝑌, 𝑧〉))) |
38 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐶 ∈ Cat) |
39 | 5 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) |
40 | | eqid 2610 |
. . . . . . . . 9
⊢
((1st ‘𝐺)‘𝑋) = ((1st ‘𝐺)‘𝑋) |
41 | 1, 2, 38, 35, 39, 6, 28, 40, 29 | curf11 16689 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧) = (𝑋(1st ‘𝐹)𝑧)) |
42 | | df-ov 6552 |
. . . . . . . 8
⊢ (𝑋(1st ‘𝐹)𝑧) = ((1st ‘𝐹)‘〈𝑋, 𝑧〉) |
43 | 41, 42 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧) = ((1st ‘𝐹)‘〈𝑋, 𝑧〉)) |
44 | | eqid 2610 |
. . . . . . . . 9
⊢
((1st ‘𝐺)‘𝑌) = ((1st ‘𝐺)‘𝑌) |
45 | 1, 2, 38, 35, 39, 6, 30, 44, 29 | curf11 16689 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st
‘((1st ‘𝐺)‘𝑌))‘𝑧) = (𝑌(1st ‘𝐹)𝑧)) |
46 | | df-ov 6552 |
. . . . . . . 8
⊢ (𝑌(1st ‘𝐹)𝑧) = ((1st ‘𝐹)‘〈𝑌, 𝑧〉) |
47 | 45, 46 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st
‘((1st ‘𝐺)‘𝑌))‘𝑧) = ((1st ‘𝐹)‘〈𝑌, 𝑧〉)) |
48 | 43, 47 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st
‘𝐺)‘𝑌))‘𝑧)) = (((1st ‘𝐹)‘〈𝑋, 𝑧〉)(Hom ‘𝐸)((1st ‘𝐹)‘〈𝑌, 𝑧〉))) |
49 | 37, 48 | eleqtrrd 2691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)) ∈ (((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st
‘𝐺)‘𝑌))‘𝑧))) |
50 | 49 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)) ∈ (((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st
‘𝐺)‘𝑌))‘𝑧))) |
51 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝐷)
∈ V |
52 | 6, 51 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
53 | | mptelixpg 7831 |
. . . . 5
⊢ (𝐵 ∈ V → ((𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧))) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st
‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st
‘𝐺)‘𝑌))‘𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)) ∈ (((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st
‘𝐺)‘𝑌))‘𝑧)))) |
54 | 52, 53 | ax-mp 5 |
. . . 4
⊢ ((𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧))) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st
‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st
‘𝐺)‘𝑌))‘𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)) ∈ (((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st
‘𝐺)‘𝑌))‘𝑧))) |
55 | 50, 54 | sylibr 223 |
. . 3
⊢ (𝜑 → (𝑧 ∈ 𝐵 ↦ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧))) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st
‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st
‘𝐺)‘𝑌))‘𝑧))) |
56 | 13, 55 | eqeltrd 2688 |
. 2
⊢ (𝜑 → 𝐿 ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st
‘𝐺)‘𝑋))‘𝑧)(Hom ‘𝐸)((1st ‘((1st
‘𝐺)‘𝑌))‘𝑧))) |
57 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Id‘𝐶) =
(Id‘𝐶) |
58 | 3 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐶 ∈ Cat) |
59 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑋 ∈ 𝐴) |
60 | | eqid 2610 |
. . . . . . . . . 10
⊢
(comp‘𝐶) =
(comp‘𝐶) |
61 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑌 ∈ 𝐴) |
62 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐾 ∈ (𝑋𝐻𝑌)) |
63 | 2, 7, 57, 58, 59, 60, 61, 62 | catrid 16168 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐾(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) = 𝐾) |
64 | 2, 7, 57, 58, 59, 60, 61, 62 | catlid 16167 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑌)(〈𝑋, 𝑌〉(comp‘𝐶)𝑌)𝐾) = 𝐾) |
65 | 63, 64 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐾(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)) = (((Id‘𝐶)‘𝑌)(〈𝑋, 𝑌〉(comp‘𝐶)𝑌)𝐾)) |
66 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐷 ∈ Cat) |
67 | | simpr1 1060 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑧 ∈ 𝐵) |
68 | | eqid 2610 |
. . . . . . . . . 10
⊢
(comp‘𝐷) =
(comp‘𝐷) |
69 | | simpr2 1061 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑤 ∈ 𝐵) |
70 | | simpr3 1062 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤)) |
71 | 6, 27, 8, 66, 67, 68, 69, 70 | catlid 16167 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐼‘𝑤)(〈𝑧, 𝑤〉(comp‘𝐷)𝑤)𝑓) = 𝑓) |
72 | 6, 27, 8, 66, 67, 68, 69, 70 | catrid 16168 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝑓(〈𝑧, 𝑧〉(comp‘𝐷)𝑤)(𝐼‘𝑧)) = 𝑓) |
73 | 71, 72 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐼‘𝑤)(〈𝑧, 𝑤〉(comp‘𝐷)𝑤)𝑓) = (𝑓(〈𝑧, 𝑧〉(comp‘𝐷)𝑤)(𝐼‘𝑧))) |
74 | 65, 73 | opeq12d 4348 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈(𝐾(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)), ((𝐼‘𝑤)(〈𝑧, 𝑤〉(comp‘𝐷)𝑤)𝑓)〉 = 〈(((Id‘𝐶)‘𝑌)(〈𝑋, 𝑌〉(comp‘𝐶)𝑌)𝐾), (𝑓(〈𝑧, 𝑧〉(comp‘𝐷)𝑤)(𝐼‘𝑧))〉) |
75 | | eqid 2610 |
. . . . . . . 8
⊢
(comp‘(𝐶
×c 𝐷)) = (comp‘(𝐶 ×c 𝐷)) |
76 | 2, 7, 57, 58, 59 | catidcl 16166 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑋) ∈ (𝑋𝐻𝑋)) |
77 | 6, 27, 8, 66, 69 | catidcl 16166 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐼‘𝑤) ∈ (𝑤(Hom ‘𝐷)𝑤)) |
78 | 14, 2, 6, 7, 27, 59, 67, 59, 69, 60, 68, 75, 61, 69, 76, 70, 62, 77 | xpcco2 16650 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (〈𝐾, (𝐼‘𝑤)〉(〈〈𝑋, 𝑧〉, 〈𝑋, 𝑤〉〉(comp‘(𝐶 ×c 𝐷))〈𝑌, 𝑤〉)〈((Id‘𝐶)‘𝑋), 𝑓〉) = 〈(𝐾(〈𝑋, 𝑋〉(comp‘𝐶)𝑌)((Id‘𝐶)‘𝑋)), ((𝐼‘𝑤)(〈𝑧, 𝑤〉(comp‘𝐷)𝑤)𝑓)〉) |
79 | 36 | 3ad2antr1 1219 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐼‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧)) |
80 | 2, 7, 57, 58, 61 | catidcl 16166 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑌) ∈ (𝑌𝐻𝑌)) |
81 | 14, 2, 6, 7, 27, 59, 67, 61, 67, 60, 68, 75, 61, 69, 62, 79, 80, 70 | xpcco2 16650 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (〈((Id‘𝐶)‘𝑌), 𝑓〉(〈〈𝑋, 𝑧〉, 〈𝑌, 𝑧〉〉(comp‘(𝐶 ×c 𝐷))〈𝑌, 𝑤〉)〈𝐾, (𝐼‘𝑧)〉) = 〈(((Id‘𝐶)‘𝑌)(〈𝑋, 𝑌〉(comp‘𝐶)𝑌)𝐾), (𝑓(〈𝑧, 𝑧〉(comp‘𝐷)𝑤)(𝐼‘𝑧))〉) |
82 | 74, 78, 81 | 3eqtr4d 2654 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (〈𝐾, (𝐼‘𝑤)〉(〈〈𝑋, 𝑧〉, 〈𝑋, 𝑤〉〉(comp‘(𝐶 ×c 𝐷))〈𝑌, 𝑤〉)〈((Id‘𝐶)‘𝑋), 𝑓〉) = (〈((Id‘𝐶)‘𝑌), 𝑓〉(〈〈𝑋, 𝑧〉, 〈𝑌, 𝑧〉〉(comp‘(𝐶 ×c 𝐷))〈𝑌, 𝑤〉)〈𝐾, (𝐼‘𝑧)〉)) |
83 | 82 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑤〉)‘(〈𝐾, (𝐼‘𝑤)〉(〈〈𝑋, 𝑧〉, 〈𝑋, 𝑤〉〉(comp‘(𝐶 ×c 𝐷))〈𝑌, 𝑤〉)〈((Id‘𝐶)‘𝑋), 𝑓〉)) = ((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑤〉)‘(〈((Id‘𝐶)‘𝑌), 𝑓〉(〈〈𝑋, 𝑧〉, 〈𝑌, 𝑧〉〉(comp‘(𝐶 ×c 𝐷))〈𝑌, 𝑤〉)〈𝐾, (𝐼‘𝑧)〉))) |
84 | | eqid 2610 |
. . . . . 6
⊢
(comp‘𝐸) =
(comp‘𝐸) |
85 | 20 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹)) |
86 | 23 | 3ad2antr1 1219 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈𝑋, 𝑧〉 ∈ (𝐴 × 𝐵)) |
87 | | opelxpi 5072 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → 〈𝑋, 𝑤〉 ∈ (𝐴 × 𝐵)) |
88 | 59, 69, 87 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈𝑋, 𝑤〉 ∈ (𝐴 × 𝐵)) |
89 | | opelxpi 5072 |
. . . . . . 7
⊢ ((𝑌 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → 〈𝑌, 𝑤〉 ∈ (𝐴 × 𝐵)) |
90 | 61, 69, 89 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈𝑌, 𝑤〉 ∈ (𝐴 × 𝐵)) |
91 | | opelxpi 5072 |
. . . . . . . 8
⊢
((((Id‘𝐶)‘𝑋) ∈ (𝑋𝐻𝑋) ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤)) → 〈((Id‘𝐶)‘𝑋), 𝑓〉 ∈ ((𝑋𝐻𝑋) × (𝑧(Hom ‘𝐷)𝑤))) |
92 | 76, 70, 91 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈((Id‘𝐶)‘𝑋), 𝑓〉 ∈ ((𝑋𝐻𝑋) × (𝑧(Hom ‘𝐷)𝑤))) |
93 | 14, 2, 6, 7, 27, 59, 67, 59, 69, 16 | xpchom2 16649 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (〈𝑋, 𝑧〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑤〉) = ((𝑋𝐻𝑋) × (𝑧(Hom ‘𝐷)𝑤))) |
94 | 92, 93 | eleqtrrd 2691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈((Id‘𝐶)‘𝑋), 𝑓〉 ∈ (〈𝑋, 𝑧〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑤〉)) |
95 | | opelxpi 5072 |
. . . . . . . 8
⊢ ((𝐾 ∈ (𝑋𝐻𝑌) ∧ (𝐼‘𝑤) ∈ (𝑤(Hom ‘𝐷)𝑤)) → 〈𝐾, (𝐼‘𝑤)〉 ∈ ((𝑋𝐻𝑌) × (𝑤(Hom ‘𝐷)𝑤))) |
96 | 62, 77, 95 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈𝐾, (𝐼‘𝑤)〉 ∈ ((𝑋𝐻𝑌) × (𝑤(Hom ‘𝐷)𝑤))) |
97 | 14, 2, 6, 7, 27, 59, 69, 61, 69, 16 | xpchom2 16649 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (〈𝑋, 𝑤〉(Hom ‘(𝐶 ×c 𝐷))〈𝑌, 𝑤〉) = ((𝑋𝐻𝑌) × (𝑤(Hom ‘𝐷)𝑤))) |
98 | 96, 97 | eleqtrrd 2691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈𝐾, (𝐼‘𝑤)〉 ∈ (〈𝑋, 𝑤〉(Hom ‘(𝐶 ×c 𝐷))〈𝑌, 𝑤〉)) |
99 | 15, 16, 75, 84, 85, 86, 88, 90, 94, 98 | funcco 16354 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑤〉)‘(〈𝐾, (𝐼‘𝑤)〉(〈〈𝑋, 𝑧〉, 〈𝑋, 𝑤〉〉(comp‘(𝐶 ×c 𝐷))〈𝑌, 𝑤〉)〈((Id‘𝐶)‘𝑋), 𝑓〉)) = (((〈𝑋, 𝑤〉(2nd ‘𝐹)〈𝑌, 𝑤〉)‘〈𝐾, (𝐼‘𝑤)〉)(〈((1st ‘𝐹)‘〈𝑋, 𝑧〉), ((1st ‘𝐹)‘〈𝑋, 𝑤〉)〉(comp‘𝐸)((1st ‘𝐹)‘〈𝑌, 𝑤〉))((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑋, 𝑤〉)‘〈((Id‘𝐶)‘𝑋), 𝑓〉))) |
100 | 25 | 3ad2antr1 1219 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈𝑌, 𝑧〉 ∈ (𝐴 × 𝐵)) |
101 | | opelxpi 5072 |
. . . . . . . 8
⊢ ((𝐾 ∈ (𝑋𝐻𝑌) ∧ (𝐼‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧)) → 〈𝐾, (𝐼‘𝑧)〉 ∈ ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧))) |
102 | 62, 79, 101 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈𝐾, (𝐼‘𝑧)〉 ∈ ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧))) |
103 | 14, 2, 6, 7, 27, 59, 67, 61, 67, 16 | xpchom2 16649 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (〈𝑋, 𝑧〉(Hom ‘(𝐶 ×c 𝐷))〈𝑌, 𝑧〉) = ((𝑋𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑧))) |
104 | 102, 103 | eleqtrrd 2691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈𝐾, (𝐼‘𝑧)〉 ∈ (〈𝑋, 𝑧〉(Hom ‘(𝐶 ×c 𝐷))〈𝑌, 𝑧〉)) |
105 | | opelxpi 5072 |
. . . . . . . 8
⊢
((((Id‘𝐶)‘𝑌) ∈ (𝑌𝐻𝑌) ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤)) → 〈((Id‘𝐶)‘𝑌), 𝑓〉 ∈ ((𝑌𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑤))) |
106 | 80, 70, 105 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈((Id‘𝐶)‘𝑌), 𝑓〉 ∈ ((𝑌𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑤))) |
107 | 14, 2, 6, 7, 27, 61, 67, 61, 69, 16 | xpchom2 16649 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (〈𝑌, 𝑧〉(Hom ‘(𝐶 ×c 𝐷))〈𝑌, 𝑤〉) = ((𝑌𝐻𝑌) × (𝑧(Hom ‘𝐷)𝑤))) |
108 | 106, 107 | eleqtrrd 2691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈((Id‘𝐶)‘𝑌), 𝑓〉 ∈ (〈𝑌, 𝑧〉(Hom ‘(𝐶 ×c 𝐷))〈𝑌, 𝑤〉)) |
109 | 15, 16, 75, 84, 85, 86, 100, 90, 104, 108 | funcco 16354 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑤〉)‘(〈((Id‘𝐶)‘𝑌), 𝑓〉(〈〈𝑋, 𝑧〉, 〈𝑌, 𝑧〉〉(comp‘(𝐶 ×c 𝐷))〈𝑌, 𝑤〉)〈𝐾, (𝐼‘𝑧)〉)) = (((〈𝑌, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑤〉)‘〈((Id‘𝐶)‘𝑌), 𝑓〉)(〈((1st ‘𝐹)‘〈𝑋, 𝑧〉), ((1st ‘𝐹)‘〈𝑌, 𝑧〉)〉(comp‘𝐸)((1st ‘𝐹)‘〈𝑌, 𝑤〉))((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)‘〈𝐾, (𝐼‘𝑧)〉))) |
110 | 83, 99, 109 | 3eqtr3d 2652 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((〈𝑋, 𝑤〉(2nd ‘𝐹)〈𝑌, 𝑤〉)‘〈𝐾, (𝐼‘𝑤)〉)(〈((1st ‘𝐹)‘〈𝑋, 𝑧〉), ((1st ‘𝐹)‘〈𝑋, 𝑤〉)〉(comp‘𝐸)((1st ‘𝐹)‘〈𝑌, 𝑤〉))((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑋, 𝑤〉)‘〈((Id‘𝐶)‘𝑋), 𝑓〉)) = (((〈𝑌, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑤〉)‘〈((Id‘𝐶)‘𝑌), 𝑓〉)(〈((1st ‘𝐹)‘〈𝑋, 𝑧〉), ((1st ‘𝐹)‘〈𝑌, 𝑧〉)〉(comp‘𝐸)((1st ‘𝐹)‘〈𝑌, 𝑤〉))((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)‘〈𝐾, (𝐼‘𝑧)〉))) |
111 | 5 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) |
112 | 1, 2, 58, 66, 111, 6, 59, 40, 67 | curf11 16689 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧) = (𝑋(1st ‘𝐹)𝑧)) |
113 | 112, 42 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧) = ((1st ‘𝐹)‘〈𝑋, 𝑧〉)) |
114 | 1, 2, 58, 66, 111, 6, 59, 40, 69 | curf11 16689 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st
‘((1st ‘𝐺)‘𝑋))‘𝑤) = (𝑋(1st ‘𝐹)𝑤)) |
115 | | df-ov 6552 |
. . . . . . . 8
⊢ (𝑋(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘〈𝑋, 𝑤〉) |
116 | 114, 115 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st
‘((1st ‘𝐺)‘𝑋))‘𝑤) = ((1st ‘𝐹)‘〈𝑋, 𝑤〉)) |
117 | 113, 116 | opeq12d 4348 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st
‘𝐺)‘𝑋))‘𝑤)〉 = 〈((1st ‘𝐹)‘〈𝑋, 𝑧〉), ((1st ‘𝐹)‘〈𝑋, 𝑤〉)〉) |
118 | 1, 2, 58, 66, 111, 6, 61, 44, 69 | curf11 16689 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st
‘((1st ‘𝐺)‘𝑌))‘𝑤) = (𝑌(1st ‘𝐹)𝑤)) |
119 | | df-ov 6552 |
. . . . . . 7
⊢ (𝑌(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘〈𝑌, 𝑤〉) |
120 | 118, 119 | syl6eq 2660 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st
‘((1st ‘𝐺)‘𝑌))‘𝑤) = ((1st ‘𝐹)‘〈𝑌, 𝑤〉)) |
121 | 117, 120 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (〈((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st
‘𝐺)‘𝑋))‘𝑤)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑌))‘𝑤)) = (〈((1st ‘𝐹)‘〈𝑋, 𝑧〉), ((1st ‘𝐹)‘〈𝑋, 𝑤〉)〉(comp‘𝐸)((1st ‘𝐹)‘〈𝑌, 𝑤〉))) |
122 | 1, 2, 58, 66, 111, 6, 7, 8, 59,
61, 62, 12, 69 | curf2val 16693 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑤) = (𝐾(〈𝑋, 𝑤〉(2nd ‘𝐹)〈𝑌, 𝑤〉)(𝐼‘𝑤))) |
123 | | df-ov 6552 |
. . . . . 6
⊢ (𝐾(〈𝑋, 𝑤〉(2nd ‘𝐹)〈𝑌, 𝑤〉)(𝐼‘𝑤)) = ((〈𝑋, 𝑤〉(2nd ‘𝐹)〈𝑌, 𝑤〉)‘〈𝐾, (𝐼‘𝑤)〉) |
124 | 122, 123 | syl6eq 2660 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑤) = ((〈𝑋, 𝑤〉(2nd ‘𝐹)〈𝑌, 𝑤〉)‘〈𝐾, (𝐼‘𝑤)〉)) |
125 | 1, 2, 58, 66, 111, 6, 59, 40, 67, 27, 57, 69, 70 | curf12 16690 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st
‘𝐺)‘𝑋))𝑤)‘𝑓) = (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑋, 𝑤〉)𝑓)) |
126 | | df-ov 6552 |
. . . . . 6
⊢
(((Id‘𝐶)‘𝑋)(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑋, 𝑤〉)𝑓) = ((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑋, 𝑤〉)‘〈((Id‘𝐶)‘𝑋), 𝑓〉) |
127 | 125, 126 | syl6eq 2660 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st
‘𝐺)‘𝑋))𝑤)‘𝑓) = ((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑋, 𝑤〉)‘〈((Id‘𝐶)‘𝑋), 𝑓〉)) |
128 | 121, 124,
127 | oveq123d 6570 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐿‘𝑤)(〈((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st
‘𝐺)‘𝑋))‘𝑤)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑌))‘𝑤))((𝑧(2nd ‘((1st
‘𝐺)‘𝑋))𝑤)‘𝑓)) = (((〈𝑋, 𝑤〉(2nd ‘𝐹)〈𝑌, 𝑤〉)‘〈𝐾, (𝐼‘𝑤)〉)(〈((1st ‘𝐹)‘〈𝑋, 𝑧〉), ((1st ‘𝐹)‘〈𝑋, 𝑤〉)〉(comp‘𝐸)((1st ‘𝐹)‘〈𝑌, 𝑤〉))((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑋, 𝑤〉)‘〈((Id‘𝐶)‘𝑋), 𝑓〉))) |
129 | 1, 2, 58, 66, 111, 6, 61, 44, 67 | curf11 16689 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st
‘((1st ‘𝐺)‘𝑌))‘𝑧) = (𝑌(1st ‘𝐹)𝑧)) |
130 | 129, 46 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st
‘((1st ‘𝐺)‘𝑌))‘𝑧) = ((1st ‘𝐹)‘〈𝑌, 𝑧〉)) |
131 | 113, 130 | opeq12d 4348 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st
‘𝐺)‘𝑌))‘𝑧)〉 = 〈((1st ‘𝐹)‘〈𝑋, 𝑧〉), ((1st ‘𝐹)‘〈𝑌, 𝑧〉)〉) |
132 | 131, 120 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (〈((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st
‘𝐺)‘𝑌))‘𝑧)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑌))‘𝑤)) = (〈((1st ‘𝐹)‘〈𝑋, 𝑧〉), ((1st ‘𝐹)‘〈𝑌, 𝑧〉)〉(comp‘𝐸)((1st ‘𝐹)‘〈𝑌, 𝑤〉))) |
133 | 1, 2, 58, 66, 111, 6, 61, 44, 67, 27, 57, 69, 70 | curf12 16690 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st
‘𝐺)‘𝑌))𝑤)‘𝑓) = (((Id‘𝐶)‘𝑌)(〈𝑌, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑤〉)𝑓)) |
134 | | df-ov 6552 |
. . . . . 6
⊢
(((Id‘𝐶)‘𝑌)(〈𝑌, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑤〉)𝑓) = ((〈𝑌, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑤〉)‘〈((Id‘𝐶)‘𝑌), 𝑓〉) |
135 | 133, 134 | syl6eq 2660 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘((1st
‘𝐺)‘𝑌))𝑤)‘𝑓) = ((〈𝑌, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑤〉)‘〈((Id‘𝐶)‘𝑌), 𝑓〉)) |
136 | 1, 2, 58, 66, 111, 6, 7, 8, 59,
61, 62, 12, 67 | curf2val 16693 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑧) = (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧))) |
137 | | df-ov 6552 |
. . . . . 6
⊢ (𝐾(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)(𝐼‘𝑧)) = ((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)‘〈𝐾, (𝐼‘𝑧)〉) |
138 | 136, 137 | syl6eq 2660 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (𝐿‘𝑧) = ((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)‘〈𝐾, (𝐼‘𝑧)〉)) |
139 | 132, 135,
138 | oveq123d 6570 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((𝑧(2nd ‘((1st
‘𝐺)‘𝑌))𝑤)‘𝑓)(〈((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st
‘𝐺)‘𝑌))‘𝑧)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧)) = (((〈𝑌, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑤〉)‘〈((Id‘𝐶)‘𝑌), 𝑓〉)(〈((1st ‘𝐹)‘〈𝑋, 𝑧〉), ((1st ‘𝐹)‘〈𝑌, 𝑧〉)〉(comp‘𝐸)((1st ‘𝐹)‘〈𝑌, 𝑤〉))((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑌, 𝑧〉)‘〈𝐾, (𝐼‘𝑧)〉))) |
140 | 110, 128,
139 | 3eqtr4d 2654 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ 𝑓 ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝐿‘𝑤)(〈((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st
‘𝐺)‘𝑋))‘𝑤)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑌))‘𝑤))((𝑧(2nd ‘((1st
‘𝐺)‘𝑋))𝑤)‘𝑓)) = (((𝑧(2nd ‘((1st
‘𝐺)‘𝑌))𝑤)‘𝑓)(〈((1st
‘((1st ‘𝐺)‘𝑋))‘𝑧), ((1st ‘((1st
‘𝐺)‘𝑌))‘𝑧)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧))) |
141 | 140 | ralrimivvva 2955 |
. 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 𝐸) |
143 | 1, 2, 3, 4, 5, 6, 9, 40 | curf1cl 16691 |
. . 3
⊢ (𝜑 → ((1st
‘𝐺)‘𝑋) ∈ (𝐷 Func 𝐸)) |
144 | 1, 2, 3, 4, 5, 6, 10, 44 | curf1cl 16691 |
. . 3
⊢ (𝜑 → ((1st
‘𝐺)‘𝑌) ∈ (𝐷 Func 𝐸)) |
145 | 142, 6, 27, 17, 84, 143, 144 | isnat2 16431 |
. 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
‘𝐺)‘𝑌))‘𝑤))(𝐿‘𝑧))))) |
146 | 56, 141, 145 | mpbir2and 959 |
1
⊢ (𝜑 → 𝐿 ∈ (((1st ‘𝐺)‘𝑋)𝑁((1st ‘𝐺)‘𝑌))) |