Proof of Theorem yon12
Step | Hyp | Ref
| Expression |
1 | | yon11.y |
. . . . . . . . . 10
⊢ 𝑌 = (Yon‘𝐶) |
2 | | yon11.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ Cat) |
3 | | eqid 2610 |
. . . . . . . . . 10
⊢
(oppCat‘𝐶) =
(oppCat‘𝐶) |
4 | | eqid 2610 |
. . . . . . . . . 10
⊢
(HomF‘(oppCat‘𝐶)) =
(HomF‘(oppCat‘𝐶)) |
5 | 1, 2, 3, 4 | yonval 16724 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 = (〈𝐶, (oppCat‘𝐶)〉 curryF
(HomF‘(oppCat‘𝐶)))) |
6 | 5 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘𝑌) = (1st
‘(〈𝐶,
(oppCat‘𝐶)〉
curryF (HomF‘(oppCat‘𝐶))))) |
7 | 6 | fveq1d 6105 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘𝑌)‘𝑋) = ((1st
‘(〈𝐶,
(oppCat‘𝐶)〉
curryF (HomF‘(oppCat‘𝐶))))‘𝑋)) |
8 | 7 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 → (2nd
‘((1st ‘𝑌)‘𝑋)) = (2nd ‘((1st
‘(〈𝐶,
(oppCat‘𝐶)〉
curryF (HomF‘(oppCat‘𝐶))))‘𝑋))) |
9 | 8 | oveqd 6566 |
. . . . 5
⊢ (𝜑 → (𝑍(2nd ‘((1st
‘𝑌)‘𝑋))𝑊) = (𝑍(2nd ‘((1st
‘(〈𝐶,
(oppCat‘𝐶)〉
curryF (HomF‘(oppCat‘𝐶))))‘𝑋))𝑊)) |
10 | 9 | fveq1d 6105 |
. . . 4
⊢ (𝜑 → ((𝑍(2nd ‘((1st
‘𝑌)‘𝑋))𝑊)‘𝐹) = ((𝑍(2nd ‘((1st
‘(〈𝐶,
(oppCat‘𝐶)〉
curryF (HomF‘(oppCat‘𝐶))))‘𝑋))𝑊)‘𝐹)) |
11 | | eqid 2610 |
. . . . 5
⊢
(〈𝐶,
(oppCat‘𝐶)〉
curryF (HomF‘(oppCat‘𝐶))) = (〈𝐶, (oppCat‘𝐶)〉 curryF
(HomF‘(oppCat‘𝐶))) |
12 | | yon11.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐶) |
13 | 3 | oppccat 16205 |
. . . . . 6
⊢ (𝐶 ∈ Cat →
(oppCat‘𝐶) ∈
Cat) |
14 | 2, 13 | syl 17 |
. . . . 5
⊢ (𝜑 → (oppCat‘𝐶) ∈ Cat) |
15 | | eqid 2610 |
. . . . . 6
⊢
(SetCat‘ran (Homf ‘𝐶)) = (SetCat‘ran
(Homf ‘𝐶)) |
16 | | fvex 6113 |
. . . . . . . 8
⊢
(Homf ‘𝐶) ∈ V |
17 | 16 | rnex 6992 |
. . . . . . 7
⊢ ran
(Homf ‘𝐶) ∈ V |
18 | 17 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ran
(Homf ‘𝐶) ∈ V) |
19 | | ssid 3587 |
. . . . . . 7
⊢ ran
(Homf ‘𝐶) ⊆ ran (Homf
‘𝐶) |
20 | 19 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ran
(Homf ‘𝐶) ⊆ ran (Homf
‘𝐶)) |
21 | 3, 4, 15, 2, 18, 20 | oppchofcl 16723 |
. . . . 5
⊢ (𝜑 →
(HomF‘(oppCat‘𝐶)) ∈ ((𝐶 ×c
(oppCat‘𝐶)) Func
(SetCat‘ran (Homf ‘𝐶)))) |
22 | 3, 12 | oppcbas 16201 |
. . . . 5
⊢ 𝐵 =
(Base‘(oppCat‘𝐶)) |
23 | | yon11.p |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
24 | | eqid 2610 |
. . . . 5
⊢
((1st ‘(〈𝐶, (oppCat‘𝐶)〉 curryF
(HomF‘(oppCat‘𝐶))))‘𝑋) = ((1st ‘(〈𝐶, (oppCat‘𝐶)〉 curryF
(HomF‘(oppCat‘𝐶))))‘𝑋) |
25 | | yon11.z |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
26 | | eqid 2610 |
. . . . 5
⊢ (Hom
‘(oppCat‘𝐶)) =
(Hom ‘(oppCat‘𝐶)) |
27 | | eqid 2610 |
. . . . 5
⊢
(Id‘𝐶) =
(Id‘𝐶) |
28 | | yon12.w |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ 𝐵) |
29 | | yon12.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝑊𝐻𝑍)) |
30 | | yon11.h |
. . . . . . 7
⊢ 𝐻 = (Hom ‘𝐶) |
31 | 30, 3 | oppchom 16198 |
. . . . . 6
⊢ (𝑍(Hom ‘(oppCat‘𝐶))𝑊) = (𝑊𝐻𝑍) |
32 | 29, 31 | syl6eleqr 2699 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑍(Hom ‘(oppCat‘𝐶))𝑊)) |
33 | 11, 12, 2, 14, 21, 22, 23, 24, 25, 26, 27, 28, 32 | curf12 16690 |
. . . 4
⊢ (𝜑 → ((𝑍(2nd ‘((1st
‘(〈𝐶,
(oppCat‘𝐶)〉
curryF (HomF‘(oppCat‘𝐶))))‘𝑋))𝑊)‘𝐹) = (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑍〉(2nd
‘(HomF‘(oppCat‘𝐶)))〈𝑋, 𝑊〉)𝐹)) |
34 | 10, 33 | eqtrd 2644 |
. . 3
⊢ (𝜑 → ((𝑍(2nd ‘((1st
‘𝑌)‘𝑋))𝑊)‘𝐹) = (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑍〉(2nd
‘(HomF‘(oppCat‘𝐶)))〈𝑋, 𝑊〉)𝐹)) |
35 | 34 | fveq1d 6105 |
. 2
⊢ (𝜑 → (((𝑍(2nd ‘((1st
‘𝑌)‘𝑋))𝑊)‘𝐹)‘𝐺) = ((((Id‘𝐶)‘𝑋)(〈𝑋, 𝑍〉(2nd
‘(HomF‘(oppCat‘𝐶)))〈𝑋, 𝑊〉)𝐹)‘𝐺)) |
36 | | eqid 2610 |
. . 3
⊢
(comp‘(oppCat‘𝐶)) = (comp‘(oppCat‘𝐶)) |
37 | 12, 30, 27, 2, 23 | catidcl 16166 |
. . . 4
⊢ (𝜑 → ((Id‘𝐶)‘𝑋) ∈ (𝑋𝐻𝑋)) |
38 | 30, 3 | oppchom 16198 |
. . . 4
⊢ (𝑋(Hom ‘(oppCat‘𝐶))𝑋) = (𝑋𝐻𝑋) |
39 | 37, 38 | syl6eleqr 2699 |
. . 3
⊢ (𝜑 → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘(oppCat‘𝐶))𝑋)) |
40 | | yon12.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ (𝑍𝐻𝑋)) |
41 | 30, 3 | oppchom 16198 |
. . . 4
⊢ (𝑋(Hom ‘(oppCat‘𝐶))𝑍) = (𝑍𝐻𝑋) |
42 | 40, 41 | syl6eleqr 2699 |
. . 3
⊢ (𝜑 → 𝐺 ∈ (𝑋(Hom ‘(oppCat‘𝐶))𝑍)) |
43 | 4, 14, 22, 26, 23, 25, 23, 28, 36, 39, 32, 42 | hof2 16720 |
. 2
⊢ (𝜑 → ((((Id‘𝐶)‘𝑋)(〈𝑋, 𝑍〉(2nd
‘(HomF‘(oppCat‘𝐶)))〈𝑋, 𝑊〉)𝐹)‘𝐺) = ((𝐹(〈𝑋, 𝑍〉(comp‘(oppCat‘𝐶))𝑊)𝐺)(〈𝑋, 𝑋〉(comp‘(oppCat‘𝐶))𝑊)((Id‘𝐶)‘𝑋))) |
44 | | yon12.x |
. . . . 5
⊢ · =
(comp‘𝐶) |
45 | 12, 44, 3, 23, 25, 28 | oppcco 16200 |
. . . 4
⊢ (𝜑 → (𝐹(〈𝑋, 𝑍〉(comp‘(oppCat‘𝐶))𝑊)𝐺) = (𝐺(〈𝑊, 𝑍〉 · 𝑋)𝐹)) |
46 | 45 | oveq1d 6564 |
. . 3
⊢ (𝜑 → ((𝐹(〈𝑋, 𝑍〉(comp‘(oppCat‘𝐶))𝑊)𝐺)(〈𝑋, 𝑋〉(comp‘(oppCat‘𝐶))𝑊)((Id‘𝐶)‘𝑋)) = ((𝐺(〈𝑊, 𝑍〉 · 𝑋)𝐹)(〈𝑋, 𝑋〉(comp‘(oppCat‘𝐶))𝑊)((Id‘𝐶)‘𝑋))) |
47 | 12, 44, 3, 23, 23, 28 | oppcco 16200 |
. . 3
⊢ (𝜑 → ((𝐺(〈𝑊, 𝑍〉 · 𝑋)𝐹)(〈𝑋, 𝑋〉(comp‘(oppCat‘𝐶))𝑊)((Id‘𝐶)‘𝑋)) = (((Id‘𝐶)‘𝑋)(〈𝑊, 𝑋〉 · 𝑋)(𝐺(〈𝑊, 𝑍〉 · 𝑋)𝐹))) |
48 | 12, 30, 44, 2, 28, 25, 23, 29, 40 | catcocl 16169 |
. . . 4
⊢ (𝜑 → (𝐺(〈𝑊, 𝑍〉 · 𝑋)𝐹) ∈ (𝑊𝐻𝑋)) |
49 | 12, 30, 27, 2, 28, 44, 23, 48 | catlid 16167 |
. . 3
⊢ (𝜑 → (((Id‘𝐶)‘𝑋)(〈𝑊, 𝑋〉 · 𝑋)(𝐺(〈𝑊, 𝑍〉 · 𝑋)𝐹)) = (𝐺(〈𝑊, 𝑍〉 · 𝑋)𝐹)) |
50 | 46, 47, 49 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → ((𝐹(〈𝑋, 𝑍〉(comp‘(oppCat‘𝐶))𝑊)𝐺)(〈𝑋, 𝑋〉(comp‘(oppCat‘𝐶))𝑊)((Id‘𝐶)‘𝑋)) = (𝐺(〈𝑊, 𝑍〉 · 𝑋)𝐹)) |
51 | 35, 43, 50 | 3eqtrd 2648 |
1
⊢ (𝜑 → (((𝑍(2nd ‘((1st
‘𝑌)‘𝑋))𝑊)‘𝐹)‘𝐺) = (𝐺(〈𝑊, 𝑍〉 · 𝑋)𝐹)) |