Proof of Theorem diag12
Step | Hyp | Ref
| Expression |
1 | | diag11.k |
. . . . . 6
⊢ 𝐾 = ((1st ‘𝐿)‘𝑋) |
2 | | diagval.l |
. . . . . . . . 9
⊢ 𝐿 = (𝐶Δfunc𝐷) |
3 | | diagval.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ Cat) |
4 | | diagval.d |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ Cat) |
5 | 2, 3, 4 | diagval 16703 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 = (〈𝐶, 𝐷〉 curryF (𝐶
1stF 𝐷))) |
6 | 5 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → (1st
‘𝐿) = (1st
‘(〈𝐶, 𝐷〉 curryF
(𝐶
1stF 𝐷)))) |
7 | 6 | fveq1d 6105 |
. . . . . 6
⊢ (𝜑 → ((1st
‘𝐿)‘𝑋) = ((1st
‘(〈𝐶, 𝐷〉 curryF
(𝐶
1stF 𝐷)))‘𝑋)) |
8 | 1, 7 | syl5eq 2656 |
. . . . 5
⊢ (𝜑 → 𝐾 = ((1st ‘(〈𝐶, 𝐷〉 curryF (𝐶
1stF 𝐷)))‘𝑋)) |
9 | 8 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (2nd
‘𝐾) = (2nd
‘((1st ‘(〈𝐶, 𝐷〉 curryF (𝐶
1stF 𝐷)))‘𝑋))) |
10 | 9 | oveqd 6566 |
. . 3
⊢ (𝜑 → (𝑌(2nd ‘𝐾)𝑍) = (𝑌(2nd ‘((1st
‘(〈𝐶, 𝐷〉 curryF
(𝐶
1stF 𝐷)))‘𝑋))𝑍)) |
11 | 10 | fveq1d 6105 |
. 2
⊢ (𝜑 → ((𝑌(2nd ‘𝐾)𝑍)‘𝐹) = ((𝑌(2nd ‘((1st
‘(〈𝐶, 𝐷〉 curryF
(𝐶
1stF 𝐷)))‘𝑋))𝑍)‘𝐹)) |
12 | | eqid 2610 |
. . 3
⊢
(〈𝐶, 𝐷〉 curryF
(𝐶
1stF 𝐷)) = (〈𝐶, 𝐷〉 curryF (𝐶
1stF 𝐷)) |
13 | | diag11.a |
. . 3
⊢ 𝐴 = (Base‘𝐶) |
14 | | eqid 2610 |
. . . 4
⊢ (𝐶 ×c
𝐷) = (𝐶 ×c 𝐷) |
15 | | eqid 2610 |
. . . 4
⊢ (𝐶
1stF 𝐷) = (𝐶 1stF 𝐷) |
16 | 14, 3, 4, 15 | 1stfcl 16660 |
. . 3
⊢ (𝜑 → (𝐶 1stF 𝐷) ∈ ((𝐶 ×c 𝐷) Func 𝐶)) |
17 | | diag11.b |
. . 3
⊢ 𝐵 = (Base‘𝐷) |
18 | | diag11.c |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
19 | | eqid 2610 |
. . 3
⊢
((1st ‘(〈𝐶, 𝐷〉 curryF (𝐶
1stF 𝐷)))‘𝑋) = ((1st ‘(〈𝐶, 𝐷〉 curryF (𝐶
1stF 𝐷)))‘𝑋) |
20 | | diag11.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
21 | | diag12.j |
. . 3
⊢ 𝐽 = (Hom ‘𝐷) |
22 | | diag12.i |
. . 3
⊢ 1 =
(Id‘𝐶) |
23 | | diag12.z |
. . 3
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
24 | | diag12.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ (𝑌𝐽𝑍)) |
25 | 12, 13, 3, 4, 16, 17, 18, 19, 20, 21, 22, 23, 24 | curf12 16690 |
. 2
⊢ (𝜑 → ((𝑌(2nd ‘((1st
‘(〈𝐶, 𝐷〉 curryF
(𝐶
1stF 𝐷)))‘𝑋))𝑍)‘𝐹) = (( 1 ‘𝑋)(〈𝑋, 𝑌〉(2nd ‘(𝐶
1stF 𝐷))〈𝑋, 𝑍〉)𝐹)) |
26 | | df-ov 6552 |
. . . 4
⊢ (( 1 ‘𝑋)(〈𝑋, 𝑌〉(2nd ‘(𝐶
1stF 𝐷))〈𝑋, 𝑍〉)𝐹) = ((〈𝑋, 𝑌〉(2nd ‘(𝐶
1stF 𝐷))〈𝑋, 𝑍〉)‘〈( 1 ‘𝑋), 𝐹〉) |
27 | 14, 13, 17 | xpcbas 16641 |
. . . . . 6
⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷)) |
28 | | eqid 2610 |
. . . . . 6
⊢ (Hom
‘(𝐶
×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷)) |
29 | | opelxpi 5072 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐴 × 𝐵)) |
30 | 18, 20, 29 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝐴 × 𝐵)) |
31 | | opelxpi 5072 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑍 ∈ 𝐵) → 〈𝑋, 𝑍〉 ∈ (𝐴 × 𝐵)) |
32 | 18, 23, 31 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → 〈𝑋, 𝑍〉 ∈ (𝐴 × 𝐵)) |
33 | 14, 27, 28, 3, 4, 15, 30, 32 | 1stf2 16656 |
. . . . 5
⊢ (𝜑 → (〈𝑋, 𝑌〉(2nd ‘(𝐶
1stF 𝐷))〈𝑋, 𝑍〉) = (1st ↾
(〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑍〉))) |
34 | 33 | fveq1d 6105 |
. . . 4
⊢ (𝜑 → ((〈𝑋, 𝑌〉(2nd ‘(𝐶
1stF 𝐷))〈𝑋, 𝑍〉)‘〈( 1 ‘𝑋), 𝐹〉) = ((1st ↾
(〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑍〉))‘〈( 1 ‘𝑋), 𝐹〉)) |
35 | 26, 34 | syl5eq 2656 |
. . 3
⊢ (𝜑 → (( 1 ‘𝑋)(〈𝑋, 𝑌〉(2nd ‘(𝐶
1stF 𝐷))〈𝑋, 𝑍〉)𝐹) = ((1st ↾ (〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑍〉))‘〈( 1 ‘𝑋), 𝐹〉)) |
36 | | eqid 2610 |
. . . . . . 7
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
37 | 13, 36, 22, 3, 18 | catidcl 16166 |
. . . . . 6
⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋)) |
38 | | opelxpi 5072 |
. . . . . 6
⊢ ((( 1 ‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝐹 ∈ (𝑌𝐽𝑍)) → 〈( 1 ‘𝑋), 𝐹〉 ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑌𝐽𝑍))) |
39 | 37, 24, 38 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → 〈( 1 ‘𝑋), 𝐹〉 ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑌𝐽𝑍))) |
40 | 14, 13, 17, 36, 21, 18, 20, 18, 23, 28 | xpchom2 16649 |
. . . . 5
⊢ (𝜑 → (〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑍〉) = ((𝑋(Hom ‘𝐶)𝑋) × (𝑌𝐽𝑍))) |
41 | 39, 40 | eleqtrrd 2691 |
. . . 4
⊢ (𝜑 → 〈( 1 ‘𝑋), 𝐹〉 ∈ (〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑍〉)) |
42 | | fvres 6117 |
. . . 4
⊢ (〈(
1
‘𝑋), 𝐹〉 ∈ (〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑍〉) → ((1st ↾
(〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑍〉))‘〈( 1 ‘𝑋), 𝐹〉) = (1st ‘〈(
1
‘𝑋), 𝐹〉)) |
43 | 41, 42 | syl 17 |
. . 3
⊢ (𝜑 → ((1st ↾
(〈𝑋, 𝑌〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑍〉))‘〈( 1 ‘𝑋), 𝐹〉) = (1st ‘〈(
1
‘𝑋), 𝐹〉)) |
44 | | op1stg 7071 |
. . . 4
⊢ ((( 1 ‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝐹 ∈ (𝑌𝐽𝑍)) → (1st ‘〈(
1
‘𝑋), 𝐹〉) = ( 1 ‘𝑋)) |
45 | 37, 24, 44 | syl2anc 691 |
. . 3
⊢ (𝜑 → (1st
‘〈( 1 ‘𝑋), 𝐹〉) = ( 1 ‘𝑋)) |
46 | 35, 43, 45 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → (( 1 ‘𝑋)(〈𝑋, 𝑌〉(2nd ‘(𝐶
1stF 𝐷))〈𝑋, 𝑍〉)𝐹) = ( 1 ‘𝑋)) |
47 | 11, 25, 46 | 3eqtrd 2648 |
1
⊢ (𝜑 → ((𝑌(2nd ‘𝐾)𝑍)‘𝐹) = ( 1 ‘𝑋)) |