Step | Hyp | Ref
| Expression |
1 | | yoneda.m |
. . . . 5
⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥)))) |
2 | | ovex 6577 |
. . . . . 6
⊢
(((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ∈ V |
3 | 2 | mptex 6390 |
. . . . 5
⊢ (𝑎 ∈ (((1st
‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))) ∈ V |
4 | 1, 3 | fnmpt2i 7128 |
. . . 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 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → 𝑔 ∈ (𝑂 Func 𝑆)) |
26 | | simprr 792 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
27 | 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 18, 20, 22, 24, 25, 26, 1 | yonedalem3a 16737 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → ((𝑔𝑀𝑦) = (𝑎 ∈ (((1st ‘𝑌)‘𝑦)(𝑂 Nat 𝑆)𝑔) ↦ ((𝑎‘𝑦)‘( 1 ‘𝑦))) ∧ (𝑔𝑀𝑦):(𝑔(1st ‘𝑍)𝑦)⟶(𝑔(1st ‘𝐸)𝑦))) |
28 | 27 | simprd 478 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → (𝑔𝑀𝑦):(𝑔(1st ‘𝑍)𝑦)⟶(𝑔(1st ‘𝐸)𝑦)) |
29 | | eqid 2610 |
. . . . . . 7
⊢ (Hom
‘𝑇) = (Hom
‘𝑇) |
30 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑄 ×c
𝑂) = (𝑄 ×c 𝑂) |
31 | 12 | fucbas 16443 |
. . . . . . . . . . 11
⊢ (𝑂 Func 𝑆) = (Base‘𝑄) |
32 | 9, 7 | oppcbas 16201 |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝑂) |
33 | 30, 31, 32 | xpcbas 16641 |
. . . . . . . . . 10
⊢ ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂)) |
34 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝑇) =
(Base‘𝑇) |
35 | | relfunc 16345 |
. . . . . . . . . . 11
⊢ Rel
((𝑄
×c 𝑂) Func 𝑇) |
36 | 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 19, 21, 23 | yonedalem1 16735 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))) |
37 | 36 | simpld 474 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) |
38 | | 1st2ndbr 7108 |
. . . . . . . . . . 11
⊢ ((Rel
((𝑄
×c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st ‘𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝑍)) |
39 | 35, 37, 38 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘𝑍)((𝑄 ×c
𝑂) Func 𝑇)(2nd ‘𝑍)) |
40 | 33, 34, 39 | funcf1 16349 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)) |
41 | 40 | fovrnda 6703 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → (𝑔(1st ‘𝑍)𝑦) ∈ (Base‘𝑇)) |
42 | 11, 20 | setcbas 16551 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → 𝑉 = (Base‘𝑇)) |
43 | 41, 42 | eleqtrrd 2691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → (𝑔(1st ‘𝑍)𝑦) ∈ 𝑉) |
44 | 36 | simprd 478 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) |
45 | | 1st2ndbr 7108 |
. . . . . . . . . . 11
⊢ ((Rel
((𝑄
×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st ‘𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝐸)) |
46 | 35, 44, 45 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘𝐸)((𝑄 ×c
𝑂) Func 𝑇)(2nd ‘𝐸)) |
47 | 33, 34, 46 | funcf1 16349 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)) |
48 | 47 | fovrnda 6703 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → (𝑔(1st ‘𝐸)𝑦) ∈ (Base‘𝑇)) |
49 | 48, 42 | eleqtrrd 2691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → (𝑔(1st ‘𝐸)𝑦) ∈ 𝑉) |
50 | 11, 20, 29, 43, 49 | elsetchom 16554 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → ((𝑔𝑀𝑦) ∈ ((𝑔(1st ‘𝑍)𝑦)(Hom ‘𝑇)(𝑔(1st ‘𝐸)𝑦)) ↔ (𝑔𝑀𝑦):(𝑔(1st ‘𝑍)𝑦)⟶(𝑔(1st ‘𝐸)𝑦))) |
51 | 28, 50 | mpbird 246 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ (𝑂 Func 𝑆) ∧ 𝑦 ∈ 𝐵)) → (𝑔𝑀𝑦) ∈ ((𝑔(1st ‘𝑍)𝑦)(Hom ‘𝑇)(𝑔(1st ‘𝐸)𝑦))) |
52 | 51 | ralrimivva 2954 |
. . . 4
⊢ (𝜑 → ∀𝑔 ∈ (𝑂 Func 𝑆)∀𝑦 ∈ 𝐵 (𝑔𝑀𝑦) ∈ ((𝑔(1st ‘𝑍)𝑦)(Hom ‘𝑇)(𝑔(1st ‘𝐸)𝑦))) |
53 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑧 = 〈𝑔, 𝑦〉 → (𝑀‘𝑧) = (𝑀‘〈𝑔, 𝑦〉)) |
54 | | df-ov 6552 |
. . . . . . 7
⊢ (𝑔𝑀𝑦) = (𝑀‘〈𝑔, 𝑦〉) |
55 | 53, 54 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑧 = 〈𝑔, 𝑦〉 → (𝑀‘𝑧) = (𝑔𝑀𝑦)) |
56 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑔, 𝑦〉 → ((1st ‘𝑍)‘𝑧) = ((1st ‘𝑍)‘〈𝑔, 𝑦〉)) |
57 | | df-ov 6552 |
. . . . . . . 8
⊢ (𝑔(1st ‘𝑍)𝑦) = ((1st ‘𝑍)‘〈𝑔, 𝑦〉) |
58 | 56, 57 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑧 = 〈𝑔, 𝑦〉 → ((1st ‘𝑍)‘𝑧) = (𝑔(1st ‘𝑍)𝑦)) |
59 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑔, 𝑦〉 → ((1st ‘𝐸)‘𝑧) = ((1st ‘𝐸)‘〈𝑔, 𝑦〉)) |
60 | | df-ov 6552 |
. . . . . . . 8
⊢ (𝑔(1st ‘𝐸)𝑦) = ((1st ‘𝐸)‘〈𝑔, 𝑦〉) |
61 | 59, 60 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑧 = 〈𝑔, 𝑦〉 → ((1st ‘𝐸)‘𝑧) = (𝑔(1st ‘𝐸)𝑦)) |
62 | 58, 61 | oveq12d 6567 |
. . . . . 6
⊢ (𝑧 = 〈𝑔, 𝑦〉 → (((1st ‘𝑍)‘𝑧)(Hom ‘𝑇)((1st ‘𝐸)‘𝑧)) = ((𝑔(1st ‘𝑍)𝑦)(Hom ‘𝑇)(𝑔(1st ‘𝐸)𝑦))) |
63 | 55, 62 | eleq12d 2682 |
. . . . 5
⊢ (𝑧 = 〈𝑔, 𝑦〉 → ((𝑀‘𝑧) ∈ (((1st ‘𝑍)‘𝑧)(Hom ‘𝑇)((1st ‘𝐸)‘𝑧)) ↔ (𝑔𝑀𝑦) ∈ ((𝑔(1st ‘𝑍)𝑦)(Hom ‘𝑇)(𝑔(1st ‘𝐸)𝑦)))) |
64 | 63 | ralxp 5185 |
. . . 4
⊢
(∀𝑧 ∈
((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧) ∈ (((1st ‘𝑍)‘𝑧)(Hom ‘𝑇)((1st ‘𝐸)‘𝑧)) ↔ ∀𝑔 ∈ (𝑂 Func 𝑆)∀𝑦 ∈ 𝐵 (𝑔𝑀𝑦) ∈ ((𝑔(1st ‘𝑍)𝑦)(Hom ‘𝑇)(𝑔(1st ‘𝐸)𝑦))) |
65 | 52, 64 | sylibr 223 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧) ∈ (((1st ‘𝑍)‘𝑧)(Hom ‘𝑇)((1st ‘𝐸)‘𝑧))) |
66 | | ovex 6577 |
. . . . . 6
⊢ (𝑂 Func 𝑆) ∈ V |
67 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝐶)
∈ V |
68 | 7, 67 | eqeltri 2684 |
. . . . . 6
⊢ 𝐵 ∈ V |
69 | 66, 68 | mpt2ex 7136 |
. . . . 5
⊢ (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥)))) ∈ V |
70 | 1, 69 | eqeltri 2684 |
. . . 4
⊢ 𝑀 ∈ V |
71 | 70 | elixp 7801 |
. . 3
⊢ (𝑀 ∈ X𝑧 ∈
((𝑂 Func 𝑆) × 𝐵)(((1st ‘𝑍)‘𝑧)(Hom ‘𝑇)((1st ‘𝐸)‘𝑧)) ↔ (𝑀 Fn ((𝑂 Func 𝑆) × 𝐵) ∧ ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧) ∈ (((1st ‘𝑍)‘𝑧)(Hom ‘𝑇)((1st ‘𝐸)‘𝑧)))) |
72 | 5, 65, 71 | sylanbrc 695 |
. 2
⊢ (𝜑 → 𝑀 ∈ X𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(((1st ‘𝑍)‘𝑧)(Hom ‘𝑇)((1st ‘𝐸)‘𝑧))) |
73 | 17 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝐶 ∈ Cat) |
74 | 19 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝑉 ∈ 𝑊) |
75 | 21 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ran (Homf
‘𝐶) ⊆ 𝑈) |
76 | 23 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (ran (Homf
‘𝑄) ∪ 𝑈) ⊆ 𝑉) |
77 | | simpr1 1060 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)) |
78 | | xp1st 7089 |
. . . . . 6
⊢ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) → (1st ‘𝑧) ∈ (𝑂 Func 𝑆)) |
79 | 77, 78 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (1st ‘𝑧) ∈ (𝑂 Func 𝑆)) |
80 | | xp2nd 7090 |
. . . . . 6
⊢ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) → (2nd ‘𝑧) ∈ 𝐵) |
81 | 77, 80 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (2nd ‘𝑧) ∈ 𝐵) |
82 | | simpr2 1061 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵)) |
83 | | xp1st 7089 |
. . . . . 6
⊢ (𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) → (1st ‘𝑤) ∈ (𝑂 Func 𝑆)) |
84 | 82, 83 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (1st ‘𝑤) ∈ (𝑂 Func 𝑆)) |
85 | | xp2nd 7090 |
. . . . . 6
⊢ (𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) → (2nd ‘𝑤) ∈ 𝐵) |
86 | 82, 85 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (2nd ‘𝑤) ∈ 𝐵) |
87 | | simpr3 1062 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤)) |
88 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆) |
89 | 12, 88 | fuchom 16444 |
. . . . . . . . 9
⊢ (𝑂 Nat 𝑆) = (Hom ‘𝑄) |
90 | | eqid 2610 |
. . . . . . . . 9
⊢ (Hom
‘𝑂) = (Hom
‘𝑂) |
91 | | eqid 2610 |
. . . . . . . . 9
⊢ (Hom
‘(𝑄
×c 𝑂)) = (Hom ‘(𝑄 ×c 𝑂)) |
92 | 30, 33, 89, 90, 91, 77, 82 | xpchom 16643 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤) = (((1st ‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤)) × ((2nd ‘𝑧)(Hom ‘𝑂)(2nd ‘𝑤)))) |
93 | | eqid 2610 |
. . . . . . . . . 10
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
94 | 93, 9 | oppchom 16198 |
. . . . . . . . 9
⊢
((2nd ‘𝑧)(Hom ‘𝑂)(2nd ‘𝑤)) = ((2nd ‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧)) |
95 | 94 | xpeq2i 5060 |
. . . . . . . 8
⊢
(((1st ‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤)) × ((2nd ‘𝑧)(Hom ‘𝑂)(2nd ‘𝑤))) = (((1st ‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤)) × ((2nd ‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧))) |
96 | 92, 95 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤) = (((1st ‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤)) × ((2nd ‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧)))) |
97 | 87, 96 | eleqtrd 2690 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝑔 ∈ (((1st ‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤)) × ((2nd ‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧)))) |
98 | | xp1st 7089 |
. . . . . 6
⊢ (𝑔 ∈ (((1st
‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤)) × ((2nd ‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧))) → (1st ‘𝑔) ∈ ((1st
‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤))) |
99 | 97, 98 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (1st ‘𝑔) ∈ ((1st
‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤))) |
100 | | xp2nd 7090 |
. . . . . 6
⊢ (𝑔 ∈ (((1st
‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤)) × ((2nd ‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧))) → (2nd ‘𝑔) ∈ ((2nd
‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧))) |
101 | 97, 100 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (2nd ‘𝑔) ∈ ((2nd
‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧))) |
102 | 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 73, 74, 75, 76, 79, 81, 84, 86, 99, 101, 1 | yonedalem3b 16742 |
. . . 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 ‘𝑧)))) |
103 | | 1st2nd2 7096 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
104 | 77, 103 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
105 | 104 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((1st ‘𝑍)‘𝑧) = ((1st ‘𝑍)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
106 | | df-ov 6552 |
. . . . . . . 8
⊢
((1st ‘𝑧)(1st ‘𝑍)(2nd ‘𝑧)) = ((1st ‘𝑍)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
107 | 105, 106 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((1st ‘𝑍)‘𝑧) = ((1st ‘𝑧)(1st ‘𝑍)(2nd ‘𝑧))) |
108 | | 1st2nd2 7096 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) → 𝑤 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉) |
109 | 82, 108 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝑤 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉) |
110 | 109 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((1st ‘𝑍)‘𝑤) = ((1st ‘𝑍)‘〈(1st ‘𝑤), (2nd ‘𝑤)〉)) |
111 | | df-ov 6552 |
. . . . . . . 8
⊢
((1st ‘𝑤)(1st ‘𝑍)(2nd ‘𝑤)) = ((1st ‘𝑍)‘〈(1st
‘𝑤), (2nd
‘𝑤)〉) |
112 | 110, 111 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((1st ‘𝑍)‘𝑤) = ((1st ‘𝑤)(1st ‘𝑍)(2nd ‘𝑤))) |
113 | 107, 112 | opeq12d 4348 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 〈((1st
‘𝑍)‘𝑧), ((1st ‘𝑍)‘𝑤)〉 = 〈((1st ‘𝑧)(1st ‘𝑍)(2nd ‘𝑧)), ((1st
‘𝑤)(1st
‘𝑍)(2nd
‘𝑤))〉) |
114 | 109 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((1st ‘𝐸)‘𝑤) = ((1st ‘𝐸)‘〈(1st ‘𝑤), (2nd ‘𝑤)〉)) |
115 | | df-ov 6552 |
. . . . . . 7
⊢
((1st ‘𝑤)(1st ‘𝐸)(2nd ‘𝑤)) = ((1st ‘𝐸)‘〈(1st
‘𝑤), (2nd
‘𝑤)〉) |
116 | 114, 115 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((1st ‘𝐸)‘𝑤) = ((1st ‘𝑤)(1st ‘𝐸)(2nd ‘𝑤))) |
117 | 113, 116 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (〈((1st
‘𝑍)‘𝑧), ((1st ‘𝑍)‘𝑤)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤)) = (〈((1st ‘𝑧)(1st ‘𝑍)(2nd ‘𝑧)), ((1st
‘𝑤)(1st
‘𝑍)(2nd
‘𝑤))〉(comp‘𝑇)((1st ‘𝑤)(1st ‘𝐸)(2nd ‘𝑤)))) |
118 | 109 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (𝑀‘𝑤) = (𝑀‘〈(1st ‘𝑤), (2nd ‘𝑤)〉)) |
119 | | df-ov 6552 |
. . . . . 6
⊢
((1st ‘𝑤)𝑀(2nd ‘𝑤)) = (𝑀‘〈(1st ‘𝑤), (2nd ‘𝑤)〉) |
120 | 118, 119 | syl6eqr 2662 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (𝑀‘𝑤) = ((1st ‘𝑤)𝑀(2nd ‘𝑤))) |
121 | 104, 109 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (𝑧(2nd ‘𝑍)𝑤) = (〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd
‘𝑍)〈(1st ‘𝑤), (2nd ‘𝑤)〉)) |
122 | | 1st2nd2 7096 |
. . . . . . . 8
⊢ (𝑔 ∈ (((1st
‘𝑧)(𝑂 Nat 𝑆)(1st ‘𝑤)) × ((2nd ‘𝑤)(Hom ‘𝐶)(2nd ‘𝑧))) → 𝑔 = 〈(1st ‘𝑔), (2nd ‘𝑔)〉) |
123 | 97, 122 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 𝑔 = 〈(1st ‘𝑔), (2nd ‘𝑔)〉) |
124 | 121, 123 | fveq12d 6109 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((𝑧(2nd ‘𝑍)𝑤)‘𝑔) = ((〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd
‘𝑍)〈(1st ‘𝑤), (2nd ‘𝑤)〉)‘〈(1st
‘𝑔), (2nd
‘𝑔)〉)) |
125 | | df-ov 6552 |
. . . . . 6
⊢
((1st ‘𝑔)(〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd
‘𝑍)〈(1st ‘𝑤), (2nd ‘𝑤)〉)(2nd
‘𝑔)) =
((〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd ‘𝑍)〈(1st
‘𝑤), (2nd
‘𝑤)〉)‘〈(1st
‘𝑔), (2nd
‘𝑔)〉) |
126 | 124, 125 | syl6eqr 2662 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((𝑧(2nd ‘𝑍)𝑤)‘𝑔) = ((1st ‘𝑔)(〈(1st
‘𝑧), (2nd
‘𝑧)〉(2nd ‘𝑍)〈(1st
‘𝑤), (2nd
‘𝑤)〉)(2nd ‘𝑔))) |
127 | 117, 120,
126 | oveq123d 6570 |
. . . 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
‘𝑔)))) |
128 | 104 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((1st ‘𝐸)‘𝑧) = ((1st ‘𝐸)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
129 | | df-ov 6552 |
. . . . . . . 8
⊢
((1st ‘𝑧)(1st ‘𝐸)(2nd ‘𝑧)) = ((1st ‘𝐸)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
130 | 128, 129 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((1st ‘𝐸)‘𝑧) = ((1st ‘𝑧)(1st ‘𝐸)(2nd ‘𝑧))) |
131 | 107, 130 | opeq12d 4348 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → 〈((1st
‘𝑍)‘𝑧), ((1st ‘𝐸)‘𝑧)〉 = 〈((1st ‘𝑧)(1st ‘𝑍)(2nd ‘𝑧)), ((1st
‘𝑧)(1st
‘𝐸)(2nd
‘𝑧))〉) |
132 | 131, 116 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (〈((1st
‘𝑍)‘𝑧), ((1st ‘𝐸)‘𝑧)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤)) = (〈((1st ‘𝑧)(1st ‘𝑍)(2nd ‘𝑧)), ((1st
‘𝑧)(1st
‘𝐸)(2nd
‘𝑧))〉(comp‘𝑇)((1st ‘𝑤)(1st ‘𝐸)(2nd ‘𝑤)))) |
133 | 104, 109 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (𝑧(2nd ‘𝐸)𝑤) = (〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd
‘𝐸)〈(1st ‘𝑤), (2nd ‘𝑤)〉)) |
134 | 133, 123 | fveq12d 6109 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((𝑧(2nd ‘𝐸)𝑤)‘𝑔) = ((〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd
‘𝐸)〈(1st ‘𝑤), (2nd ‘𝑤)〉)‘〈(1st
‘𝑔), (2nd
‘𝑔)〉)) |
135 | | df-ov 6552 |
. . . . . 6
⊢
((1st ‘𝑔)(〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd
‘𝐸)〈(1st ‘𝑤), (2nd ‘𝑤)〉)(2nd
‘𝑔)) =
((〈(1st ‘𝑧), (2nd ‘𝑧)〉(2nd ‘𝐸)〈(1st
‘𝑤), (2nd
‘𝑤)〉)‘〈(1st
‘𝑔), (2nd
‘𝑔)〉) |
136 | 134, 135 | syl6eqr 2662 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((𝑧(2nd ‘𝐸)𝑤)‘𝑔) = ((1st ‘𝑔)(〈(1st
‘𝑧), (2nd
‘𝑧)〉(2nd ‘𝐸)〈(1st
‘𝑤), (2nd
‘𝑤)〉)(2nd ‘𝑔))) |
137 | 104 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (𝑀‘𝑧) = (𝑀‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
138 | | df-ov 6552 |
. . . . . 6
⊢
((1st ‘𝑧)𝑀(2nd ‘𝑧)) = (𝑀‘〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
139 | 137, 138 | syl6eqr 2662 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → (𝑀‘𝑧) = ((1st ‘𝑧)𝑀(2nd ‘𝑧))) |
140 | 132, 136,
139 | oveq123d 6570 |
. . . 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 ‘𝑧)))) |
141 | 102, 127,
140 | 3eqtr4d 2654 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤))) → ((𝑀‘𝑤)(〈((1st ‘𝑍)‘𝑧), ((1st ‘𝑍)‘𝑤)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤))((𝑧(2nd ‘𝑍)𝑤)‘𝑔)) = (((𝑧(2nd ‘𝐸)𝑤)‘𝑔)(〈((1st ‘𝑍)‘𝑧), ((1st ‘𝐸)‘𝑧)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤))(𝑀‘𝑧))) |
142 | 141 | ralrimivvva 2955 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)∀𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵)∀𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤)((𝑀‘𝑤)(〈((1st ‘𝑍)‘𝑧), ((1st ‘𝑍)‘𝑤)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤))((𝑧(2nd ‘𝑍)𝑤)‘𝑔)) = (((𝑧(2nd ‘𝐸)𝑤)‘𝑔)(〈((1st ‘𝑍)‘𝑧), ((1st ‘𝐸)‘𝑧)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤))(𝑀‘𝑧))) |
143 | | eqid 2610 |
. . 3
⊢ ((𝑄 ×c
𝑂) Nat 𝑇) = ((𝑄 ×c 𝑂) Nat 𝑇) |
144 | | eqid 2610 |
. . 3
⊢
(comp‘𝑇) =
(comp‘𝑇) |
145 | 143, 33, 91, 29, 144, 37, 44 | isnat2 16431 |
. 2
⊢ (𝜑 → (𝑀 ∈ (𝑍((𝑄 ×c 𝑂) Nat 𝑇)𝐸) ↔ (𝑀 ∈ X𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(((1st ‘𝑍)‘𝑧)(Hom ‘𝑇)((1st ‘𝐸)‘𝑧)) ∧ ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)∀𝑤 ∈ ((𝑂 Func 𝑆) × 𝐵)∀𝑔 ∈ (𝑧(Hom ‘(𝑄 ×c 𝑂))𝑤)((𝑀‘𝑤)(〈((1st ‘𝑍)‘𝑧), ((1st ‘𝑍)‘𝑤)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤))((𝑧(2nd ‘𝑍)𝑤)‘𝑔)) = (((𝑧(2nd ‘𝐸)𝑤)‘𝑔)(〈((1st ‘𝑍)‘𝑧), ((1st ‘𝐸)‘𝑧)〉(comp‘𝑇)((1st ‘𝐸)‘𝑤))(𝑀‘𝑧))))) |
146 | 72, 142, 145 | mpbir2and 959 |
1
⊢ (𝜑 → 𝑀 ∈ (𝑍((𝑄 ×c 𝑂) Nat 𝑇)𝐸)) |