Proof of Theorem yonedalem22
Step | Hyp | Ref
| Expression |
1 | | yoneda.z |
. . . . . . 7
⊢ 𝑍 = (𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂))) |
2 | 1 | fveq2i 6194 |
. . . . . 6
⊢
(2nd ‘𝑍) = (2nd ‘(𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))) |
3 | 2 | oveqi 6663 |
. . . . 5
⊢
(〈𝐹, 𝑋〉(2nd
‘𝑍)〈𝐺, 𝑃〉) = (〈𝐹, 𝑋〉(2nd ‘(𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂))))〈𝐺, 𝑃〉) |
4 | 3 | oveqi 6663 |
. . . 4
⊢ (𝐴(〈𝐹, 𝑋〉(2nd ‘𝑍)〈𝐺, 𝑃〉)𝐾) = (𝐴(〈𝐹, 𝑋〉(2nd ‘(𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂))))〈𝐺, 𝑃〉)𝐾) |
5 | | df-ov 6653 |
. . . 4
⊢ (𝐴(〈𝐹, 𝑋〉(2nd ‘(𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂))))〈𝐺, 𝑃〉)𝐾) = ((〈𝐹, 𝑋〉(2nd ‘(𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂))))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) |
6 | 4, 5 | eqtri 2644 |
. . 3
⊢ (𝐴(〈𝐹, 𝑋〉(2nd ‘𝑍)〈𝐺, 𝑃〉)𝐾) = ((〈𝐹, 𝑋〉(2nd ‘(𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂))))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) |
7 | | eqid 2622 |
. . . . 5
⊢ (𝑄 ×c
𝑂) = (𝑄 ×c 𝑂) |
8 | | yoneda.q |
. . . . . 6
⊢ 𝑄 = (𝑂 FuncCat 𝑆) |
9 | 8 | fucbas 16620 |
. . . . 5
⊢ (𝑂 Func 𝑆) = (Base‘𝑄) |
10 | | yoneda.o |
. . . . . 6
⊢ 𝑂 = (oppCat‘𝐶) |
11 | | yoneda.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
12 | 10, 11 | oppcbas 16378 |
. . . . 5
⊢ 𝐵 = (Base‘𝑂) |
13 | 7, 9, 12 | xpcbas 16818 |
. . . 4
⊢ ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂)) |
14 | | eqid 2622 |
. . . . 5
⊢
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)) = ((〈(1st
‘𝑌), tpos
(2nd ‘𝑌)〉 ∘func (𝑄
2ndF 𝑂)) 〈,〉F (𝑄
1stF 𝑂)) |
15 | | eqid 2622 |
. . . . 5
⊢
((oppCat‘𝑄)
×c 𝑄) = ((oppCat‘𝑄) ×c 𝑄) |
16 | | yoneda.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ Cat) |
17 | 10 | oppccat 16382 |
. . . . . . . . 9
⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑂 ∈ Cat) |
19 | | yoneda.w |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ 𝑊) |
20 | | yoneda.v |
. . . . . . . . . . 11
⊢ (𝜑 → (ran
(Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) |
21 | 20 | unssbd 3791 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ⊆ 𝑉) |
22 | 19, 21 | ssexd 4805 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ V) |
23 | | yoneda.s |
. . . . . . . . . 10
⊢ 𝑆 = (SetCat‘𝑈) |
24 | 23 | setccat 16735 |
. . . . . . . . 9
⊢ (𝑈 ∈ V → 𝑆 ∈ Cat) |
25 | 22, 24 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ Cat) |
26 | 8, 18, 25 | fuccat 16630 |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ Cat) |
27 | | eqid 2622 |
. . . . . . 7
⊢ (𝑄
2ndF 𝑂) = (𝑄 2ndF 𝑂) |
28 | 7, 26, 18, 27 | 2ndfcl 16838 |
. . . . . 6
⊢ (𝜑 → (𝑄 2ndF 𝑂) ∈ ((𝑄 ×c 𝑂) Func 𝑂)) |
29 | | eqid 2622 |
. . . . . . . 8
⊢
(oppCat‘𝑄) =
(oppCat‘𝑄) |
30 | | relfunc 16522 |
. . . . . . . . 9
⊢ Rel
(𝐶 Func 𝑄) |
31 | | yoneda.y |
. . . . . . . . . 10
⊢ 𝑌 = (Yon‘𝐶) |
32 | | yoneda.u |
. . . . . . . . . 10
⊢ (𝜑 → ran
(Homf ‘𝐶) ⊆ 𝑈) |
33 | 31, 16, 10, 23, 8, 22, 32 | yoncl 16902 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄)) |
34 | | 1st2ndbr 7217 |
. . . . . . . . 9
⊢ ((Rel
(𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st ‘𝑌)(𝐶 Func 𝑄)(2nd ‘𝑌)) |
35 | 30, 33, 34 | sylancr 695 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘𝑌)(𝐶 Func 𝑄)(2nd ‘𝑌)) |
36 | 10, 29, 35 | funcoppc 16535 |
. . . . . . 7
⊢ (𝜑 → (1st
‘𝑌)(𝑂 Func (oppCat‘𝑄))tpos (2nd ‘𝑌)) |
37 | | df-br 4654 |
. . . . . . 7
⊢
((1st ‘𝑌)(𝑂 Func (oppCat‘𝑄))tpos (2nd ‘𝑌) ↔ 〈(1st
‘𝑌), tpos
(2nd ‘𝑌)〉 ∈ (𝑂 Func (oppCat‘𝑄))) |
38 | 36, 37 | sylib 208 |
. . . . . 6
⊢ (𝜑 → 〈(1st
‘𝑌), tpos
(2nd ‘𝑌)〉 ∈ (𝑂 Func (oppCat‘𝑄))) |
39 | 28, 38 | cofucl 16548 |
. . . . 5
⊢ (𝜑 → (〈(1st
‘𝑌), tpos
(2nd ‘𝑌)〉 ∘func (𝑄
2ndF 𝑂)) ∈ ((𝑄 ×c 𝑂) Func (oppCat‘𝑄))) |
40 | | eqid 2622 |
. . . . . 6
⊢ (𝑄
1stF 𝑂) = (𝑄 1stF 𝑂) |
41 | 7, 26, 18, 40 | 1stfcl 16837 |
. . . . 5
⊢ (𝜑 → (𝑄 1stF 𝑂) ∈ ((𝑄 ×c 𝑂) Func 𝑄)) |
42 | 14, 15, 39, 41 | prfcl 16843 |
. . . 4
⊢ (𝜑 → ((〈(1st
‘𝑌), tpos
(2nd ‘𝑌)〉 ∘func (𝑄
2ndF 𝑂)) 〈,〉F (𝑄
1stF 𝑂)) ∈ ((𝑄 ×c 𝑂) Func ((oppCat‘𝑄) ×c
𝑄))) |
43 | | yoneda.h |
. . . . 5
⊢ 𝐻 =
(HomF‘𝑄) |
44 | | yoneda.t |
. . . . 5
⊢ 𝑇 = (SetCat‘𝑉) |
45 | 20 | unssad 3790 |
. . . . 5
⊢ (𝜑 → ran
(Homf ‘𝑄) ⊆ 𝑉) |
46 | 43, 29, 44, 26, 19, 45 | hofcl 16899 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ (((oppCat‘𝑄) ×c 𝑄) Func 𝑇)) |
47 | | yonedalem21.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆)) |
48 | | yonedalem21.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
49 | | opelxpi 5148 |
. . . . 5
⊢ ((𝐹 ∈ (𝑂 Func 𝑆) ∧ 𝑋 ∈ 𝐵) → 〈𝐹, 𝑋〉 ∈ ((𝑂 Func 𝑆) × 𝐵)) |
50 | 47, 48, 49 | syl2anc 693 |
. . . 4
⊢ (𝜑 → 〈𝐹, 𝑋〉 ∈ ((𝑂 Func 𝑆) × 𝐵)) |
51 | | yonedalem22.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑆)) |
52 | | yonedalem22.p |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ 𝐵) |
53 | | opelxpi 5148 |
. . . . 5
⊢ ((𝐺 ∈ (𝑂 Func 𝑆) ∧ 𝑃 ∈ 𝐵) → 〈𝐺, 𝑃〉 ∈ ((𝑂 Func 𝑆) × 𝐵)) |
54 | 51, 52, 53 | syl2anc 693 |
. . . 4
⊢ (𝜑 → 〈𝐺, 𝑃〉 ∈ ((𝑂 Func 𝑆) × 𝐵)) |
55 | | eqid 2622 |
. . . 4
⊢ (Hom
‘(𝑄
×c 𝑂)) = (Hom ‘(𝑄 ×c 𝑂)) |
56 | | yonedalem22.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺)) |
57 | | yonedalem22.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋)) |
58 | | eqid 2622 |
. . . . . . . 8
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
59 | 58, 10 | oppchom 16375 |
. . . . . . 7
⊢ (𝑋(Hom ‘𝑂)𝑃) = (𝑃(Hom ‘𝐶)𝑋) |
60 | 57, 59 | syl6eleqr 2712 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃)) |
61 | | opelxpi 5148 |
. . . . . 6
⊢ ((𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺) ∧ 𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃)) → 〈𝐴, 𝐾〉 ∈ ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃))) |
62 | 56, 60, 61 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → 〈𝐴, 𝐾〉 ∈ ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃))) |
63 | | eqid 2622 |
. . . . . . 7
⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆) |
64 | 8, 63 | fuchom 16621 |
. . . . . 6
⊢ (𝑂 Nat 𝑆) = (Hom ‘𝑄) |
65 | | eqid 2622 |
. . . . . 6
⊢ (Hom
‘𝑂) = (Hom
‘𝑂) |
66 | 7, 9, 12, 64, 65, 47, 48, 51, 52, 55 | xpchom2 16826 |
. . . . 5
⊢ (𝜑 → (〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃))) |
67 | 62, 66 | eleqtrrd 2704 |
. . . 4
⊢ (𝜑 → 〈𝐴, 𝐾〉 ∈ (〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉)) |
68 | 13, 42, 46, 50, 54, 55, 67 | cofu2 16546 |
. . 3
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd ‘(𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂))))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = ((((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐹, 𝑋〉)(2nd ‘𝐻)((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐺, 𝑃〉))‘((〈𝐹, 𝑋〉(2nd
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉))) |
69 | 6, 68 | syl5eq 2668 |
. 2
⊢ (𝜑 → (𝐴(〈𝐹, 𝑋〉(2nd ‘𝑍)〈𝐺, 𝑃〉)𝐾) = ((((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐹, 𝑋〉)(2nd ‘𝐻)((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐺, 𝑃〉))‘((〈𝐹, 𝑋〉(2nd
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉))) |
70 | 14, 13, 55, 39, 41, 50 | prf1 16840 |
. . . . . 6
⊢ (𝜑 → ((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐹, 𝑋〉) = 〈((1st
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))‘〈𝐹, 𝑋〉), ((1st ‘(𝑄
1stF 𝑂))‘〈𝐹, 𝑋〉)〉) |
71 | 13, 28, 38, 50 | cofu1 16544 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))‘〈𝐹, 𝑋〉) = ((1st
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)‘((1st
‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉))) |
72 | | fvex 6201 |
. . . . . . . . . . 11
⊢
(1st ‘𝑌) ∈ V |
73 | | fvex 6201 |
. . . . . . . . . . . 12
⊢
(2nd ‘𝑌) ∈ V |
74 | 73 | tposex 7386 |
. . . . . . . . . . 11
⊢ tpos
(2nd ‘𝑌)
∈ V |
75 | 72, 74 | op1st 7176 |
. . . . . . . . . 10
⊢
(1st ‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉) = (1st
‘𝑌) |
76 | 75 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉) = (1st
‘𝑌)) |
77 | 7, 13, 55, 26, 18, 27, 50 | 2ndf1 16835 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st
‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉) = (2nd ‘〈𝐹, 𝑋〉)) |
78 | | op2ndg 7181 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝑂 Func 𝑆) ∧ 𝑋 ∈ 𝐵) → (2nd ‘〈𝐹, 𝑋〉) = 𝑋) |
79 | 47, 48, 78 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → (2nd
‘〈𝐹, 𝑋〉) = 𝑋) |
80 | 77, 79 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉) = 𝑋) |
81 | 76, 80 | fveq12d 6197 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)‘((1st
‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉)) = ((1st ‘𝑌)‘𝑋)) |
82 | 71, 81 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))‘〈𝐹, 𝑋〉) = ((1st ‘𝑌)‘𝑋)) |
83 | 7, 13, 55, 26, 18, 40, 50 | 1stf1 16832 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝑄
1stF 𝑂))‘〈𝐹, 𝑋〉) = (1st ‘〈𝐹, 𝑋〉)) |
84 | | op1stg 7180 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑂 Func 𝑆) ∧ 𝑋 ∈ 𝐵) → (1st ‘〈𝐹, 𝑋〉) = 𝐹) |
85 | 47, 48, 84 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘〈𝐹, 𝑋〉) = 𝐹) |
86 | 83, 85 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝑄
1stF 𝑂))‘〈𝐹, 𝑋〉) = 𝐹) |
87 | 82, 86 | opeq12d 4410 |
. . . . . 6
⊢ (𝜑 → 〈((1st
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))‘〈𝐹, 𝑋〉), ((1st ‘(𝑄
1stF 𝑂))‘〈𝐹, 𝑋〉)〉 = 〈((1st
‘𝑌)‘𝑋), 𝐹〉) |
88 | 70, 87 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → ((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐹, 𝑋〉) = 〈((1st
‘𝑌)‘𝑋), 𝐹〉) |
89 | 14, 13, 55, 39, 41, 54 | prf1 16840 |
. . . . . 6
⊢ (𝜑 → ((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐺, 𝑃〉) = 〈((1st
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))‘〈𝐺, 𝑃〉), ((1st ‘(𝑄
1stF 𝑂))‘〈𝐺, 𝑃〉)〉) |
90 | 13, 28, 38, 54 | cofu1 16544 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))‘〈𝐺, 𝑃〉) = ((1st
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)‘((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉))) |
91 | 7, 13, 55, 26, 18, 27, 54 | 2ndf1 16835 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉) = (2nd ‘〈𝐺, 𝑃〉)) |
92 | | op2ndg 7181 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ (𝑂 Func 𝑆) ∧ 𝑃 ∈ 𝐵) → (2nd ‘〈𝐺, 𝑃〉) = 𝑃) |
93 | 51, 52, 92 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → (2nd
‘〈𝐺, 𝑃〉) = 𝑃) |
94 | 91, 93 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉) = 𝑃) |
95 | 76, 94 | fveq12d 6197 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)‘((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)) = ((1st ‘𝑌)‘𝑃)) |
96 | 90, 95 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))‘〈𝐺, 𝑃〉) = ((1st ‘𝑌)‘𝑃)) |
97 | 7, 13, 55, 26, 18, 40, 54 | 1stf1 16832 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝑄
1stF 𝑂))‘〈𝐺, 𝑃〉) = (1st ‘〈𝐺, 𝑃〉)) |
98 | | op1stg 7180 |
. . . . . . . . 9
⊢ ((𝐺 ∈ (𝑂 Func 𝑆) ∧ 𝑃 ∈ 𝐵) → (1st ‘〈𝐺, 𝑃〉) = 𝐺) |
99 | 51, 52, 98 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘〈𝐺, 𝑃〉) = 𝐺) |
100 | 97, 99 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝑄
1stF 𝑂))‘〈𝐺, 𝑃〉) = 𝐺) |
101 | 96, 100 | opeq12d 4410 |
. . . . . 6
⊢ (𝜑 → 〈((1st
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))‘〈𝐺, 𝑃〉), ((1st ‘(𝑄
1stF 𝑂))‘〈𝐺, 𝑃〉)〉 = 〈((1st
‘𝑌)‘𝑃), 𝐺〉) |
102 | 89, 101 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → ((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐺, 𝑃〉) = 〈((1st
‘𝑌)‘𝑃), 𝐺〉) |
103 | 88, 102 | oveq12d 6668 |
. . . 4
⊢ (𝜑 → (((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐹, 𝑋〉)(2nd ‘𝐻)((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐺, 𝑃〉)) = (〈((1st
‘𝑌)‘𝑋), 𝐹〉(2nd ‘𝐻)〈((1st
‘𝑌)‘𝑃), 𝐺〉)) |
104 | 14, 13, 55, 39, 41, 50, 54, 67 | prf2 16842 |
. . . . 5
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = 〈((〈𝐹, 𝑋〉(2nd
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉), ((〈𝐹, 𝑋〉(2nd ‘(𝑄
1stF 𝑂))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉)〉) |
105 | 13, 28, 38, 50, 54, 55, 67 | cofu2 16546 |
. . . . . . 7
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = ((((1st ‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉)(2nd
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉))‘((〈𝐹, 𝑋〉(2nd ‘(𝑄
2ndF 𝑂))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉))) |
106 | 72, 74 | op2nd 7177 |
. . . . . . . . . . 11
⊢
(2nd ‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉) = tpos (2nd
‘𝑌) |
107 | 106 | oveqi 6663 |
. . . . . . . . . 10
⊢
(((1st ‘(𝑄 2ndF 𝑂))‘〈𝐹, 𝑋〉)(2nd
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)) = (((1st ‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉)tpos (2nd ‘𝑌)((1st ‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)) |
108 | | ovtpos 7367 |
. . . . . . . . . 10
⊢
(((1st ‘(𝑄 2ndF 𝑂))‘〈𝐹, 𝑋〉)tpos (2nd ‘𝑌)((1st ‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)) = (((1st ‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)(2nd ‘𝑌)((1st ‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉)) |
109 | 107, 108 | eqtri 2644 |
. . . . . . . . 9
⊢
(((1st ‘(𝑄 2ndF 𝑂))‘〈𝐹, 𝑋〉)(2nd
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)) = (((1st ‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)(2nd ‘𝑌)((1st ‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉)) |
110 | 94, 80 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝜑 → (((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)(2nd ‘𝑌)((1st ‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉)) = (𝑃(2nd ‘𝑌)𝑋)) |
111 | 109, 110 | syl5eq 2668 |
. . . . . . . 8
⊢ (𝜑 → (((1st
‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉)(2nd
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)) = (𝑃(2nd ‘𝑌)𝑋)) |
112 | 7, 13, 55, 26, 18, 27, 50, 54 | 2ndf2 16836 |
. . . . . . . . . 10
⊢ (𝜑 → (〈𝐹, 𝑋〉(2nd ‘(𝑄
2ndF 𝑂))〈𝐺, 𝑃〉) = (2nd ↾
(〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉))) |
113 | 112 | fveq1d 6193 |
. . . . . . . . 9
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd ‘(𝑄
2ndF 𝑂))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = ((2nd ↾
(〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉))‘〈𝐴, 𝐾〉)) |
114 | | fvres 6207 |
. . . . . . . . . 10
⊢
(〈𝐴, 𝐾〉 ∈ (〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉) → ((2nd ↾
(〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉))‘〈𝐴, 𝐾〉) = (2nd ‘〈𝐴, 𝐾〉)) |
115 | 67, 114 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((2nd ↾
(〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉))‘〈𝐴, 𝐾〉) = (2nd ‘〈𝐴, 𝐾〉)) |
116 | | op2ndg 7181 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺) ∧ 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋)) → (2nd ‘〈𝐴, 𝐾〉) = 𝐾) |
117 | 56, 57, 116 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘〈𝐴, 𝐾〉) = 𝐾) |
118 | 113, 115,
117 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd ‘(𝑄
2ndF 𝑂))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = 𝐾) |
119 | 111, 118 | fveq12d 6197 |
. . . . . . 7
⊢ (𝜑 → ((((1st
‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉)(2nd
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉))‘((〈𝐹, 𝑋〉(2nd ‘(𝑄
2ndF 𝑂))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉)) = ((𝑃(2nd ‘𝑌)𝑋)‘𝐾)) |
120 | 105, 119 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = ((𝑃(2nd ‘𝑌)𝑋)‘𝐾)) |
121 | 7, 13, 55, 26, 18, 40, 50, 54 | 1stf2 16833 |
. . . . . . . 8
⊢ (𝜑 → (〈𝐹, 𝑋〉(2nd ‘(𝑄
1stF 𝑂))〈𝐺, 𝑃〉) = (1st ↾
(〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉))) |
122 | 121 | fveq1d 6193 |
. . . . . . 7
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd ‘(𝑄
1stF 𝑂))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = ((1st ↾
(〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉))‘〈𝐴, 𝐾〉)) |
123 | | fvres 6207 |
. . . . . . . 8
⊢
(〈𝐴, 𝐾〉 ∈ (〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉) → ((1st ↾
(〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉))‘〈𝐴, 𝐾〉) = (1st ‘〈𝐴, 𝐾〉)) |
124 | 67, 123 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((1st ↾
(〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉))‘〈𝐴, 𝐾〉) = (1st ‘〈𝐴, 𝐾〉)) |
125 | | op1stg 7180 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺) ∧ 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋)) → (1st ‘〈𝐴, 𝐾〉) = 𝐴) |
126 | 56, 57, 125 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (1st
‘〈𝐴, 𝐾〉) = 𝐴) |
127 | 122, 124,
126 | 3eqtrd 2660 |
. . . . . 6
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd ‘(𝑄
1stF 𝑂))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = 𝐴) |
128 | 120, 127 | opeq12d 4410 |
. . . . 5
⊢ (𝜑 → 〈((〈𝐹, 𝑋〉(2nd
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉), ((〈𝐹, 𝑋〉(2nd ‘(𝑄
1stF 𝑂))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉)〉 = 〈((𝑃(2nd ‘𝑌)𝑋)‘𝐾), 𝐴〉) |
129 | 104, 128 | eqtrd 2656 |
. . . 4
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = 〈((𝑃(2nd ‘𝑌)𝑋)‘𝐾), 𝐴〉) |
130 | 103, 129 | fveq12d 6197 |
. . 3
⊢ (𝜑 → ((((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐹, 𝑋〉)(2nd ‘𝐻)((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐺, 𝑃〉))‘((〈𝐹, 𝑋〉(2nd
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉)) = ((〈((1st
‘𝑌)‘𝑋), 𝐹〉(2nd ‘𝐻)〈((1st
‘𝑌)‘𝑃), 𝐺〉)‘〈((𝑃(2nd ‘𝑌)𝑋)‘𝐾), 𝐴〉)) |
131 | | df-ov 6653 |
. . 3
⊢ (((𝑃(2nd ‘𝑌)𝑋)‘𝐾)(〈((1st ‘𝑌)‘𝑋), 𝐹〉(2nd ‘𝐻)〈((1st
‘𝑌)‘𝑃), 𝐺〉)𝐴) = ((〈((1st ‘𝑌)‘𝑋), 𝐹〉(2nd ‘𝐻)〈((1st
‘𝑌)‘𝑃), 𝐺〉)‘〈((𝑃(2nd ‘𝑌)𝑋)‘𝐾), 𝐴〉) |
132 | 130, 131 | syl6eqr 2674 |
. 2
⊢ (𝜑 → ((((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐹, 𝑋〉)(2nd ‘𝐻)((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐺, 𝑃〉))‘((〈𝐹, 𝑋〉(2nd
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉)) = (((𝑃(2nd ‘𝑌)𝑋)‘𝐾)(〈((1st ‘𝑌)‘𝑋), 𝐹〉(2nd ‘𝐻)〈((1st
‘𝑌)‘𝑃), 𝐺〉)𝐴)) |
133 | 69, 132 | eqtrd 2656 |
1
⊢ (𝜑 → (𝐴(〈𝐹, 𝑋〉(2nd ‘𝑍)〈𝐺, 𝑃〉)𝐾) = (((𝑃(2nd ‘𝑌)𝑋)‘𝐾)(〈((1st ‘𝑌)‘𝑋), 𝐹〉(2nd ‘𝐻)〈((1st
‘𝑌)‘𝑃), 𝐺〉)𝐴)) |