MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  yonedalem22 Structured version   Visualization version   GIF version

Theorem yonedalem22 18166
Description: Lemma for yoneda 18171. (Contributed by Mario Carneiro, 29-Jan-2017.)
Hypotheses
Ref Expression
yoneda.y 𝑌 = (Yon‘𝐶)
yoneda.b 𝐵 = (Base‘𝐶)
yoneda.1 1 = (Id‘𝐶)
yoneda.o 𝑂 = (oppCat‘𝐶)
yoneda.s 𝑆 = (SetCat‘𝑈)
yoneda.t 𝑇 = (SetCat‘𝑉)
yoneda.q 𝑄 = (𝑂 FuncCat 𝑆)
yoneda.h 𝐻 = (HomF𝑄)
yoneda.r 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)
yoneda.e 𝐸 = (𝑂 evalF 𝑆)
yoneda.z 𝑍 = (𝐻func ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))
yoneda.c (𝜑𝐶 ∈ Cat)
yoneda.w (𝜑𝑉𝑊)
yoneda.u (𝜑 → ran (Homf𝐶) ⊆ 𝑈)
yoneda.v (𝜑 → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
yonedalem21.f (𝜑𝐹 ∈ (𝑂 Func 𝑆))
yonedalem21.x (𝜑𝑋𝐵)
yonedalem22.g (𝜑𝐺 ∈ (𝑂 Func 𝑆))
yonedalem22.p (𝜑𝑃𝐵)
yonedalem22.a (𝜑𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
yonedalem22.k (𝜑𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
Assertion
Ref Expression
yonedalem22 (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾) = (((𝑃(2nd𝑌)𝑋)‘𝐾)(⟨((1st𝑌)‘𝑋), 𝐹⟩(2nd𝐻)⟨((1st𝑌)‘𝑃), 𝐺⟩)𝐴))

Proof of Theorem yonedalem22
StepHypRef Expression
1 yoneda.z . . . . . . 7 𝑍 = (𝐻func ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))
21fveq2i 6845 . . . . . 6 (2nd𝑍) = (2nd ‘(𝐻func ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))))
32oveqi 7369 . . . . 5 (⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩) = (⟨𝐹, 𝑋⟩(2nd ‘(𝐻func ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))))⟨𝐺, 𝑃⟩)
43oveqi 7369 . . . 4 (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾) = (𝐴(⟨𝐹, 𝑋⟩(2nd ‘(𝐻func ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))))⟨𝐺, 𝑃⟩)𝐾)
5 df-ov 7359 . . . 4 (𝐴(⟨𝐹, 𝑋⟩(2nd ‘(𝐻func ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))))⟨𝐺, 𝑃⟩)𝐾) = ((⟨𝐹, 𝑋⟩(2nd ‘(𝐻func ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩)
64, 5eqtri 2764 . . 3 (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾) = ((⟨𝐹, 𝑋⟩(2nd ‘(𝐻func ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩)
7 eqid 2736 . . . . 5 (𝑄 ×c 𝑂) = (𝑄 ×c 𝑂)
8 yoneda.q . . . . . 6 𝑄 = (𝑂 FuncCat 𝑆)
98fucbas 17847 . . . . 5 (𝑂 Func 𝑆) = (Base‘𝑄)
10 yoneda.o . . . . . 6 𝑂 = (oppCat‘𝐶)
11 yoneda.b . . . . . 6 𝐵 = (Base‘𝐶)
1210, 11oppcbas 17598 . . . . 5 𝐵 = (Base‘𝑂)
137, 9, 12xpcbas 18065 . . . 4 ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂))
14 eqid 2736 . . . . 5 ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)) = ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂))
15 eqid 2736 . . . . 5 ((oppCat‘𝑄) ×c 𝑄) = ((oppCat‘𝑄) ×c 𝑄)
16 yoneda.c . . . . . . . . 9 (𝜑𝐶 ∈ Cat)
1710oppccat 17603 . . . . . . . . 9 (𝐶 ∈ Cat → 𝑂 ∈ Cat)
1816, 17syl 17 . . . . . . . 8 (𝜑𝑂 ∈ Cat)
19 yoneda.w . . . . . . . . . 10 (𝜑𝑉𝑊)
20 yoneda.v . . . . . . . . . . 11 (𝜑 → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
2120unssbd 4148 . . . . . . . . . 10 (𝜑𝑈𝑉)
2219, 21ssexd 5281 . . . . . . . . 9 (𝜑𝑈 ∈ V)
23 yoneda.s . . . . . . . . . 10 𝑆 = (SetCat‘𝑈)
2423setccat 17970 . . . . . . . . 9 (𝑈 ∈ V → 𝑆 ∈ Cat)
2522, 24syl 17 . . . . . . . 8 (𝜑𝑆 ∈ Cat)
268, 18, 25fuccat 17858 . . . . . . 7 (𝜑𝑄 ∈ Cat)
27 eqid 2736 . . . . . . 7 (𝑄 2ndF 𝑂) = (𝑄 2ndF 𝑂)
287, 26, 18, 272ndfcl 18085 . . . . . 6 (𝜑 → (𝑄 2ndF 𝑂) ∈ ((𝑄 ×c 𝑂) Func 𝑂))
29 eqid 2736 . . . . . . . 8 (oppCat‘𝑄) = (oppCat‘𝑄)
30 relfunc 17747 . . . . . . . . 9 Rel (𝐶 Func 𝑄)
31 yoneda.y . . . . . . . . . 10 𝑌 = (Yon‘𝐶)
32 yoneda.u . . . . . . . . . 10 (𝜑 → ran (Homf𝐶) ⊆ 𝑈)
3331, 16, 10, 23, 8, 22, 32yoncl 18150 . . . . . . . . 9 (𝜑𝑌 ∈ (𝐶 Func 𝑄))
34 1st2ndbr 7973 . . . . . . . . 9 ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
3530, 33, 34sylancr 587 . . . . . . . 8 (𝜑 → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
3610, 29, 35funcoppc 17760 . . . . . . 7 (𝜑 → (1st𝑌)(𝑂 Func (oppCat‘𝑄))tpos (2nd𝑌))
37 df-br 5106 . . . . . . 7 ((1st𝑌)(𝑂 Func (oppCat‘𝑄))tpos (2nd𝑌) ↔ ⟨(1st𝑌), tpos (2nd𝑌)⟩ ∈ (𝑂 Func (oppCat‘𝑄)))
3836, 37sylib 217 . . . . . 6 (𝜑 → ⟨(1st𝑌), tpos (2nd𝑌)⟩ ∈ (𝑂 Func (oppCat‘𝑄)))
3928, 38cofucl 17773 . . . . 5 (𝜑 → (⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ∈ ((𝑄 ×c 𝑂) Func (oppCat‘𝑄)))
40 eqid 2736 . . . . . 6 (𝑄 1stF 𝑂) = (𝑄 1stF 𝑂)
417, 26, 18, 401stfcl 18084 . . . . 5 (𝜑 → (𝑄 1stF 𝑂) ∈ ((𝑄 ×c 𝑂) Func 𝑄))
4214, 15, 39, 41prfcl 18090 . . . 4 (𝜑 → ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)) ∈ ((𝑄 ×c 𝑂) Func ((oppCat‘𝑄) ×c 𝑄)))
43 yoneda.h . . . . 5 𝐻 = (HomF𝑄)
44 yoneda.t . . . . 5 𝑇 = (SetCat‘𝑉)
4520unssad 4147 . . . . 5 (𝜑 → ran (Homf𝑄) ⊆ 𝑉)
4643, 29, 44, 26, 19, 45hofcl 18147 . . . 4 (𝜑𝐻 ∈ (((oppCat‘𝑄) ×c 𝑄) Func 𝑇))
47 yonedalem21.f . . . . 5 (𝜑𝐹 ∈ (𝑂 Func 𝑆))
48 yonedalem21.x . . . . 5 (𝜑𝑋𝐵)
4947, 48opelxpd 5671 . . . 4 (𝜑 → ⟨𝐹, 𝑋⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
50 yonedalem22.g . . . . 5 (𝜑𝐺 ∈ (𝑂 Func 𝑆))
51 yonedalem22.p . . . . 5 (𝜑𝑃𝐵)
5250, 51opelxpd 5671 . . . 4 (𝜑 → ⟨𝐺, 𝑃⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
53 eqid 2736 . . . 4 (Hom ‘(𝑄 ×c 𝑂)) = (Hom ‘(𝑄 ×c 𝑂))
54 yonedalem22.a . . . . . 6 (𝜑𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
55 yonedalem22.k . . . . . . 7 (𝜑𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
56 eqid 2736 . . . . . . . 8 (Hom ‘𝐶) = (Hom ‘𝐶)
5756, 10oppchom 17595 . . . . . . 7 (𝑋(Hom ‘𝑂)𝑃) = (𝑃(Hom ‘𝐶)𝑋)
5855, 57eleqtrrdi 2849 . . . . . 6 (𝜑𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃))
5954, 58opelxpd 5671 . . . . 5 (𝜑 → ⟨𝐴, 𝐾⟩ ∈ ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃)))
60 eqid 2736 . . . . . . 7 (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
618, 60fuchom 17848 . . . . . 6 (𝑂 Nat 𝑆) = (Hom ‘𝑄)
62 eqid 2736 . . . . . 6 (Hom ‘𝑂) = (Hom ‘𝑂)
637, 9, 12, 61, 62, 47, 48, 50, 51, 53xpchom2 18073 . . . . 5 (𝜑 → (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃)))
6459, 63eleqtrrd 2841 . . . 4 (𝜑 → ⟨𝐴, 𝐾⟩ ∈ (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩))
6513, 42, 46, 49, 52, 53, 64cofu2 17771 . . 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 𝑂)))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩)))
666, 65eqtrid 2788 . 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 𝑂)))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩)))
6714, 13, 53, 39, 41, 49prf1 18087 . . . . . 6 (𝜑 → ((1st ‘((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))‘⟨𝐹, 𝑋⟩) = ⟨((1st ‘(⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)))‘⟨𝐹, 𝑋⟩), ((1st ‘(𝑄 1stF 𝑂))‘⟨𝐹, 𝑋⟩)⟩)
6813, 28, 38, 49cofu1 17769 . . . . . . . 8 (𝜑 → ((1st ‘(⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)))‘⟨𝐹, 𝑋⟩) = ((1st ‘⟨(1st𝑌), tpos (2nd𝑌)⟩)‘((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐹, 𝑋⟩)))
69 fvex 6855 . . . . . . . . . . 11 (1st𝑌) ∈ V
70 fvex 6855 . . . . . . . . . . . 12 (2nd𝑌) ∈ V
7170tposex 8190 . . . . . . . . . . 11 tpos (2nd𝑌) ∈ V
7269, 71op1st 7928 . . . . . . . . . 10 (1st ‘⟨(1st𝑌), tpos (2nd𝑌)⟩) = (1st𝑌)
7372a1i 11 . . . . . . . . 9 (𝜑 → (1st ‘⟨(1st𝑌), tpos (2nd𝑌)⟩) = (1st𝑌))
747, 13, 53, 26, 18, 27, 492ndf1 18082 . . . . . . . . . 10 (𝜑 → ((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐹, 𝑋⟩) = (2nd ‘⟨𝐹, 𝑋⟩))
75 op2ndg 7933 . . . . . . . . . . 11 ((𝐹 ∈ (𝑂 Func 𝑆) ∧ 𝑋𝐵) → (2nd ‘⟨𝐹, 𝑋⟩) = 𝑋)
7647, 48, 75syl2anc 584 . . . . . . . . . 10 (𝜑 → (2nd ‘⟨𝐹, 𝑋⟩) = 𝑋)
7774, 76eqtrd 2776 . . . . . . . . 9 (𝜑 → ((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐹, 𝑋⟩) = 𝑋)
7873, 77fveq12d 6849 . . . . . . . 8 (𝜑 → ((1st ‘⟨(1st𝑌), tpos (2nd𝑌)⟩)‘((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐹, 𝑋⟩)) = ((1st𝑌)‘𝑋))
7968, 78eqtrd 2776 . . . . . . 7 (𝜑 → ((1st ‘(⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)))‘⟨𝐹, 𝑋⟩) = ((1st𝑌)‘𝑋))
807, 13, 53, 26, 18, 40, 491stf1 18079 . . . . . . . 8 (𝜑 → ((1st ‘(𝑄 1stF 𝑂))‘⟨𝐹, 𝑋⟩) = (1st ‘⟨𝐹, 𝑋⟩))
81 op1stg 7932 . . . . . . . . 9 ((𝐹 ∈ (𝑂 Func 𝑆) ∧ 𝑋𝐵) → (1st ‘⟨𝐹, 𝑋⟩) = 𝐹)
8247, 48, 81syl2anc 584 . . . . . . . 8 (𝜑 → (1st ‘⟨𝐹, 𝑋⟩) = 𝐹)
8380, 82eqtrd 2776 . . . . . . 7 (𝜑 → ((1st ‘(𝑄 1stF 𝑂))‘⟨𝐹, 𝑋⟩) = 𝐹)
8479, 83opeq12d 4838 . . . . . 6 (𝜑 → ⟨((1st ‘(⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)))‘⟨𝐹, 𝑋⟩), ((1st ‘(𝑄 1stF 𝑂))‘⟨𝐹, 𝑋⟩)⟩ = ⟨((1st𝑌)‘𝑋), 𝐹⟩)
8567, 84eqtrd 2776 . . . . 5 (𝜑 → ((1st ‘((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))‘⟨𝐹, 𝑋⟩) = ⟨((1st𝑌)‘𝑋), 𝐹⟩)
8614, 13, 53, 39, 41, 52prf1 18087 . . . . . 6 (𝜑 → ((1st ‘((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))‘⟨𝐺, 𝑃⟩) = ⟨((1st ‘(⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)))‘⟨𝐺, 𝑃⟩), ((1st ‘(𝑄 1stF 𝑂))‘⟨𝐺, 𝑃⟩)⟩)
8713, 28, 38, 52cofu1 17769 . . . . . . . 8 (𝜑 → ((1st ‘(⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)))‘⟨𝐺, 𝑃⟩) = ((1st ‘⟨(1st𝑌), tpos (2nd𝑌)⟩)‘((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐺, 𝑃⟩)))
887, 13, 53, 26, 18, 27, 522ndf1 18082 . . . . . . . . . 10 (𝜑 → ((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐺, 𝑃⟩) = (2nd ‘⟨𝐺, 𝑃⟩))
89 op2ndg 7933 . . . . . . . . . . 11 ((𝐺 ∈ (𝑂 Func 𝑆) ∧ 𝑃𝐵) → (2nd ‘⟨𝐺, 𝑃⟩) = 𝑃)
9050, 51, 89syl2anc 584 . . . . . . . . . 10 (𝜑 → (2nd ‘⟨𝐺, 𝑃⟩) = 𝑃)
9188, 90eqtrd 2776 . . . . . . . . 9 (𝜑 → ((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐺, 𝑃⟩) = 𝑃)
9273, 91fveq12d 6849 . . . . . . . 8 (𝜑 → ((1st ‘⟨(1st𝑌), tpos (2nd𝑌)⟩)‘((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐺, 𝑃⟩)) = ((1st𝑌)‘𝑃))
9387, 92eqtrd 2776 . . . . . . 7 (𝜑 → ((1st ‘(⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)))‘⟨𝐺, 𝑃⟩) = ((1st𝑌)‘𝑃))
947, 13, 53, 26, 18, 40, 521stf1 18079 . . . . . . . 8 (𝜑 → ((1st ‘(𝑄 1stF 𝑂))‘⟨𝐺, 𝑃⟩) = (1st ‘⟨𝐺, 𝑃⟩))
95 op1stg 7932 . . . . . . . . 9 ((𝐺 ∈ (𝑂 Func 𝑆) ∧ 𝑃𝐵) → (1st ‘⟨𝐺, 𝑃⟩) = 𝐺)
9650, 51, 95syl2anc 584 . . . . . . . 8 (𝜑 → (1st ‘⟨𝐺, 𝑃⟩) = 𝐺)
9794, 96eqtrd 2776 . . . . . . 7 (𝜑 → ((1st ‘(𝑄 1stF 𝑂))‘⟨𝐺, 𝑃⟩) = 𝐺)
9893, 97opeq12d 4838 . . . . . 6 (𝜑 → ⟨((1st ‘(⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)))‘⟨𝐺, 𝑃⟩), ((1st ‘(𝑄 1stF 𝑂))‘⟨𝐺, 𝑃⟩)⟩ = ⟨((1st𝑌)‘𝑃), 𝐺⟩)
9986, 98eqtrd 2776 . . . . 5 (𝜑 → ((1st ‘((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))‘⟨𝐺, 𝑃⟩) = ⟨((1st𝑌)‘𝑃), 𝐺⟩)
10085, 99oveq12d 7374 . . . 4 (𝜑 → (((1st ‘((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))‘⟨𝐹, 𝑋⟩)(2nd𝐻)((1st ‘((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))‘⟨𝐺, 𝑃⟩)) = (⟨((1st𝑌)‘𝑋), 𝐹⟩(2nd𝐻)⟨((1st𝑌)‘𝑃), 𝐺⟩))
10114, 13, 53, 39, 41, 49, 52, 64prf2 18089 . . . . 5 (𝜑 → ((⟨𝐹, 𝑋⟩(2nd ‘((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩) = ⟨((⟨𝐹, 𝑋⟩(2nd ‘(⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩), ((⟨𝐹, 𝑋⟩(2nd ‘(𝑄 1stF 𝑂))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩)⟩)
10213, 28, 38, 49, 52, 53, 64cofu2 17771 . . . . . . 7 (𝜑 → ((⟨𝐹, 𝑋⟩(2nd ‘(⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩) = ((((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐹, 𝑋⟩)(2nd ‘⟨(1st𝑌), tpos (2nd𝑌)⟩)((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐺, 𝑃⟩))‘((⟨𝐹, 𝑋⟩(2nd ‘(𝑄 2ndF 𝑂))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩)))
10369, 71op2nd 7929 . . . . . . . . . . 11 (2nd ‘⟨(1st𝑌), tpos (2nd𝑌)⟩) = tpos (2nd𝑌)
104103oveqi 7369 . . . . . . . . . 10 (((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐹, 𝑋⟩)(2nd ‘⟨(1st𝑌), tpos (2nd𝑌)⟩)((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐺, 𝑃⟩)) = (((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐹, 𝑋⟩)tpos (2nd𝑌)((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐺, 𝑃⟩))
105 ovtpos 8171 . . . . . . . . . 10 (((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐹, 𝑋⟩)tpos (2nd𝑌)((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐺, 𝑃⟩)) = (((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐺, 𝑃⟩)(2nd𝑌)((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐹, 𝑋⟩))
106104, 105eqtri 2764 . . . . . . . . 9 (((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐹, 𝑋⟩)(2nd ‘⟨(1st𝑌), tpos (2nd𝑌)⟩)((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐺, 𝑃⟩)) = (((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐺, 𝑃⟩)(2nd𝑌)((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐹, 𝑋⟩))
10791, 77oveq12d 7374 . . . . . . . . 9 (𝜑 → (((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐺, 𝑃⟩)(2nd𝑌)((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐹, 𝑋⟩)) = (𝑃(2nd𝑌)𝑋))
108106, 107eqtrid 2788 . . . . . . . 8 (𝜑 → (((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐹, 𝑋⟩)(2nd ‘⟨(1st𝑌), tpos (2nd𝑌)⟩)((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐺, 𝑃⟩)) = (𝑃(2nd𝑌)𝑋))
1097, 13, 53, 26, 18, 27, 49, 522ndf2 18083 . . . . . . . . . 10 (𝜑 → (⟨𝐹, 𝑋⟩(2nd ‘(𝑄 2ndF 𝑂))⟨𝐺, 𝑃⟩) = (2nd ↾ (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩)))
110109fveq1d 6844 . . . . . . . . 9 (𝜑 → ((⟨𝐹, 𝑋⟩(2nd ‘(𝑄 2ndF 𝑂))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩) = ((2nd ↾ (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩))‘⟨𝐴, 𝐾⟩))
11164fvresd 6862 . . . . . . . . 9 (𝜑 → ((2nd ↾ (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩))‘⟨𝐴, 𝐾⟩) = (2nd ‘⟨𝐴, 𝐾⟩))
112 op2ndg 7933 . . . . . . . . . 10 ((𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺) ∧ 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋)) → (2nd ‘⟨𝐴, 𝐾⟩) = 𝐾)
11354, 55, 112syl2anc 584 . . . . . . . . 9 (𝜑 → (2nd ‘⟨𝐴, 𝐾⟩) = 𝐾)
114110, 111, 1133eqtrd 2780 . . . . . . . 8 (𝜑 → ((⟨𝐹, 𝑋⟩(2nd ‘(𝑄 2ndF 𝑂))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩) = 𝐾)
115108, 114fveq12d 6849 . . . . . . 7 (𝜑 → ((((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐹, 𝑋⟩)(2nd ‘⟨(1st𝑌), tpos (2nd𝑌)⟩)((1st ‘(𝑄 2ndF 𝑂))‘⟨𝐺, 𝑃⟩))‘((⟨𝐹, 𝑋⟩(2nd ‘(𝑄 2ndF 𝑂))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩)) = ((𝑃(2nd𝑌)𝑋)‘𝐾))
116102, 115eqtrd 2776 . . . . . 6 (𝜑 → ((⟨𝐹, 𝑋⟩(2nd ‘(⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩) = ((𝑃(2nd𝑌)𝑋)‘𝐾))
1177, 13, 53, 26, 18, 40, 49, 521stf2 18080 . . . . . . . 8 (𝜑 → (⟨𝐹, 𝑋⟩(2nd ‘(𝑄 1stF 𝑂))⟨𝐺, 𝑃⟩) = (1st ↾ (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩)))
118117fveq1d 6844 . . . . . . 7 (𝜑 → ((⟨𝐹, 𝑋⟩(2nd ‘(𝑄 1stF 𝑂))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩) = ((1st ↾ (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩))‘⟨𝐴, 𝐾⟩))
11964fvresd 6862 . . . . . . 7 (𝜑 → ((1st ↾ (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩))‘⟨𝐴, 𝐾⟩) = (1st ‘⟨𝐴, 𝐾⟩))
120 op1stg 7932 . . . . . . . 8 ((𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺) ∧ 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋)) → (1st ‘⟨𝐴, 𝐾⟩) = 𝐴)
12154, 55, 120syl2anc 584 . . . . . . 7 (𝜑 → (1st ‘⟨𝐴, 𝐾⟩) = 𝐴)
122118, 119, 1213eqtrd 2780 . . . . . 6 (𝜑 → ((⟨𝐹, 𝑋⟩(2nd ‘(𝑄 1stF 𝑂))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩) = 𝐴)
123116, 122opeq12d 4838 . . . . 5 (𝜑 → ⟨((⟨𝐹, 𝑋⟩(2nd ‘(⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩), ((⟨𝐹, 𝑋⟩(2nd ‘(𝑄 1stF 𝑂))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩)⟩ = ⟨((𝑃(2nd𝑌)𝑋)‘𝐾), 𝐴⟩)
124101, 123eqtrd 2776 . . . 4 (𝜑 → ((⟨𝐹, 𝑋⟩(2nd ‘((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))⟨𝐺, 𝑃⟩)‘⟨𝐴, 𝐾⟩) = ⟨((𝑃(2nd𝑌)𝑋)‘𝐾), 𝐴⟩)
125100, 124fveq12d 6849 . . 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 7359 . . 3 (((𝑃(2nd𝑌)𝑋)‘𝐾)(⟨((1st𝑌)‘𝑋), 𝐹⟩(2nd𝐻)⟨((1st𝑌)‘𝑃), 𝐺⟩)𝐴) = ((⟨((1st𝑌)‘𝑋), 𝐹⟩(2nd𝐻)⟨((1st𝑌)‘𝑃), 𝐺⟩)‘⟨((𝑃(2nd𝑌)𝑋)‘𝐾), 𝐴⟩)
127125, 126eqtr4di 2794 . 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𝑌)‘𝑃), 𝐺⟩)𝐴))
12866, 127eqtrd 2776 1 (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾) = (((𝑃(2nd𝑌)𝑋)‘𝐾)(⟨((1st𝑌)‘𝑋), 𝐹⟩(2nd𝐻)⟨((1st𝑌)‘𝑃), 𝐺⟩)𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wcel 2106  Vcvv 3445  cun 3908  wss 3910  cop 4592   class class class wbr 5105   × cxp 5631  ran crn 5634  cres 5635  Rel wrel 5638  cfv 6496  (class class class)co 7356  1st c1st 7918  2nd c2nd 7919  tpos ctpos 8155  Basecbs 17082  Hom chom 17143  Catccat 17543  Idccid 17544  Homf chomf 17545  oppCatcoppc 17590   Func cfunc 17739  func ccofu 17741   Nat cnat 17827   FuncCat cfuc 17828  SetCatcsetc 17960   ×c cxpc 18055   1stF c1stf 18056   2ndF c2ndf 18057   ⟨,⟩F cprf 18058   evalF cevlf 18097  HomFchof 18136  Yoncyon 18137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7671  ax-cnex 11106  ax-resscn 11107  ax-1cn 11108  ax-icn 11109  ax-addcl 11110  ax-addrcl 11111  ax-mulcl 11112  ax-mulrcl 11113  ax-mulcom 11114  ax-addass 11115  ax-mulass 11116  ax-distr 11117  ax-i2m1 11118  ax-1ne0 11119  ax-1rid 11120  ax-rnegex 11121  ax-rrecex 11122  ax-cnre 11123  ax-pre-lttri 11124  ax-pre-lttrn 11125  ax-pre-ltadd 11126  ax-pre-mulgt0 11127
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7312  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7802  df-1st 7920  df-2nd 7921  df-tpos 8156  df-frecs 8211  df-wrecs 8242  df-recs 8316  df-rdg 8355  df-1o 8411  df-er 8647  df-map 8766  df-ixp 8835  df-en 8883  df-dom 8884  df-sdom 8885  df-fin 8886  df-pnf 11190  df-mnf 11191  df-xr 11192  df-ltxr 11193  df-le 11194  df-sub 11386  df-neg 11387  df-nn 12153  df-2 12215  df-3 12216  df-4 12217  df-5 12218  df-6 12219  df-7 12220  df-8 12221  df-9 12222  df-n0 12413  df-z 12499  df-dec 12618  df-uz 12763  df-fz 13424  df-struct 17018  df-sets 17035  df-slot 17053  df-ndx 17065  df-base 17083  df-hom 17156  df-cco 17157  df-cat 17547  df-cid 17548  df-homf 17549  df-comf 17550  df-oppc 17591  df-func 17743  df-cofu 17745  df-nat 17829  df-fuc 17830  df-setc 17961  df-xpc 18059  df-1stf 18060  df-2ndf 18061  df-prf 18062  df-curf 18102  df-hof 18138  df-yon 18139
This theorem is referenced by:  yonedalem3b  18167
  Copyright terms: Public domain W3C validator