Step | Hyp | Ref
| Expression |
1 | | diag2.l |
. . . . . 6
⊢ 𝐿 = (𝐶Δfunc𝐷) |
2 | | diag2.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ Cat) |
3 | | diag2.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ Cat) |
4 | 1, 2, 3 | diagval 16703 |
. . . . 5
⊢ (𝜑 → 𝐿 = (〈𝐶, 𝐷〉 curryF (𝐶
1stF 𝐷))) |
5 | 4 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (2nd
‘𝐿) = (2nd
‘(〈𝐶, 𝐷〉 curryF
(𝐶
1stF 𝐷)))) |
6 | 5 | oveqd 6566 |
. . 3
⊢ (𝜑 → (𝑋(2nd ‘𝐿)𝑌) = (𝑋(2nd ‘(〈𝐶, 𝐷〉 curryF (𝐶
1stF 𝐷)))𝑌)) |
7 | 6 | fveq1d 6105 |
. 2
⊢ (𝜑 → ((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = ((𝑋(2nd ‘(〈𝐶, 𝐷〉 curryF (𝐶
1stF 𝐷)))𝑌)‘𝐹)) |
8 | | eqid 2610 |
. . 3
⊢
(〈𝐶, 𝐷〉 curryF
(𝐶
1stF 𝐷)) = (〈𝐶, 𝐷〉 curryF (𝐶
1stF 𝐷)) |
9 | | diag2.a |
. . 3
⊢ 𝐴 = (Base‘𝐶) |
10 | | eqid 2610 |
. . . 4
⊢ (𝐶 ×c
𝐷) = (𝐶 ×c 𝐷) |
11 | | eqid 2610 |
. . . 4
⊢ (𝐶
1stF 𝐷) = (𝐶 1stF 𝐷) |
12 | 10, 2, 3, 11 | 1stfcl 16660 |
. . 3
⊢ (𝜑 → (𝐶 1stF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐶)) |
13 | | diag2.b |
. . 3
⊢ 𝐵 = (Base‘𝐷) |
14 | | diag2.h |
. . 3
⊢ 𝐻 = (Hom ‘𝐶) |
15 | | eqid 2610 |
. . 3
⊢
(Id‘𝐷) =
(Id‘𝐷) |
16 | | diag2.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
17 | | diag2.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝐴) |
18 | | diag2.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) |
19 | | eqid 2610 |
. . 3
⊢ ((𝑋(2nd
‘(〈𝐶, 𝐷〉 curryF
(𝐶
1stF 𝐷)))𝑌)‘𝐹) = ((𝑋(2nd ‘(〈𝐶, 𝐷〉 curryF (𝐶
1stF 𝐷)))𝑌)‘𝐹) |
20 | 8, 9, 2, 3, 12, 13, 14, 15, 16, 17, 18, 19 | curf2 16692 |
. 2
⊢ (𝜑 → ((𝑋(2nd ‘(〈𝐶, 𝐷〉 curryF (𝐶
1stF 𝐷)))𝑌)‘𝐹) = (𝑥 ∈ 𝐵 ↦ (𝐹(〈𝑋, 𝑥〉(2nd ‘(𝐶
1stF 𝐷))〈𝑌, 𝑥〉)((Id‘𝐷)‘𝑥)))) |
21 | 10, 9, 13 | xpcbas 16641 |
. . . . . . 7
⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷)) |
22 | | eqid 2610 |
. . . . . . 7
⊢ (Hom
‘(𝐶
×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷)) |
23 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ Cat) |
24 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ Cat) |
25 | | opelxpi 5072 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 〈𝑋, 𝑥〉 ∈ (𝐴 × 𝐵)) |
26 | 16, 25 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 〈𝑋, 𝑥〉 ∈ (𝐴 × 𝐵)) |
27 | | opelxpi 5072 |
. . . . . . . 8
⊢ ((𝑌 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 〈𝑌, 𝑥〉 ∈ (𝐴 × 𝐵)) |
28 | 17, 27 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 〈𝑌, 𝑥〉 ∈ (𝐴 × 𝐵)) |
29 | 10, 21, 22, 23, 24, 11, 26, 28 | 1stf2 16656 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (〈𝑋, 𝑥〉(2nd ‘(𝐶
1stF 𝐷))〈𝑌, 𝑥〉) = (1st ↾
(〈𝑋, 𝑥〉(Hom ‘(𝐶 ×c
𝐷))〈𝑌, 𝑥〉))) |
30 | 29 | oveqd 6566 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐹(〈𝑋, 𝑥〉(2nd ‘(𝐶
1stF 𝐷))〈𝑌, 𝑥〉)((Id‘𝐷)‘𝑥)) = (𝐹(1st ↾ (〈𝑋, 𝑥〉(Hom ‘(𝐶 ×c 𝐷))〈𝑌, 𝑥〉))((Id‘𝐷)‘𝑥))) |
31 | | df-ov 6552 |
. . . . . 6
⊢ (𝐹(1st ↾
(〈𝑋, 𝑥〉(Hom ‘(𝐶 ×c
𝐷))〈𝑌, 𝑥〉))((Id‘𝐷)‘𝑥)) = ((1st ↾ (〈𝑋, 𝑥〉(Hom ‘(𝐶 ×c 𝐷))〈𝑌, 𝑥〉))‘〈𝐹, ((Id‘𝐷)‘𝑥)〉) |
32 | 18 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐹 ∈ (𝑋𝐻𝑌)) |
33 | | eqid 2610 |
. . . . . . . . . 10
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
34 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
35 | 13, 33, 15, 24, 34 | catidcl 16166 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((Id‘𝐷)‘𝑥) ∈ (𝑥(Hom ‘𝐷)𝑥)) |
36 | | opelxpi 5072 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑋𝐻𝑌) ∧ ((Id‘𝐷)‘𝑥) ∈ (𝑥(Hom ‘𝐷)𝑥)) → 〈𝐹, ((Id‘𝐷)‘𝑥)〉 ∈ ((𝑋𝐻𝑌) × (𝑥(Hom ‘𝐷)𝑥))) |
37 | 32, 35, 36 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 〈𝐹, ((Id‘𝐷)‘𝑥)〉 ∈ ((𝑋𝐻𝑌) × (𝑥(Hom ‘𝐷)𝑥))) |
38 | 16 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑋 ∈ 𝐴) |
39 | 17 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑌 ∈ 𝐴) |
40 | 10, 9, 13, 14, 33, 38, 34, 39, 34, 22 | xpchom2 16649 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (〈𝑋, 𝑥〉(Hom ‘(𝐶 ×c 𝐷))〈𝑌, 𝑥〉) = ((𝑋𝐻𝑌) × (𝑥(Hom ‘𝐷)𝑥))) |
41 | 37, 40 | eleqtrrd 2691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 〈𝐹, ((Id‘𝐷)‘𝑥)〉 ∈ (〈𝑋, 𝑥〉(Hom ‘(𝐶 ×c 𝐷))〈𝑌, 𝑥〉)) |
42 | | fvres 6117 |
. . . . . . 7
⊢
(〈𝐹,
((Id‘𝐷)‘𝑥)〉 ∈ (〈𝑋, 𝑥〉(Hom ‘(𝐶 ×c 𝐷))〈𝑌, 𝑥〉) → ((1st ↾
(〈𝑋, 𝑥〉(Hom ‘(𝐶 ×c
𝐷))〈𝑌, 𝑥〉))‘〈𝐹, ((Id‘𝐷)‘𝑥)〉) = (1st ‘〈𝐹, ((Id‘𝐷)‘𝑥)〉)) |
43 | 41, 42 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((1st ↾
(〈𝑋, 𝑥〉(Hom ‘(𝐶 ×c
𝐷))〈𝑌, 𝑥〉))‘〈𝐹, ((Id‘𝐷)‘𝑥)〉) = (1st ‘〈𝐹, ((Id‘𝐷)‘𝑥)〉)) |
44 | 31, 43 | syl5eq 2656 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐹(1st ↾ (〈𝑋, 𝑥〉(Hom ‘(𝐶 ×c 𝐷))〈𝑌, 𝑥〉))((Id‘𝐷)‘𝑥)) = (1st ‘〈𝐹, ((Id‘𝐷)‘𝑥)〉)) |
45 | | op1stg 7071 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑋𝐻𝑌) ∧ ((Id‘𝐷)‘𝑥) ∈ (𝑥(Hom ‘𝐷)𝑥)) → (1st ‘〈𝐹, ((Id‘𝐷)‘𝑥)〉) = 𝐹) |
46 | 32, 35, 45 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (1st ‘〈𝐹, ((Id‘𝐷)‘𝑥)〉) = 𝐹) |
47 | 30, 44, 46 | 3eqtrd 2648 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐹(〈𝑋, 𝑥〉(2nd ‘(𝐶
1stF 𝐷))〈𝑌, 𝑥〉)((Id‘𝐷)‘𝑥)) = 𝐹) |
48 | 47 | mpteq2dva 4672 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝐹(〈𝑋, 𝑥〉(2nd ‘(𝐶
1stF 𝐷))〈𝑌, 𝑥〉)((Id‘𝐷)‘𝑥))) = (𝑥 ∈ 𝐵 ↦ 𝐹)) |
49 | | fconstmpt 5085 |
. . 3
⊢ (𝐵 × {𝐹}) = (𝑥 ∈ 𝐵 ↦ 𝐹) |
50 | 48, 49 | syl6eqr 2662 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝐹(〈𝑋, 𝑥〉(2nd ‘(𝐶
1stF 𝐷))〈𝑌, 𝑥〉)((Id‘𝐷)‘𝑥))) = (𝐵 × {𝐹})) |
51 | 7, 20, 50 | 3eqtrd 2648 |
1
⊢ (𝜑 → ((𝑋(2nd ‘𝐿)𝑌)‘𝐹) = (𝐵 × {𝐹})) |