| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | yoneda.m | . . . . 5
⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥)))) | 
| 2 |  | ovex 7465 | . . . . . 6
⊢
(((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ∈ V | 
| 3 | 2 | mptex 7244 | . . . . 5
⊢ (𝑎 ∈ (((1st
‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))) ∈ V | 
| 4 | 1, 3 | fnmpoi 8096 | . . . 4
⊢ 𝑀 Fn ((𝑂 Func 𝑆) × 𝐵) | 
| 5 | 4 | a1i 11 | . . 3
⊢ (𝜑 → 𝑀 Fn ((𝑂 Func 𝑆) × 𝐵)) | 
| 6 |  | yoneda.y | . . . . . . . 8
⊢ 𝑌 = (Yon‘𝐶) | 
| 7 |  | yoneda.b | . . . . . . . 8
⊢ 𝐵 = (Base‘𝐶) | 
| 8 |  | yoneda.1 | . . . . . . . 8
⊢  1 =
(Id‘𝐶) | 
| 9 |  | yoneda.o | . . . . . . . 8
⊢ 𝑂 = (oppCat‘𝐶) | 
| 10 |  | yoneda.s | . . . . . . . 8
⊢ 𝑆 = (SetCat‘𝑈) | 
| 11 |  | yoneda.t | . . . . . . . 8
⊢ 𝑇 = (SetCat‘𝑉) | 
| 12 |  | yoneda.q | . . . . . . . 8
⊢ 𝑄 = (𝑂 FuncCat 𝑆) | 
| 13 |  | yoneda.h | . . . . . . . 8
⊢ 𝐻 =
(HomF‘𝑄) | 
| 14 |  | yoneda.r | . . . . . . . 8
⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇) | 
| 15 |  | yoneda.e | . . . . . . . 8
⊢ 𝐸 = (𝑂 evalF 𝑆) | 
| 16 |  | yoneda.z | . . . . . . . 8
⊢ 𝑍 = (𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂))) | 
| 17 |  | yoneda.c | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ Cat) | 
| 18 | 17 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ Cat) | 
| 19 |  | yoneda.w | . . . . . . . . 9
⊢ (𝜑 → 𝑉 ∈ 𝑊) | 
| 20 | 19 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → 𝑉 ∈ 𝑊) | 
| 21 |  | yoneda.u | . . . . . . . . 9
⊢ (𝜑 → ran
(Homf ‘𝐶) ⊆ 𝑈) | 
| 22 | 21 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → ran (Homf
‘𝐶) ⊆ 𝑈) | 
| 23 |  | yoneda.v | . . . . . . . . 9
⊢ (𝜑 → (ran
(Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) | 
| 24 | 23 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → (ran (Homf
‘𝑄) ∪ 𝑈) ⊆ 𝑉) | 
| 25 |  | simprl 770 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → 𝑔 ∈ (𝑂 Func 𝑆)) | 
| 26 |  | simprr 772 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) | 
| 27 | 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 18, 20, 22, 24, 25, 26, 1 | yonedalem3a 18320 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → ((𝑔𝑀𝑦) = (𝑎 ∈ (((1st ‘𝑌)‘𝑦)(𝑂 Nat 𝑆)𝑔) ↦ ((𝑎‘𝑦)‘( 1 ‘𝑦))) ∧ (𝑔𝑀𝑦):(𝑔(1st ‘𝑍)𝑦)⟶(𝑔(1st ‘𝐸)𝑦))) | 
| 28 | 27 | simprd 495 | . . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → (𝑔𝑀𝑦):(𝑔(1st ‘𝑍)𝑦)⟶(𝑔(1st ‘𝐸)𝑦)) | 
| 29 |  | eqid 2736 | . . . . . . 7
⊢ (Hom
‘𝑇) = (Hom
‘𝑇) | 
| 30 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (𝑄 ×c
𝑂) = (𝑄 ×c 𝑂) | 
| 31 | 12 | fucbas 18009 | . . . . . . . . . . 11
⊢ (𝑂 Func 𝑆) = (Base‘𝑄) | 
| 32 | 9, 7 | oppcbas 17762 | . . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝑂) | 
| 33 | 30, 31, 32 | xpcbas 18224 | . . . . . . . . . 10
⊢ ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂)) | 
| 34 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Base‘𝑇) =
(Base‘𝑇) | 
| 35 |  | relfunc 17908 | . . . . . . . . . . 11
⊢ Rel
((𝑄
×c 𝑂) Func 𝑇) | 
| 36 | 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 19, 21, 23 | yonedalem1 18318 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))) | 
| 37 | 36 | simpld 494 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) | 
| 38 |  | 1st2ndbr 8068 | . . . . . . . . . . 11
⊢ ((Rel
((𝑄
×c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st ‘𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝑍)) | 
| 39 | 35, 37, 38 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (1st
‘𝑍)((𝑄 ×c
𝑂) Func 𝑇)(2nd ‘𝑍)) | 
| 40 | 33, 34, 39 | funcf1 17912 | . . . . . . . . 9
⊢ (𝜑 → (1st
‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)) | 
| 41 | 40 | fovcdmda 7605 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → (𝑔(1st ‘𝑍)𝑦) ∈ (Base‘𝑇)) | 
| 42 | 11, 20 | setcbas 18124 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → 𝑉 = (Base‘𝑇)) | 
| 43 | 41, 42 | eleqtrrd 2843 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → (𝑔(1st ‘𝑍)𝑦) ∈ 𝑉) | 
| 44 | 36 | simprd 495 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) | 
| 45 |  | 1st2ndbr 8068 | . . . . . . . . . . 11
⊢ ((Rel
((𝑄
×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st ‘𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝐸)) | 
| 46 | 35, 44, 45 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (1st
‘𝐸)((𝑄 ×c
𝑂) Func 𝑇)(2nd ‘𝐸)) | 
| 47 | 33, 34, 46 | funcf1 17912 | . . . . . . . . 9
⊢ (𝜑 → (1st
‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)) | 
| 48 | 47 | fovcdmda 7605 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → (𝑔(1st ‘𝐸)𝑦) ∈ (Base‘𝑇)) | 
| 49 | 48, 42 | eleqtrrd 2843 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → (𝑔(1st ‘𝐸)𝑦) ∈ 𝑉) | 
| 50 | 11, 20, 29, 43, 49 | elsetchom 18127 | . . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → ((𝑔𝑀𝑦) ∈ ((𝑔(1st ‘𝑍)𝑦)(Hom ‘𝑇)(𝑔(1st ‘𝐸)𝑦)) ↔ (𝑔𝑀𝑦):(𝑔(1st ‘𝑍)𝑦)⟶(𝑔(1st ‘𝐸)𝑦))) | 
| 51 | 28, 50 | mpbird 257 | . . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → (𝑔𝑀𝑦) ∈ ((𝑔(1st ‘𝑍)𝑦)(Hom ‘𝑇)(𝑔(1st ‘𝐸)𝑦))) | 
| 52 | 51 | ralrimivva 3201 | . . . 4
⊢ (𝜑 → ∀𝑔 ∈ (𝑂 Func 𝑆)∀𝑦 ∈ 𝐵 (𝑔𝑀𝑦) ∈ ((𝑔(1st ‘𝑍)𝑦)(Hom ‘𝑇)(𝑔(1st ‘𝐸)𝑦))) | 
| 53 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑧 = 〈𝑔, 𝑦〉 → (𝑀‘𝑧) = (𝑀‘〈𝑔, 𝑦〉)) | 
| 54 |  | df-ov 7435 | . . . . . . 7
⊢ (𝑔𝑀𝑦) = (𝑀‘〈𝑔, 𝑦〉) | 
| 55 | 53, 54 | eqtr4di 2794 | . . . . . 6
⊢ (𝑧 = 〈𝑔, 𝑦〉 → (𝑀‘𝑧) = (𝑔𝑀𝑦)) | 
| 56 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑧 = 〈𝑔, 𝑦〉 → ((1st ‘𝑍)‘𝑧) = ((1st ‘𝑍)‘〈𝑔, 𝑦〉)) | 
| 57 |  | df-ov 7435 | . . . . . . . 8
⊢ (𝑔(1st ‘𝑍)𝑦) = ((1st ‘𝑍)‘〈𝑔, 𝑦〉) | 
| 58 | 56, 57 | eqtr4di 2794 | . . . . . . 7
⊢ (𝑧 = 〈𝑔, 𝑦〉 → ((1st ‘𝑍)‘𝑧) = (𝑔(1st ‘𝑍)𝑦)) | 
| 59 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑧 = 〈𝑔, 𝑦〉 → ((1st ‘𝐸)‘𝑧) = ((1st ‘𝐸)‘〈𝑔, 𝑦〉)) | 
| 60 |  | df-ov 7435 | . . . . . . . 8
⊢ (𝑔(1st ‘𝐸)𝑦) = ((1st ‘𝐸)‘〈𝑔, 𝑦〉) | 
| 61 | 59, 60 | eqtr4di 2794 | . . . . . . 7
⊢ (𝑧 = 〈𝑔, 𝑦〉 → ((1st ‘𝐸)‘𝑧) = (𝑔(1st ‘𝐸)𝑦)) | 
| 62 | 58, 61 | oveq12d 7450 | . . . . . 6
⊢ (𝑧 = 〈𝑔, 𝑦〉 → (((1st ‘𝑍)‘𝑧)(Hom ‘𝑇)((1st ‘𝐸)‘𝑧)) = ((𝑔(1st ‘𝑍)𝑦)(Hom ‘𝑇)(𝑔(1st ‘𝐸)𝑦))) | 
| 63 | 55, 62 | eleq12d 2834 | . . . . 5
⊢ (𝑧 = 〈𝑔, 𝑦〉 → ((𝑀‘𝑧) ∈ (((1st ‘𝑍)‘𝑧)(Hom ‘𝑇)((1st ‘𝐸)‘𝑧)) ↔ (𝑔𝑀𝑦) ∈ ((𝑔(1st ‘𝑍)𝑦)(Hom ‘𝑇)(𝑔(1st ‘𝐸)𝑦)))) | 
| 64 | 63 | ralxp 5851 | . . . 4
⊢
(∀𝑧 ∈
((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧) ∈ (((1st ‘𝑍)‘𝑧)(Hom ‘𝑇)((1st ‘𝐸)‘𝑧)) ↔ ∀𝑔 ∈ (𝑂 Func 𝑆)∀𝑦 ∈ 𝐵 (𝑔𝑀𝑦) ∈ ((𝑔(1st ‘𝑍)𝑦)(Hom ‘𝑇)(𝑔(1st ‘𝐸)𝑦))) | 
| 65 | 52, 64 | sylibr 234 | . . 3
⊢ (𝜑 → ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧) ∈ (((1st ‘𝑍)‘𝑧)(Hom ‘𝑇)((1st ‘𝐸)‘𝑧))) | 
| 66 |  | ovex 7465 | . . . . . 6
⊢ (𝑂 Func 𝑆) ∈ V | 
| 67 | 7 | fvexi 6919 | . . . . . 6
⊢ 𝐵 ∈ V | 
| 68 | 66, 67 | mpoex 8105 | . . . . 5
⊢ (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥)))) ∈ V | 
| 69 | 1, 68 | eqeltri 2836 | . . . 4
⊢ 𝑀 ∈ V | 
| 70 | 69 | elixp 8945 | . . 3
⊢ (𝑀 ∈ X𝑧 ∈
((𝑂 Func 𝑆) × 𝐵)(((1st ‘𝑍)‘𝑧)(Hom ‘𝑇)((1st ‘𝐸)‘𝑧)) ↔ (𝑀 Fn ((𝑂 Func 𝑆) × 𝐵) ∧ ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧) ∈ (((1st ‘𝑍)‘𝑧)(Hom ‘𝑇)((1st ‘𝐸)‘𝑧)))) | 
| 71 | 5, 65, 70 | sylanbrc 583 | . 2
⊢ (𝜑 → 𝑀 ∈ X𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(((1st ‘𝑍)‘𝑧)(Hom ‘𝑇)((1st ‘𝐸)‘𝑧))) | 
| 72 | 17 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝐶 ∈ Cat) | 
| 73 | 19 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝑉 ∈ 𝑊) | 
| 74 | 21 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ran (Homf
‘𝐶) ⊆ 𝑈) | 
| 75 | 23 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (ran (Homf
‘𝑄) ∪ 𝑈) ⊆ 𝑉) | 
| 76 |  | simpr1 1194 | . . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)) | 
| 77 |  | xp1st 8047 | . . . . . 6
⊢ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) → (1st ‘𝑧) ∈ (𝑂 Func 𝑆)) | 
| 78 | 76, 77 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (1st ‘𝑧) ∈ (𝑂 Func 𝑆)) | 
| 79 |  | xp2nd 8048 | . . . . . 6
⊢ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) → (2nd ‘𝑧) ∈ 𝐵) | 
| 80 | 76, 79 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (2nd ‘𝑧) ∈ 𝐵) | 
| 81 |  | simpr2 1195 | . . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵)) | 
| 82 |  | xp1st 8047 | . . . . . 6
⊢ (𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) → (1st ‘𝑤) ∈ (𝑂 Func 𝑆)) | 
| 83 | 81, 82 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (1st ‘𝑤) ∈ (𝑂 Func 𝑆)) | 
| 84 |  | xp2nd 8048 | . . . . . 6
⊢ (𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) → (2nd ‘𝑤) ∈ 𝐵) | 
| 85 | 81, 84 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (2nd ‘𝑤) ∈ 𝐵) | 
| 86 |  | simpr3 1196 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤)) | 
| 87 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆) | 
| 88 | 12, 87 | fuchom 18010 | . . . . . . . . 9
⊢ (𝑂 Nat 𝑆) = (Hom ‘𝑄) | 
| 89 |  | eqid 2736 | . . . . . . . . 9
⊢ (Hom
‘𝑂) = (Hom
‘𝑂) | 
| 90 |  | eqid 2736 | . . . . . . . . 9
⊢ (Hom
‘(𝑄
×c 𝑂)) = (Hom ‘(𝑄 ×c 𝑂)) | 
| 91 | 30, 33, 88, 89, 90, 76, 81 | xpchom 18226 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤) = (((1st ‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤)) × ((2nd ‘𝑧)(Hom ‘𝑂)(2nd ‘𝑤)))) | 
| 92 |  | eqid 2736 | . . . . . . . . . 10
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) | 
| 93 | 92, 9 | oppchom 17759 | . . . . . . . . 9
⊢
((2nd ‘𝑧)(Hom ‘𝑂)(2nd ‘𝑤)) = ((2nd ‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧)) | 
| 94 | 93 | xpeq2i 5711 | . . . . . . . 8
⊢
(((1st ‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤)) × ((2nd ‘𝑧)(Hom ‘𝑂)(2nd ‘𝑤))) = (((1st ‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤)) × ((2nd ‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧))) | 
| 95 | 91, 94 | eqtrdi 2792 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤) = (((1st ‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤)) × ((2nd ‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧)))) | 
| 96 | 86, 95 | eleqtrd 2842 | . . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝑔 ∈ (((1st ‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤)) × ((2nd ‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧)))) | 
| 97 |  | xp1st 8047 | . . . . . 6
⊢ (𝑔 ∈ (((1st
‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤)) × ((2nd ‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧))) → (1st ‘𝑔) ∈ ((1st
‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤))) | 
| 98 | 96, 97 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (1st ‘𝑔) ∈ ((1st
‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤))) | 
| 99 |  | xp2nd 8048 | . . . . . 6
⊢ (𝑔 ∈ (((1st
‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤)) × ((2nd ‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧))) → (2nd ‘𝑔) ∈ ((2nd
‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧))) | 
| 100 | 96, 99 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (2nd ‘𝑔) ∈ ((2nd
‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧))) | 
| 101 | 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 72, 73, 74, 75, 78, 80, 83, 85, 98, 100, 1 | yonedalem3b 18325 | . . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (((1st ‘𝑤)𝑀(2nd ‘𝑤))(〈((1st ‘𝑧)(1st ‘𝑍)(2nd ‘𝑧)), ((1st
‘𝑤)(1st
‘𝑍)(2nd
‘𝑤))〉(comp‘𝑇)((1st ‘𝑤)(1st ‘𝐸)(2nd ‘𝑤)))((1st ‘𝑔)(〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd
‘𝑍)〈(1st ‘𝑤), (2nd ‘𝑤)〉)(2nd
‘𝑔))) =
(((1st ‘𝑔)(〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd
‘𝐸)〈(1st ‘𝑤), (2nd ‘𝑤)〉)(2nd
‘𝑔))(〈((1st ‘𝑧)(1st ‘𝑍)(2nd ‘𝑧)), ((1st
‘𝑧)(1st
‘𝐸)(2nd
‘𝑧))〉(comp‘𝑇)((1st ‘𝑤)(1st ‘𝐸)(2nd ‘𝑤)))((1st ‘𝑧)𝑀(2nd ‘𝑧)))) | 
| 102 |  | 1st2nd2 8054 | . . . . . . . . . 10
⊢ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) | 
| 103 | 76, 102 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) | 
| 104 | 103 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((1st ‘𝑍)‘𝑧) = ((1st ‘𝑍)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) | 
| 105 |  | df-ov 7435 | . . . . . . . 8
⊢
((1st ‘𝑧)(1st ‘𝑍)(2nd ‘𝑧)) = ((1st ‘𝑍)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉) | 
| 106 | 104, 105 | eqtr4di 2794 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((1st ‘𝑍)‘𝑧) = ((1st ‘𝑧)(1st ‘𝑍)(2nd ‘𝑧))) | 
| 107 |  | 1st2nd2 8054 | . . . . . . . . . 10
⊢ (𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) → 𝑤 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉) | 
| 108 | 81, 107 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝑤 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉) | 
| 109 | 108 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((1st ‘𝑍)‘𝑤) = ((1st ‘𝑍)‘〈(1st ‘𝑤), (2nd ‘𝑤)〉)) | 
| 110 |  | df-ov 7435 | . . . . . . . 8
⊢
((1st ‘𝑤)(1st ‘𝑍)(2nd ‘𝑤)) = ((1st ‘𝑍)‘〈(1st
‘𝑤), (2nd
‘𝑤)〉) | 
| 111 | 109, 110 | eqtr4di 2794 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((1st ‘𝑍)‘𝑤) = ((1st ‘𝑤)(1st ‘𝑍)(2nd ‘𝑤))) | 
| 112 | 106, 111 | opeq12d 4880 | . . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 〈((1st
‘𝑍)‘𝑧), ((1st ‘𝑍)‘𝑤)〉 = 〈((1st ‘𝑧)(1st ‘𝑍)(2nd ‘𝑧)), ((1st
‘𝑤)(1st
‘𝑍)(2nd
‘𝑤))〉) | 
| 113 | 108 | fveq2d 6909 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((1st ‘𝐸)‘𝑤) = ((1st ‘𝐸)‘〈(1st ‘𝑤), (2nd ‘𝑤)〉)) | 
| 114 |  | df-ov 7435 | . . . . . . 7
⊢
((1st ‘𝑤)(1st ‘𝐸)(2nd ‘𝑤)) = ((1st ‘𝐸)‘〈(1st
‘𝑤), (2nd
‘𝑤)〉) | 
| 115 | 113, 114 | eqtr4di 2794 | . . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((1st ‘𝐸)‘𝑤) = ((1st ‘𝑤)(1st ‘𝐸)(2nd ‘𝑤))) | 
| 116 | 112, 115 | oveq12d 7450 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (〈((1st
‘𝑍)‘𝑧), ((1st ‘𝑍)‘𝑤)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤)) = (〈((1st ‘𝑧)(1st ‘𝑍)(2nd ‘𝑧)), ((1st
‘𝑤)(1st
‘𝑍)(2nd
‘𝑤))〉(comp‘𝑇)((1st ‘𝑤)(1st ‘𝐸)(2nd ‘𝑤)))) | 
| 117 | 108 | fveq2d 6909 | . . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (𝑀‘𝑤) = (𝑀‘〈(1st ‘𝑤), (2nd ‘𝑤)〉)) | 
| 118 |  | df-ov 7435 | . . . . . 6
⊢
((1st ‘𝑤)𝑀(2nd ‘𝑤)) = (𝑀‘〈(1st ‘𝑤), (2nd ‘𝑤)〉) | 
| 119 | 117, 118 | eqtr4di 2794 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (𝑀‘𝑤) = ((1st ‘𝑤)𝑀(2nd ‘𝑤))) | 
| 120 | 103, 108 | oveq12d 7450 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (𝑧(2nd ‘𝑍)𝑤) = (〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd
‘𝑍)〈(1st ‘𝑤), (2nd ‘𝑤)〉)) | 
| 121 |  | 1st2nd2 8054 | . . . . . . . 8
⊢ (𝑔 ∈ (((1st
‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤)) × ((2nd ‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧))) → 𝑔 = 〈(1st ‘𝑔), (2nd ‘𝑔)〉) | 
| 122 | 96, 121 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝑔 = 〈(1st ‘𝑔), (2nd ‘𝑔)〉) | 
| 123 | 120, 122 | fveq12d 6912 | . . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((𝑧(2nd ‘𝑍)𝑤)‘𝑔) = ((〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd
‘𝑍)〈(1st ‘𝑤), (2nd ‘𝑤)〉)‘〈(1st
‘𝑔), (2nd
‘𝑔)〉)) | 
| 124 |  | df-ov 7435 | . . . . . 6
⊢
((1st ‘𝑔)(〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd
‘𝑍)〈(1st ‘𝑤), (2nd ‘𝑤)〉)(2nd
‘𝑔)) =
((〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd ‘𝑍)〈(1st
‘𝑤), (2nd
‘𝑤)〉)‘〈(1st
‘𝑔), (2nd
‘𝑔)〉) | 
| 125 | 123, 124 | eqtr4di 2794 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((𝑧(2nd ‘𝑍)𝑤)‘𝑔) = ((1st ‘𝑔)(〈(1st
‘𝑧), (2nd
‘𝑧)〉(2nd ‘𝑍)〈(1st
‘𝑤), (2nd
‘𝑤)〉)(2nd ‘𝑔))) | 
| 126 | 116, 119,
125 | oveq123d 7453 | . . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((𝑀‘𝑤)(〈((1st ‘𝑍)‘𝑧), ((1st ‘𝑍)‘𝑤)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤))((𝑧(2nd ‘𝑍)𝑤)‘𝑔)) = (((1st ‘𝑤)𝑀(2nd ‘𝑤))(〈((1st ‘𝑧)(1st ‘𝑍)(2nd ‘𝑧)), ((1st
‘𝑤)(1st
‘𝑍)(2nd
‘𝑤))〉(comp‘𝑇)((1st ‘𝑤)(1st ‘𝐸)(2nd ‘𝑤)))((1st ‘𝑔)(〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd
‘𝑍)〈(1st ‘𝑤), (2nd ‘𝑤)〉)(2nd
‘𝑔)))) | 
| 127 | 103 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((1st ‘𝐸)‘𝑧) = ((1st ‘𝐸)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) | 
| 128 |  | df-ov 7435 | . . . . . . . 8
⊢
((1st ‘𝑧)(1st ‘𝐸)(2nd ‘𝑧)) = ((1st ‘𝐸)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉) | 
| 129 | 127, 128 | eqtr4di 2794 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((1st ‘𝐸)‘𝑧) = ((1st ‘𝑧)(1st ‘𝐸)(2nd ‘𝑧))) | 
| 130 | 106, 129 | opeq12d 4880 | . . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 〈((1st
‘𝑍)‘𝑧), ((1st ‘𝐸)‘𝑧)〉 = 〈((1st ‘𝑧)(1st ‘𝑍)(2nd ‘𝑧)), ((1st
‘𝑧)(1st
‘𝐸)(2nd
‘𝑧))〉) | 
| 131 | 130, 115 | oveq12d 7450 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (〈((1st
‘𝑍)‘𝑧), ((1st ‘𝐸)‘𝑧)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤)) = (〈((1st ‘𝑧)(1st ‘𝑍)(2nd ‘𝑧)), ((1st
‘𝑧)(1st
‘𝐸)(2nd
‘𝑧))〉(comp‘𝑇)((1st ‘𝑤)(1st ‘𝐸)(2nd ‘𝑤)))) | 
| 132 | 103, 108 | oveq12d 7450 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (𝑧(2nd ‘𝐸)𝑤) = (〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd
‘𝐸)〈(1st ‘𝑤), (2nd ‘𝑤)〉)) | 
| 133 | 132, 122 | fveq12d 6912 | . . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((𝑧(2nd ‘𝐸)𝑤)‘𝑔) = ((〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd
‘𝐸)〈(1st ‘𝑤), (2nd ‘𝑤)〉)‘〈(1st
‘𝑔), (2nd
‘𝑔)〉)) | 
| 134 |  | df-ov 7435 | . . . . . 6
⊢
((1st ‘𝑔)(〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd
‘𝐸)〈(1st ‘𝑤), (2nd ‘𝑤)〉)(2nd
‘𝑔)) =
((〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd ‘𝐸)〈(1st
‘𝑤), (2nd
‘𝑤)〉)‘〈(1st
‘𝑔), (2nd
‘𝑔)〉) | 
| 135 | 133, 134 | eqtr4di 2794 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((𝑧(2nd ‘𝐸)𝑤)‘𝑔) = ((1st ‘𝑔)(〈(1st
‘𝑧), (2nd
‘𝑧)〉(2nd ‘𝐸)〈(1st
‘𝑤), (2nd
‘𝑤)〉)(2nd ‘𝑔))) | 
| 136 | 103 | fveq2d 6909 | . . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (𝑀‘𝑧) = (𝑀‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) | 
| 137 |  | df-ov 7435 | . . . . . 6
⊢
((1st ‘𝑧)𝑀(2nd ‘𝑧)) = (𝑀‘〈(1st ‘𝑧), (2nd ‘𝑧)〉) | 
| 138 | 136, 137 | eqtr4di 2794 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (𝑀‘𝑧) = ((1st ‘𝑧)𝑀(2nd ‘𝑧))) | 
| 139 | 131, 135,
138 | oveq123d 7453 | . . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (((𝑧(2nd ‘𝐸)𝑤)‘𝑔)(〈((1st ‘𝑍)‘𝑧), ((1st ‘𝐸)‘𝑧)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤))(𝑀‘𝑧)) = (((1st ‘𝑔)(〈(1st
‘𝑧), (2nd
‘𝑧)〉(2nd ‘𝐸)〈(1st
‘𝑤), (2nd
‘𝑤)〉)(2nd ‘𝑔))(〈((1st
‘𝑧)(1st
‘𝑍)(2nd
‘𝑧)),
((1st ‘𝑧)(1st ‘𝐸)(2nd ‘𝑧))〉(comp‘𝑇)((1st ‘𝑤)(1st ‘𝐸)(2nd ‘𝑤)))((1st ‘𝑧)𝑀(2nd ‘𝑧)))) | 
| 140 | 101, 126,
139 | 3eqtr4d 2786 | . . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((𝑀‘𝑤)(〈((1st ‘𝑍)‘𝑧), ((1st ‘𝑍)‘𝑤)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤))((𝑧(2nd ‘𝑍)𝑤)‘𝑔)) = (((𝑧(2nd ‘𝐸)𝑤)‘𝑔)(〈((1st ‘𝑍)‘𝑧), ((1st ‘𝐸)‘𝑧)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤))(𝑀‘𝑧))) | 
| 141 | 140 | ralrimivvva 3204 | . 2
⊢ (𝜑 → ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)∀𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵)∀𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤)((𝑀‘𝑤)(〈((1st ‘𝑍)‘𝑧), ((1st ‘𝑍)‘𝑤)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤))((𝑧(2nd ‘𝑍)𝑤)‘𝑔)) = (((𝑧(2nd ‘𝐸)𝑤)‘𝑔)(〈((1st ‘𝑍)‘𝑧), ((1st ‘𝐸)‘𝑧)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤))(𝑀‘𝑧))) | 
| 142 |  | eqid 2736 | . . 3
⊢ ((𝑄 ×c
𝑂) Nat 𝑇) = ((𝑄 ×c 𝑂) Nat 𝑇) | 
| 143 |  | eqid 2736 | . . 3
⊢
(comp‘𝑇) =
(comp‘𝑇) | 
| 144 | 142, 33, 90, 29, 143, 37, 44 | isnat2 17997 | . 2
⊢ (𝜑 → (𝑀 ∈ (𝑍((𝑄 ×c 𝑂) Nat 𝑇)𝐸) ↔ (𝑀 ∈ X𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(((1st ‘𝑍)‘𝑧)(Hom ‘𝑇)((1st ‘𝐸)‘𝑧)) ∧ ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)∀𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵)∀𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤)((𝑀‘𝑤)(〈((1st ‘𝑍)‘𝑧), ((1st ‘𝑍)‘𝑤)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤))((𝑧(2nd ‘𝑍)𝑤)‘𝑔)) = (((𝑧(2nd ‘𝐸)𝑤)‘𝑔)(〈((1st ‘𝑍)‘𝑧), ((1st ‘𝐸)‘𝑧)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤))(𝑀‘𝑧))))) | 
| 145 | 71, 141, 144 | mpbir2and 713 | 1
⊢ (𝜑 → 𝑀 ∈ (𝑍((𝑄 ×c 𝑂) Nat 𝑇)𝐸)) |