Proof of Theorem yonedalem22
| Step | Hyp | Ref
| Expression |
| 1 | | yoneda.z |
. . . . . . 7
⊢ 𝑍 = (𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂))) |
| 2 | 1 | fveq2i 6909 |
. . . . . 6
⊢
(2nd ‘𝑍) = (2nd ‘(𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))) |
| 3 | 2 | oveqi 7444 |
. . . . 5
⊢
(〈𝐹, 𝑋〉(2nd
‘𝑍)〈𝐺, 𝑃〉) = (〈𝐹, 𝑋〉(2nd ‘(𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂))))〈𝐺, 𝑃〉) |
| 4 | 3 | oveqi 7444 |
. . . 4
⊢ (𝐴(〈𝐹, 𝑋〉(2nd ‘𝑍)〈𝐺, 𝑃〉)𝐾) = (𝐴(〈𝐹, 𝑋〉(2nd ‘(𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂))))〈𝐺, 𝑃〉)𝐾) |
| 5 | | df-ov 7434 |
. . . 4
⊢ (𝐴(〈𝐹, 𝑋〉(2nd ‘(𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂))))〈𝐺, 𝑃〉)𝐾) = ((〈𝐹, 𝑋〉(2nd ‘(𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂))))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) |
| 6 | 4, 5 | eqtri 2765 |
. . 3
⊢ (𝐴(〈𝐹, 𝑋〉(2nd ‘𝑍)〈𝐺, 𝑃〉)𝐾) = ((〈𝐹, 𝑋〉(2nd ‘(𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂))))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) |
| 7 | | eqid 2737 |
. . . . 5
⊢ (𝑄 ×c
𝑂) = (𝑄 ×c 𝑂) |
| 8 | | yoneda.q |
. . . . . 6
⊢ 𝑄 = (𝑂 FuncCat 𝑆) |
| 9 | 8 | fucbas 18008 |
. . . . 5
⊢ (𝑂 Func 𝑆) = (Base‘𝑄) |
| 10 | | yoneda.o |
. . . . . 6
⊢ 𝑂 = (oppCat‘𝐶) |
| 11 | | yoneda.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
| 12 | 10, 11 | oppcbas 17761 |
. . . . 5
⊢ 𝐵 = (Base‘𝑂) |
| 13 | 7, 9, 12 | xpcbas 18223 |
. . . 4
⊢ ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂)) |
| 14 | | eqid 2737 |
. . . . 5
⊢
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)) = ((〈(1st
‘𝑌), tpos
(2nd ‘𝑌)〉 ∘func (𝑄
2ndF 𝑂)) 〈,〉F (𝑄
1stF 𝑂)) |
| 15 | | eqid 2737 |
. . . . 5
⊢
((oppCat‘𝑄)
×c 𝑄) = ((oppCat‘𝑄) ×c 𝑄) |
| 16 | | yoneda.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 17 | 10 | oppccat 17765 |
. . . . . . . . 9
⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat) |
| 18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑂 ∈ Cat) |
| 19 | | yoneda.w |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ 𝑊) |
| 20 | | yoneda.v |
. . . . . . . . . . 11
⊢ (𝜑 → (ran
(Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) |
| 21 | 20 | unssbd 4194 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ⊆ 𝑉) |
| 22 | 19, 21 | ssexd 5324 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ V) |
| 23 | | yoneda.s |
. . . . . . . . . 10
⊢ 𝑆 = (SetCat‘𝑈) |
| 24 | 23 | setccat 18130 |
. . . . . . . . 9
⊢ (𝑈 ∈ V → 𝑆 ∈ Cat) |
| 25 | 22, 24 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ Cat) |
| 26 | 8, 18, 25 | fuccat 18018 |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ Cat) |
| 27 | | eqid 2737 |
. . . . . . 7
⊢ (𝑄
2ndF 𝑂) = (𝑄 2ndF 𝑂) |
| 28 | 7, 26, 18, 27 | 2ndfcl 18243 |
. . . . . 6
⊢ (𝜑 → (𝑄 2ndF 𝑂) ∈ ((𝑄 ×c 𝑂) Func 𝑂)) |
| 29 | | eqid 2737 |
. . . . . . . 8
⊢
(oppCat‘𝑄) =
(oppCat‘𝑄) |
| 30 | | relfunc 17907 |
. . . . . . . . 9
⊢ Rel
(𝐶 Func 𝑄) |
| 31 | | yoneda.y |
. . . . . . . . . 10
⊢ 𝑌 = (Yon‘𝐶) |
| 32 | | yoneda.u |
. . . . . . . . . 10
⊢ (𝜑 → ran
(Homf ‘𝐶) ⊆ 𝑈) |
| 33 | 31, 16, 10, 23, 8, 22, 32 | yoncl 18307 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄)) |
| 34 | | 1st2ndbr 8067 |
. . . . . . . . 9
⊢ ((Rel
(𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st ‘𝑌)(𝐶 Func 𝑄)(2nd ‘𝑌)) |
| 35 | 30, 33, 34 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘𝑌)(𝐶 Func 𝑄)(2nd ‘𝑌)) |
| 36 | 10, 29, 35 | funcoppc 17920 |
. . . . . . 7
⊢ (𝜑 → (1st
‘𝑌)(𝑂 Func (oppCat‘𝑄))tpos (2nd ‘𝑌)) |
| 37 | | df-br 5144 |
. . . . . . 7
⊢
((1st ‘𝑌)(𝑂 Func (oppCat‘𝑄))tpos (2nd ‘𝑌) ↔ 〈(1st
‘𝑌), tpos
(2nd ‘𝑌)〉 ∈ (𝑂 Func (oppCat‘𝑄))) |
| 38 | 36, 37 | sylib 218 |
. . . . . 6
⊢ (𝜑 → 〈(1st
‘𝑌), tpos
(2nd ‘𝑌)〉 ∈ (𝑂 Func (oppCat‘𝑄))) |
| 39 | 28, 38 | cofucl 17933 |
. . . . 5
⊢ (𝜑 → (〈(1st
‘𝑌), tpos
(2nd ‘𝑌)〉 ∘func (𝑄
2ndF 𝑂)) ∈ ((𝑄 ×c 𝑂) Func (oppCat‘𝑄))) |
| 40 | | eqid 2737 |
. . . . . 6
⊢ (𝑄
1stF 𝑂) = (𝑄 1stF 𝑂) |
| 41 | 7, 26, 18, 40 | 1stfcl 18242 |
. . . . 5
⊢ (𝜑 → (𝑄 1stF 𝑂) ∈ ((𝑄 ×c 𝑂) Func 𝑄)) |
| 42 | 14, 15, 39, 41 | prfcl 18248 |
. . . 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 4193 |
. . . . 5
⊢ (𝜑 → ran
(Homf ‘𝑄) ⊆ 𝑉) |
| 46 | 43, 29, 44, 26, 19, 45 | hofcl 18304 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ (((oppCat‘𝑄) ×c 𝑄) Func 𝑇)) |
| 47 | | yonedalem21.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆)) |
| 48 | | yonedalem21.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 49 | 47, 48 | opelxpd 5724 |
. . . 4
⊢ (𝜑 → 〈𝐹, 𝑋〉 ∈ ((𝑂 Func 𝑆) × 𝐵)) |
| 50 | | yonedalem22.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑆)) |
| 51 | | yonedalem22.p |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ 𝐵) |
| 52 | 50, 51 | opelxpd 5724 |
. . . 4
⊢ (𝜑 → 〈𝐺, 𝑃〉 ∈ ((𝑂 Func 𝑆) × 𝐵)) |
| 53 | | eqid 2737 |
. . . 4
⊢ (Hom
‘(𝑄
×c 𝑂)) = (Hom ‘(𝑄 ×c 𝑂)) |
| 54 | | yonedalem22.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺)) |
| 55 | | yonedalem22.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋)) |
| 56 | | eqid 2737 |
. . . . . . . 8
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 57 | 56, 10 | oppchom 17758 |
. . . . . . 7
⊢ (𝑋(Hom ‘𝑂)𝑃) = (𝑃(Hom ‘𝐶)𝑋) |
| 58 | 55, 57 | eleqtrrdi 2852 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃)) |
| 59 | 54, 58 | opelxpd 5724 |
. . . . 5
⊢ (𝜑 → 〈𝐴, 𝐾〉 ∈ ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃))) |
| 60 | | eqid 2737 |
. . . . . . 7
⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆) |
| 61 | 8, 60 | fuchom 18009 |
. . . . . 6
⊢ (𝑂 Nat 𝑆) = (Hom ‘𝑄) |
| 62 | | eqid 2737 |
. . . . . 6
⊢ (Hom
‘𝑂) = (Hom
‘𝑂) |
| 63 | 7, 9, 12, 61, 62, 47, 48, 50, 51, 53 | xpchom2 18231 |
. . . . 5
⊢ (𝜑 → (〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃))) |
| 64 | 59, 63 | eleqtrrd 2844 |
. . . 4
⊢ (𝜑 → 〈𝐴, 𝐾〉 ∈ (〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉)) |
| 65 | 13, 42, 46, 49, 52, 53, 64 | cofu2 17931 |
. . 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 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉))) |
| 66 | 6, 65 | eqtrid 2789 |
. 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 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉))) |
| 67 | 14, 13, 53, 39, 41, 49 | prf1 18245 |
. . . . . 6
⊢ (𝜑 → ((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐹, 𝑋〉) = 〈((1st
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))‘〈𝐹, 𝑋〉), ((1st ‘(𝑄
1stF 𝑂))‘〈𝐹, 𝑋〉)〉) |
| 68 | 13, 28, 38, 49 | cofu1 17929 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))‘〈𝐹, 𝑋〉) = ((1st
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)‘((1st
‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉))) |
| 69 | | fvex 6919 |
. . . . . . . . . . 11
⊢
(1st ‘𝑌) ∈ V |
| 70 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(2nd ‘𝑌) ∈ V |
| 71 | 70 | tposex 8285 |
. . . . . . . . . . 11
⊢ tpos
(2nd ‘𝑌)
∈ V |
| 72 | 69, 71 | op1st 8022 |
. . . . . . . . . 10
⊢
(1st ‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉) = (1st
‘𝑌) |
| 73 | 72 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉) = (1st
‘𝑌)) |
| 74 | 7, 13, 53, 26, 18, 27, 49 | 2ndf1 18240 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st
‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉) = (2nd ‘〈𝐹, 𝑋〉)) |
| 75 | | op2ndg 8027 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝑂 Func 𝑆) ∧ 𝑋 ∈ 𝐵) → (2nd ‘〈𝐹, 𝑋〉) = 𝑋) |
| 76 | 47, 48, 75 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (2nd
‘〈𝐹, 𝑋〉) = 𝑋) |
| 77 | 74, 76 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉) = 𝑋) |
| 78 | 73, 77 | fveq12d 6913 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)‘((1st
‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉)) = ((1st ‘𝑌)‘𝑋)) |
| 79 | 68, 78 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))‘〈𝐹, 𝑋〉) = ((1st ‘𝑌)‘𝑋)) |
| 80 | 7, 13, 53, 26, 18, 40, 49 | 1stf1 18237 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝑄
1stF 𝑂))‘〈𝐹, 𝑋〉) = (1st ‘〈𝐹, 𝑋〉)) |
| 81 | | op1stg 8026 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑂 Func 𝑆) ∧ 𝑋 ∈ 𝐵) → (1st ‘〈𝐹, 𝑋〉) = 𝐹) |
| 82 | 47, 48, 81 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘〈𝐹, 𝑋〉) = 𝐹) |
| 83 | 80, 82 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝑄
1stF 𝑂))‘〈𝐹, 𝑋〉) = 𝐹) |
| 84 | 79, 83 | opeq12d 4881 |
. . . . . 6
⊢ (𝜑 → 〈((1st
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))‘〈𝐹, 𝑋〉), ((1st ‘(𝑄
1stF 𝑂))‘〈𝐹, 𝑋〉)〉 = 〈((1st
‘𝑌)‘𝑋), 𝐹〉) |
| 85 | 67, 84 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → ((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐹, 𝑋〉) = 〈((1st
‘𝑌)‘𝑋), 𝐹〉) |
| 86 | 14, 13, 53, 39, 41, 52 | prf1 18245 |
. . . . . 6
⊢ (𝜑 → ((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐺, 𝑃〉) = 〈((1st
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))‘〈𝐺, 𝑃〉), ((1st ‘(𝑄
1stF 𝑂))‘〈𝐺, 𝑃〉)〉) |
| 87 | 13, 28, 38, 52 | cofu1 17929 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))‘〈𝐺, 𝑃〉) = ((1st
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)‘((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉))) |
| 88 | 7, 13, 53, 26, 18, 27, 52 | 2ndf1 18240 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉) = (2nd ‘〈𝐺, 𝑃〉)) |
| 89 | | op2ndg 8027 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ (𝑂 Func 𝑆) ∧ 𝑃 ∈ 𝐵) → (2nd ‘〈𝐺, 𝑃〉) = 𝑃) |
| 90 | 50, 51, 89 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (2nd
‘〈𝐺, 𝑃〉) = 𝑃) |
| 91 | 88, 90 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉) = 𝑃) |
| 92 | 73, 91 | fveq12d 6913 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)‘((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)) = ((1st ‘𝑌)‘𝑃)) |
| 93 | 87, 92 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))‘〈𝐺, 𝑃〉) = ((1st ‘𝑌)‘𝑃)) |
| 94 | 7, 13, 53, 26, 18, 40, 52 | 1stf1 18237 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(𝑄
1stF 𝑂))‘〈𝐺, 𝑃〉) = (1st ‘〈𝐺, 𝑃〉)) |
| 95 | | op1stg 8026 |
. . . . . . . . 9
⊢ ((𝐺 ∈ (𝑂 Func 𝑆) ∧ 𝑃 ∈ 𝐵) → (1st ‘〈𝐺, 𝑃〉) = 𝐺) |
| 96 | 50, 51, 95 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘〈𝐺, 𝑃〉) = 𝐺) |
| 97 | 94, 96 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(𝑄
1stF 𝑂))‘〈𝐺, 𝑃〉) = 𝐺) |
| 98 | 93, 97 | opeq12d 4881 |
. . . . . 6
⊢ (𝜑 → 〈((1st
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))‘〈𝐺, 𝑃〉), ((1st ‘(𝑄
1stF 𝑂))‘〈𝐺, 𝑃〉)〉 = 〈((1st
‘𝑌)‘𝑃), 𝐺〉) |
| 99 | 86, 98 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → ((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐺, 𝑃〉) = 〈((1st
‘𝑌)‘𝑃), 𝐺〉) |
| 100 | 85, 99 | oveq12d 7449 |
. . . 4
⊢ (𝜑 → (((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐹, 𝑋〉)(2nd ‘𝐻)((1st
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))‘〈𝐺, 𝑃〉)) = (〈((1st
‘𝑌)‘𝑋), 𝐹〉(2nd ‘𝐻)〈((1st
‘𝑌)‘𝑃), 𝐺〉)) |
| 101 | 14, 13, 53, 39, 41, 49, 52, 64 | prf2 18247 |
. . . . 5
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = 〈((〈𝐹, 𝑋〉(2nd
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉), ((〈𝐹, 𝑋〉(2nd ‘(𝑄
1stF 𝑂))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉)〉) |
| 102 | 13, 28, 38, 49, 52, 53, 64 | cofu2 17931 |
. . . . . . 7
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = ((((1st ‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉)(2nd
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉))‘((〈𝐹, 𝑋〉(2nd ‘(𝑄
2ndF 𝑂))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉))) |
| 103 | 69, 71 | op2nd 8023 |
. . . . . . . . . . 11
⊢
(2nd ‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉) = tpos (2nd
‘𝑌) |
| 104 | 103 | oveqi 7444 |
. . . . . . . . . 10
⊢
(((1st ‘(𝑄 2ndF 𝑂))‘〈𝐹, 𝑋〉)(2nd
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)) = (((1st ‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉)tpos (2nd ‘𝑌)((1st ‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)) |
| 105 | | ovtpos 8266 |
. . . . . . . . . 10
⊢
(((1st ‘(𝑄 2ndF 𝑂))‘〈𝐹, 𝑋〉)tpos (2nd ‘𝑌)((1st ‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)) = (((1st ‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)(2nd ‘𝑌)((1st ‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉)) |
| 106 | 104, 105 | eqtri 2765 |
. . . . . . . . 9
⊢
(((1st ‘(𝑄 2ndF 𝑂))‘〈𝐹, 𝑋〉)(2nd
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)) = (((1st ‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)(2nd ‘𝑌)((1st ‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉)) |
| 107 | 91, 77 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝜑 → (((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)(2nd ‘𝑌)((1st ‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉)) = (𝑃(2nd ‘𝑌)𝑋)) |
| 108 | 106, 107 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝜑 → (((1st
‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉)(2nd
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉)) = (𝑃(2nd ‘𝑌)𝑋)) |
| 109 | 7, 13, 53, 26, 18, 27, 49, 52 | 2ndf2 18241 |
. . . . . . . . . 10
⊢ (𝜑 → (〈𝐹, 𝑋〉(2nd ‘(𝑄
2ndF 𝑂))〈𝐺, 𝑃〉) = (2nd ↾
(〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉))) |
| 110 | 109 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd ‘(𝑄
2ndF 𝑂))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = ((2nd ↾
(〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉))‘〈𝐴, 𝐾〉)) |
| 111 | 64 | fvresd 6926 |
. . . . . . . . 9
⊢ (𝜑 → ((2nd ↾
(〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉))‘〈𝐴, 𝐾〉) = (2nd ‘〈𝐴, 𝐾〉)) |
| 112 | | op2ndg 8027 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺) ∧ 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋)) → (2nd ‘〈𝐴, 𝐾〉) = 𝐾) |
| 113 | 54, 55, 112 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘〈𝐴, 𝐾〉) = 𝐾) |
| 114 | 110, 111,
113 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd ‘(𝑄
2ndF 𝑂))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = 𝐾) |
| 115 | 108, 114 | fveq12d 6913 |
. . . . . . 7
⊢ (𝜑 → ((((1st
‘(𝑄
2ndF 𝑂))‘〈𝐹, 𝑋〉)(2nd
‘〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉)((1st
‘(𝑄
2ndF 𝑂))‘〈𝐺, 𝑃〉))‘((〈𝐹, 𝑋〉(2nd ‘(𝑄
2ndF 𝑂))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉)) = ((𝑃(2nd ‘𝑌)𝑋)‘𝐾)) |
| 116 | 102, 115 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = ((𝑃(2nd ‘𝑌)𝑋)‘𝐾)) |
| 117 | 7, 13, 53, 26, 18, 40, 49, 52 | 1stf2 18238 |
. . . . . . . 8
⊢ (𝜑 → (〈𝐹, 𝑋〉(2nd ‘(𝑄
1stF 𝑂))〈𝐺, 𝑃〉) = (1st ↾
(〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉))) |
| 118 | 117 | fveq1d 6908 |
. . . . . . 7
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd ‘(𝑄
1stF 𝑂))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = ((1st ↾
(〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉))‘〈𝐴, 𝐾〉)) |
| 119 | 64 | fvresd 6926 |
. . . . . . 7
⊢ (𝜑 → ((1st ↾
(〈𝐹, 𝑋〉(Hom ‘(𝑄 ×c 𝑂))〈𝐺, 𝑃〉))‘〈𝐴, 𝐾〉) = (1st ‘〈𝐴, 𝐾〉)) |
| 120 | | op1stg 8026 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺) ∧ 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋)) → (1st ‘〈𝐴, 𝐾〉) = 𝐴) |
| 121 | 54, 55, 120 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (1st
‘〈𝐴, 𝐾〉) = 𝐴) |
| 122 | 118, 119,
121 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd ‘(𝑄
1stF 𝑂))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = 𝐴) |
| 123 | 116, 122 | opeq12d 4881 |
. . . . 5
⊢ (𝜑 → 〈((〈𝐹, 𝑋〉(2nd
‘(〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉), ((〈𝐹, 𝑋〉(2nd ‘(𝑄
1stF 𝑂))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉)〉 = 〈((𝑃(2nd ‘𝑌)𝑋)‘𝐾), 𝐴〉) |
| 124 | 101, 123 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → ((〈𝐹, 𝑋〉(2nd
‘((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂)))〈𝐺, 𝑃〉)‘〈𝐴, 𝐾〉) = 〈((𝑃(2nd ‘𝑌)𝑋)‘𝐾), 𝐴〉) |
| 125 | 100, 124 | fveq12d 6913 |
. . 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 ‘𝑌)𝑋)‘𝐾), 𝐴〉)) |
| 126 | | df-ov 7434 |
. . 3
⊢ (((𝑃(2nd ‘𝑌)𝑋)‘𝐾)(〈((1st ‘𝑌)‘𝑋), 𝐹〉(2nd ‘𝐻)〈((1st
‘𝑌)‘𝑃), 𝐺〉)𝐴) = ((〈((1st ‘𝑌)‘𝑋), 𝐹〉(2nd ‘𝐻)〈((1st
‘𝑌)‘𝑃), 𝐺〉)‘〈((𝑃(2nd ‘𝑌)𝑋)‘𝐾), 𝐴〉) |
| 127 | 125, 126 | eqtr4di 2795 |
. 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
‘𝑌)‘𝑃), 𝐺〉)𝐴)) |
| 128 | 66, 127 | eqtrd 2777 |
1
⊢ (𝜑 → (𝐴(〈𝐹, 𝑋〉(2nd ‘𝑍)〈𝐺, 𝑃〉)𝐾) = (((𝑃(2nd ‘𝑌)𝑋)‘𝐾)(〈((1st ‘𝑌)‘𝑋), 𝐹〉(2nd ‘𝐻)〈((1st
‘𝑌)‘𝑃), 𝐺〉)𝐴)) |