Step | Hyp | Ref
| Expression |
1 | | yoneda.r |
. . 3
⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇) |
2 | | eqid 2610 |
. . . 4
⊢ (𝑄 ×c
𝑂) = (𝑄 ×c 𝑂) |
3 | | yoneda.q |
. . . . 5
⊢ 𝑄 = (𝑂 FuncCat 𝑆) |
4 | 3 | fucbas 16443 |
. . . 4
⊢ (𝑂 Func 𝑆) = (Base‘𝑄) |
5 | | yoneda.o |
. . . . 5
⊢ 𝑂 = (oppCat‘𝐶) |
6 | | yoneda.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐶) |
7 | 5, 6 | oppcbas 16201 |
. . . 4
⊢ 𝐵 = (Base‘𝑂) |
8 | 2, 4, 7 | xpcbas 16641 |
. . 3
⊢ ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂)) |
9 | | eqid 2610 |
. . 3
⊢ ((𝑄 ×c
𝑂) Nat 𝑇) = ((𝑄 ×c 𝑂) Nat 𝑇) |
10 | | yoneda.y |
. . . . 5
⊢ 𝑌 = (Yon‘𝐶) |
11 | | yoneda.1 |
. . . . 5
⊢ 1 =
(Id‘𝐶) |
12 | | yoneda.s |
. . . . 5
⊢ 𝑆 = (SetCat‘𝑈) |
13 | | yoneda.t |
. . . . 5
⊢ 𝑇 = (SetCat‘𝑉) |
14 | | yoneda.h |
. . . . 5
⊢ 𝐻 =
(HomF‘𝑄) |
15 | | yoneda.e |
. . . . 5
⊢ 𝐸 = (𝑂 evalF 𝑆) |
16 | | yoneda.z |
. . . . 5
⊢ 𝑍 = (𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂))) |
17 | | yoneda.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ Cat) |
18 | | yoneda.w |
. . . . 5
⊢ (𝜑 → 𝑉 ∈ 𝑊) |
19 | | yoneda.u |
. . . . 5
⊢ (𝜑 → ran
(Homf ‘𝐶) ⊆ 𝑈) |
20 | | yoneda.v |
. . . . 5
⊢ (𝜑 → (ran
(Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) |
21 | 10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20 | yonedalem1 16735 |
. . . 4
⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))) |
22 | 21 | simpld 474 |
. . 3
⊢ (𝜑 → 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) |
23 | 21 | simprd 478 |
. . 3
⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) |
24 | | yonedainv.i |
. . 3
⊢ 𝐼 = (Inv‘𝑅) |
25 | | eqid 2610 |
. . 3
⊢
(Inv‘𝑇) =
(Inv‘𝑇) |
26 | | yoneda.m |
. . . 4
⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥)))) |
27 | 10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20, 26 | yonedalem3 16743 |
. . 3
⊢ (𝜑 → 𝑀 ∈ (𝑍((𝑄 ×c 𝑂) Nat 𝑇)𝐸)) |
28 | 17 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝐶 ∈ Cat) |
29 | 18 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑉 ∈ 𝑊) |
30 | 19 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ran (Homf
‘𝐶) ⊆ 𝑈) |
31 | 20 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ran (Homf
‘𝑄) ∪ 𝑈) ⊆ 𝑉) |
32 | | simprl 790 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ℎ ∈ (𝑂 Func 𝑆)) |
33 | | simprr 792 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑤 ∈ 𝐵) |
34 | 10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33, 26 | yonedalem3a 16737 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤))) |
35 | 34 | simprd 478 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)) |
36 | 28 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → 𝐶 ∈ Cat) |
37 | 29 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑉 ∈ 𝑊) |
38 | 30 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → ran (Homf
‘𝐶) ⊆ 𝑈) |
39 | 31 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → (ran (Homf
‘𝑄) ∪ 𝑈) ⊆ 𝑉) |
40 | | simplrl 796 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → ℎ ∈ (𝑂 Func 𝑆)) |
41 | | simplrr 797 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑤 ∈ 𝐵) |
42 | | yonedainv.n |
. . . . . . . . . . . 12
⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢))))) |
43 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) |
44 | 10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 36, 37, 38, 39, 40, 41, 42, 43 | yonedalem4c 16740 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑁𝑤)‘𝑏) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)) |
45 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ((1st
‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)) = (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)) |
46 | 44, 45 | fmptd 6292 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)):((1st ‘ℎ)‘𝑤)⟶(((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)) |
47 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝐶)
∈ V |
48 | 6, 47 | eqeltri 2684 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 ∈ V |
49 | 48 | mptex 6390 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))) ∈ V |
50 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ ((1st
‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) |
51 | 49, 50 | fnmpti 5935 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ((1st
‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) Fn ((1st ‘ℎ)‘𝑤) |
52 | | simpl 472 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → 𝑓 = ℎ) |
53 | 52 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (1st ‘𝑓) = (1st ‘ℎ)) |
54 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → 𝑥 = 𝑤) |
55 | 53, 54 | fveq12d 6109 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → ((1st ‘𝑓)‘𝑥) = ((1st ‘ℎ)‘𝑤)) |
56 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑥 = 𝑤) |
57 | 56 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐶)𝑤)) |
58 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑓 = ℎ) |
59 | 58 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (2nd ‘𝑓) = (2nd ‘ℎ)) |
60 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑦 = 𝑦) |
61 | 59, 56, 60 | oveq123d 6570 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑥(2nd ‘𝑓)𝑦) = (𝑤(2nd ‘ℎ)𝑦)) |
62 | 61 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → ((𝑥(2nd ‘𝑓)𝑦)‘𝑔) = ((𝑤(2nd ‘ℎ)𝑦)‘𝑔)) |
63 | 62 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢) = (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)) |
64 | 57, 63 | mpteq12dv 4663 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)) = (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))) |
65 | 64 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢))) = (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) |
66 | 55, 65 | mpteq12dv 4663 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))))) |
67 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘ℎ)‘𝑤) ∈ V |
68 | 67 | mptex 6390 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ((1st
‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) ∈ V |
69 | 66, 42, 68 | ovmpt2a 6689 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵) → (ℎ𝑁𝑤) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))))) |
70 | 69 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))))) |
71 | 70 | fneq1d 5895 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) Fn ((1st ‘ℎ)‘𝑤) ↔ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) Fn ((1st ‘ℎ)‘𝑤))) |
72 | 51, 71 | mpbiri 247 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) Fn ((1st ‘ℎ)‘𝑤)) |
73 | | dffn5 6151 |
. . . . . . . . . . . 12
⊢ ((ℎ𝑁𝑤) Fn ((1st ‘ℎ)‘𝑤) ↔ (ℎ𝑁𝑤) = (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏))) |
74 | 72, 73 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) = (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏))) |
75 | 5 | oppccat 16205 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat) |
76 | 17, 75 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑂 ∈ Cat) |
77 | 76 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑂 ∈ Cat) |
78 | 20 | unssbd 3753 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ⊆ 𝑉) |
79 | 18, 78 | ssexd 4733 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ∈ V) |
80 | 12 | setccat 16558 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ V → 𝑆 ∈ Cat) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ Cat) |
82 | 81 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑆 ∈ Cat) |
83 | 15, 77, 82, 7, 32, 33 | evlf1 16683 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝐸)𝑤) = ((1st ‘ℎ)‘𝑤)) |
84 | 10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33 | yonedalem21 16736 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝑍)𝑤) = (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)) |
85 | 74, 83, 84 | feq123d 5947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤) ↔ (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)):((1st ‘ℎ)‘𝑤)⟶(((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))) |
86 | 46, 85 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤)) |
87 | | fcompt 6306 |
. . . . . . . . . . 11
⊢ (((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)))) |
88 | 35, 86, 87 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)))) |
89 | 83 | eleq2d 2673 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↔ 𝑘 ∈ ((1st ‘ℎ)‘𝑤))) |
90 | 89 | biimpa 500 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ (ℎ(1st ‘𝐸)𝑤)) → 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) |
91 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝐶 ∈ Cat) |
92 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑉 ∈ 𝑊) |
93 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ran (Homf
‘𝐶) ⊆ 𝑈) |
94 | 31 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (ran (Homf
‘𝑄) ∪ 𝑈) ⊆ 𝑉) |
95 | | simplrl 796 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ℎ ∈ (𝑂 Func 𝑆)) |
96 | | simplrr 797 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑤 ∈ 𝐵) |
97 | 10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 91, 92, 93, 94, 95, 96, 26 | yonedalem3a 16737 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤))) |
98 | 97 | simpld 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))) |
99 | 98 | fveq1d 6105 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘((ℎ𝑁𝑤)‘𝑘))) |
100 | | fvex 6113 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ℎ𝑁𝑤)‘𝑏) ∈ V |
101 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑁𝑤)‘𝑏) ∈ V) |
102 | 101, 74, 44 | fmpt2d 6300 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤):((1st ‘ℎ)‘𝑤)⟶(((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)) |
103 | 102 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑁𝑤)‘𝑘) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)) |
104 | | fveq1 6102 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = ((ℎ𝑁𝑤)‘𝑘) → (𝑎‘𝑤) = (((ℎ𝑁𝑤)‘𝑘)‘𝑤)) |
105 | 104 | fveq1d 6105 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = ((ℎ𝑁𝑤)‘𝑘) → ((𝑎‘𝑤)‘( 1 ‘𝑤)) = ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤))) |
106 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (((1st
‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) |
107 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢ ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) ∈ V |
108 | 105, 106,
107 | fvmpt 6191 |
. . . . . . . . . . . . . . 15
⊢ (((ℎ𝑁𝑤)‘𝑘) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘((ℎ𝑁𝑤)‘𝑘)) = ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤))) |
109 | 103, 108 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘((ℎ𝑁𝑤)‘𝑘)) = ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤))) |
110 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) |
111 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
112 | 6, 111, 11, 91, 96 | catidcl 16166 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ( 1 ‘𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤)) |
113 | 10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 91, 92, 93, 94, 95, 96, 42, 110, 96, 112 | yonedalem4b 16739 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤))‘𝑘)) |
114 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(Id‘𝑂) =
(Id‘𝑂) |
115 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(Id‘𝑆) =
(Id‘𝑆) |
116 | | relfunc 16345 |
. . . . . . . . . . . . . . . . . . 19
⊢ Rel
(𝑂 Func 𝑆) |
117 | | 1st2ndbr 7108 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Rel
(𝑂 Func 𝑆) ∧ ℎ ∈ (𝑂 Func 𝑆)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ)) |
118 | 116, 95, 117 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ)) |
119 | 7, 114, 115, 118, 96 | funcid 16353 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑤(2nd ‘ℎ)𝑤)‘((Id‘𝑂)‘𝑤)) = ((Id‘𝑆)‘((1st ‘ℎ)‘𝑤))) |
120 | 5, 11 | oppcid 16204 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐶 ∈ Cat →
(Id‘𝑂) = 1
) |
121 | 91, 120 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (Id‘𝑂) = 1 ) |
122 | 121 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((Id‘𝑂)‘𝑤) = ( 1 ‘𝑤)) |
123 | 122 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑤(2nd ‘ℎ)𝑤)‘((Id‘𝑂)‘𝑤)) = ((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤))) |
124 | 79 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑈 ∈ V) |
125 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Base‘𝑆) =
(Base‘𝑆) |
126 | 7, 125, 118 | funcf1 16349 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (1st ‘ℎ):𝐵⟶(Base‘𝑆)) |
127 | 12, 124 | setcbas 16551 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑈 = (Base‘𝑆)) |
128 | 127 | feq3d 5945 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((1st ‘ℎ):𝐵⟶𝑈 ↔ (1st ‘ℎ):𝐵⟶(Base‘𝑆))) |
129 | 126, 128 | mpbird 246 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (1st ‘ℎ):𝐵⟶𝑈) |
130 | 129, 96 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((1st ‘ℎ)‘𝑤) ∈ 𝑈) |
131 | 12, 115, 124, 130 | setcid 16559 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((Id‘𝑆)‘((1st ‘ℎ)‘𝑤)) = ( I ↾ ((1st
‘ℎ)‘𝑤))) |
132 | 119, 123,
131 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤)) = ( I ↾ ((1st
‘ℎ)‘𝑤))) |
133 | 132 | fveq1d 6105 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤))‘𝑘) = (( I ↾ ((1st
‘ℎ)‘𝑤))‘𝑘)) |
134 | | fvresi 6344 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ((1st
‘ℎ)‘𝑤) → (( I ↾
((1st ‘ℎ)‘𝑤))‘𝑘) = 𝑘) |
135 | 134 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (( I ↾ ((1st
‘ℎ)‘𝑤))‘𝑘) = 𝑘) |
136 | 113, 133,
135 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) = 𝑘) |
137 | 99, 109, 136 | 3eqtrd 2648 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = 𝑘) |
138 | 90, 137 | syldan 486 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ (ℎ(1st ‘𝐸)𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = 𝑘) |
139 | 138 | mpteq2dva 4672 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ 𝑘)) |
140 | | mptresid 5375 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ 𝑘) = ( I ↾ (ℎ(1st ‘𝐸)𝑤)) |
141 | 139, 140 | syl6eq 2660 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))) = ( I ↾ (ℎ(1st ‘𝐸)𝑤))) |
142 | 88, 141 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = ( I ↾ (ℎ(1st ‘𝐸)𝑤))) |
143 | | fcompt 6306 |
. . . . . . . . . . 11
⊢ (((ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)))) |
144 | 86, 35, 143 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)))) |
145 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆) |
146 | 28 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝐶 ∈ Cat) |
147 | 29 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑉 ∈ 𝑊) |
148 | 30 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ran (Homf
‘𝐶) ⊆ 𝑈) |
149 | 31 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (ran (Homf
‘𝑄) ∪ 𝑈) ⊆ 𝑉) |
150 | | simplrl 796 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ℎ ∈ (𝑂 Func 𝑆)) |
151 | | simplrr 797 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑤 ∈ 𝐵) |
152 | 83 | feq3d 5945 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤) ↔ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶((1st ‘ℎ)‘𝑤))) |
153 | 35, 152 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶((1st ‘ℎ)‘𝑤)) |
154 | 153 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) ∈ ((1st ‘ℎ)‘𝑤)) |
155 | 10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 146, 147, 148, 149, 150, 151, 42, 154 | yonedalem4c 16740 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)) |
156 | 145, 155 | nat1st2nd 16434 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (〈(1st
‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st
‘𝑌)‘𝑤))〉(𝑂 Nat 𝑆)〈(1st ‘ℎ), (2nd ‘ℎ)〉)) |
157 | 145, 156,
7 | natfn 16437 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) Fn 𝐵) |
158 | 84 | eleq2d 2673 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↔ 𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))) |
159 | 158 | biimpa 500 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)) |
160 | 145, 159 | nat1st2nd 16434 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑏 ∈ (〈(1st
‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st
‘𝑌)‘𝑤))〉(𝑂 Nat 𝑆)〈(1st ‘ℎ), (2nd ‘ℎ)〉)) |
161 | 145, 160,
7 | natfn 16437 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑏 Fn 𝐵) |
162 | 146 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝐶 ∈ Cat) |
163 | 151 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑤 ∈ 𝐵) |
164 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵) |
165 | 10, 6, 162, 163, 111, 164 | yon11 16727 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧) = (𝑧(Hom ‘𝐶)𝑤)) |
166 | 165 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧) ↔ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))) |
167 | 166 | biimpa 500 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) |
168 | 162 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝐶 ∈ Cat) |
169 | 147 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑉 ∈ 𝑊) |
170 | 148 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ran (Homf
‘𝐶) ⊆ 𝑈) |
171 | 149 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ran (Homf
‘𝑄) ∪ 𝑈) ⊆ 𝑉) |
172 | 150 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ℎ ∈ (𝑂 Func 𝑆)) |
173 | 163 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑤 ∈ 𝐵) |
174 | 154 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) ∈ ((1st ‘ℎ)‘𝑤)) |
175 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧 ∈ 𝐵) |
176 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) |
177 | 10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 168, 169, 170, 171, 172, 173, 42, 174, 175, 176 | yonedalem4b 16739 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((ℎ𝑀𝑤)‘𝑏))) |
178 | 10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 168, 169, 170, 171, 172, 173, 26 | yonedalem3a 16737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤))) |
179 | 178 | simpld 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))) |
180 | 179 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) = ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏)) |
181 | 159 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)) |
182 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 𝑏 → (𝑎‘𝑤) = (𝑏‘𝑤)) |
183 | 182 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = 𝑏 → ((𝑎‘𝑤)‘( 1 ‘𝑤)) = ((𝑏‘𝑤)‘( 1 ‘𝑤))) |
184 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏‘𝑤)‘( 1 ‘𝑤)) ∈ V |
185 | 183, 106,
184 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 ∈ (((1st
‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤))) |
186 | 181, 185 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤))) |
187 | 180, 186 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤))) |
188 | 187 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((ℎ𝑀𝑤)‘𝑏)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤)))) |
189 | 160 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (〈(1st
‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st
‘𝑌)‘𝑤))〉(𝑂 Nat 𝑆)〈(1st ‘ℎ), (2nd ‘ℎ)〉)) |
190 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Hom
‘𝑂) = (Hom
‘𝑂) |
191 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(comp‘𝑆) =
(comp‘𝑆) |
192 | 111, 5 | oppchom 16198 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑤) |
193 | 176, 192 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑘 ∈ (𝑤(Hom ‘𝑂)𝑧)) |
194 | 145, 189,
7, 190, 191, 173, 175, 193 | nati 16438 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)(〈((1st
‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘((1st
‘𝑌)‘𝑤))‘𝑧)〉(comp‘𝑆)((1st ‘ℎ)‘𝑧))((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)(〈((1st
‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘ℎ)‘𝑤)〉(comp‘𝑆)((1st ‘ℎ)‘𝑧))(𝑏‘𝑤))) |
195 | 79 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑈 ∈ V) |
196 | 195 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑈 ∈ V) |
197 | 196 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑈 ∈ V) |
198 | | relfunc 16345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ Rel
(𝐶 Func 𝑄) |
199 | 10, 17, 5, 12, 3, 79, 19 | yoncl 16725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄)) |
200 | | 1st2ndbr 7108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((Rel
(𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st ‘𝑌)(𝐶 Func 𝑄)(2nd ‘𝑌)) |
201 | 198, 199,
200 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → (1st
‘𝑌)(𝐶 Func 𝑄)(2nd ‘𝑌)) |
202 | 6, 4, 201 | funcf1 16349 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (1st
‘𝑌):𝐵⟶(𝑂 Func 𝑆)) |
203 | 202 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘𝑌):𝐵⟶(𝑂 Func 𝑆)) |
204 | 203, 151 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘𝑌)‘𝑤) ∈ (𝑂 Func 𝑆)) |
205 | | 1st2ndbr 7108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Rel
(𝑂 Func 𝑆) ∧ ((1st ‘𝑌)‘𝑤) ∈ (𝑂 Func 𝑆)) → (1st
‘((1st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st
‘𝑌)‘𝑤))) |
206 | 116, 204,
205 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st
‘((1st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st
‘𝑌)‘𝑤))) |
207 | 7, 125, 206 | funcf1 16349 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st
‘((1st ‘𝑌)‘𝑤)):𝐵⟶(Base‘𝑆)) |
208 | 12, 195 | setcbas 16551 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑈 = (Base‘𝑆)) |
209 | 208 | feq3d 5945 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st
‘((1st ‘𝑌)‘𝑤)):𝐵⟶𝑈 ↔ (1st
‘((1st ‘𝑌)‘𝑤)):𝐵⟶(Base‘𝑆))) |
210 | 207, 209 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st
‘((1st ‘𝑌)‘𝑤)):𝐵⟶𝑈) |
211 | 210, 151 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑤) ∈ 𝑈) |
212 | 211 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑤) ∈ 𝑈) |
213 | 210 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧) ∈ 𝑈) |
214 | 213 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧) ∈ 𝑈) |
215 | 116, 150,
117 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ)) |
216 | 7, 125, 215 | funcf1 16349 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘ℎ):𝐵⟶(Base‘𝑆)) |
217 | 208 | feq3d 5945 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘ℎ):𝐵⟶𝑈 ↔ (1st ‘ℎ):𝐵⟶(Base‘𝑆))) |
218 | 216, 217 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘ℎ):𝐵⟶𝑈) |
219 | 218 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1st ‘ℎ)‘𝑧) ∈ 𝑈) |
220 | 219 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘ℎ)‘𝑧) ∈ 𝑈) |
221 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Hom
‘𝑆) = (Hom
‘𝑆) |
222 | 206 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st
‘((1st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st
‘𝑌)‘𝑤))) |
223 | 7, 190, 221, 222, 173, 175 | funcf2 16351 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st
‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st
‘𝑌)‘𝑤))‘𝑧))) |
224 | 223, 193 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st
‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st
‘𝑌)‘𝑤))‘𝑧))) |
225 | 12, 197, 221, 212, 214 | elsetchom 16554 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st
‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st
‘𝑌)‘𝑤))‘𝑧)) ↔ ((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st
‘𝑌)‘𝑤))‘𝑤)⟶((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧))) |
226 | 224, 225 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st
‘𝑌)‘𝑤))‘𝑤)⟶((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧)) |
227 | 160 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑏 ∈ (〈(1st
‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st
‘𝑌)‘𝑤))〉(𝑂 Nat 𝑆)〈(1st ‘ℎ), (2nd ‘ℎ)〉)) |
228 | 145, 227,
7, 221, 164 | natcl 16436 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧) ∈ (((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧))) |
229 | 12, 196, 221, 213, 219 | elsetchom 16554 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((𝑏‘𝑧) ∈ (((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)) ↔ (𝑏‘𝑧):((1st ‘((1st
‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧))) |
230 | 228, 229 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧):((1st ‘((1st
‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧)) |
231 | 230 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏‘𝑧):((1st ‘((1st
‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧)) |
232 | 12, 197, 191, 212, 214, 220, 226, 231 | setcco 16556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)(〈((1st
‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘((1st
‘𝑌)‘𝑤))‘𝑧)〉(comp‘𝑆)((1st ‘ℎ)‘𝑧))((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘)) = ((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘))) |
233 | 218, 151 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘ℎ)‘𝑤) ∈ 𝑈) |
234 | 233 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘ℎ)‘𝑤) ∈ 𝑈) |
235 | 145, 160,
7, 221, 151 | natcl 16436 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (𝑏‘𝑤) ∈ (((1st
‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑤))) |
236 | 12, 195, 221, 211, 233 | elsetchom 16554 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((𝑏‘𝑤) ∈ (((1st
‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑤)) ↔ (𝑏‘𝑤):((1st ‘((1st
‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤))) |
237 | 235, 236 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (𝑏‘𝑤):((1st ‘((1st
‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤)) |
238 | 237 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏‘𝑤):((1st ‘((1st
‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤)) |
239 | 116, 172,
117 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ)) |
240 | 7, 190, 221, 239, 173, 175 | funcf2 16351 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd ‘ℎ)𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧))) |
241 | 240, 193 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∈ (((1st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧))) |
242 | 12, 197, 221, 234, 220 | elsetchom 16554 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∈ (((1st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)) ↔ ((𝑤(2nd ‘ℎ)𝑧)‘𝑘):((1st ‘ℎ)‘𝑤)⟶((1st ‘ℎ)‘𝑧))) |
243 | 241, 242 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘ℎ)𝑧)‘𝑘):((1st ‘ℎ)‘𝑤)⟶((1st ‘ℎ)‘𝑧)) |
244 | 12, 197, 191, 212, 234, 220, 238, 243 | setcco 16556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)(〈((1st
‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘ℎ)‘𝑤)〉(comp‘𝑆)((1st ‘ℎ)‘𝑧))(𝑏‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))) |
245 | 194, 232,
244 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))) |
246 | 245 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘))‘( 1 ‘𝑤)) = ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤))) |
247 | 6, 111, 11, 146, 151 | catidcl 16166 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ( 1 ‘𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤)) |
248 | 10, 6, 146, 151, 111, 151 | yon11 16727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑤) = (𝑤(Hom ‘𝐶)𝑤)) |
249 | 247, 248 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ( 1 ‘𝑤) ∈ ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑤)) |
250 | 249 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1 ‘𝑤) ∈ ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑤)) |
251 | | fvco3 6185 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑤(2nd
‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st
‘𝑌)‘𝑤))‘𝑤)⟶((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧) ∧ ( 1 ‘𝑤) ∈ ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑤)) → (((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘))‘( 1 ‘𝑤)) = ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤)))) |
252 | 226, 250,
251 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘))‘( 1 ‘𝑤)) = ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤)))) |
253 | | fvco3 6185 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑏‘𝑤):((1st ‘((1st
‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤) ∧ ( 1 ‘𝑤) ∈ ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑤)) → ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤)))) |
254 | 237, 249,
253 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤)))) |
255 | 254 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤)))) |
256 | 246, 252,
255 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤)))) |
257 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(comp‘𝐶) =
(comp‘𝐶) |
258 | 247 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1 ‘𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤)) |
259 | 10, 6, 168, 173, 111, 173, 257, 175, 176, 258 | yon12 16728 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤)) = (( 1 ‘𝑤)(〈𝑧, 𝑤〉(comp‘𝐶)𝑤)𝑘)) |
260 | 6, 111, 11, 168, 175, 257, 173, 176 | catlid 16167 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (( 1 ‘𝑤)(〈𝑧, 𝑤〉(comp‘𝐶)𝑤)𝑘) = 𝑘) |
261 | 259, 260 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤)) = 𝑘) |
262 | 261 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st
‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))) = ((𝑏‘𝑧)‘𝑘)) |
263 | 256, 262 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))) = ((𝑏‘𝑧)‘𝑘)) |
264 | 177, 188,
263 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏‘𝑧)‘𝑘)) |
265 | 167, 264 | syldan 486 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧)) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏‘𝑧)‘𝑘)) |
266 | 265 | mpteq2dva 4672 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)) = (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((𝑏‘𝑧)‘𝑘))) |
267 | 156 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (〈(1st
‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st
‘𝑌)‘𝑤))〉(𝑂 Nat 𝑆)〈(1st ‘ℎ), (2nd ‘ℎ)〉)) |
268 | 145, 267,
7, 221, 164 | natcl 16436 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧))) |
269 | 12, 196, 221, 213, 219 | elsetchom 16554 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)) ↔ (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st
‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧))) |
270 | 268, 269 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st
‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧)) |
271 | 270 | feqmptd 6159 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) = (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘))) |
272 | 230 | feqmptd 6159 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧) = (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((𝑏‘𝑧)‘𝑘))) |
273 | 266, 271,
272 | 3eqtr4d 2654 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) = (𝑏‘𝑧)) |
274 | 157, 161,
273 | eqfnfvd 6222 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) = 𝑏) |
275 | 274 | mpteq2dva 4672 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ 𝑏)) |
276 | | mptresid 5375 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ 𝑏) = ( I ↾ (ℎ(1st ‘𝑍)𝑤)) |
277 | 275, 276 | syl6eq 2660 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))) = ( I ↾ (ℎ(1st ‘𝑍)𝑤))) |
278 | 144, 277 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = ( I ↾ (ℎ(1st ‘𝑍)𝑤))) |
279 | | fcof1o 6451 |
. . . . . . . . 9
⊢ ((((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤)) ∧ (((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = ( I ↾ (ℎ(1st ‘𝐸)𝑤)) ∧ ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = ( I ↾ (ℎ(1st ‘𝑍)𝑤)))) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ ◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤))) |
280 | 35, 86, 142, 278, 279 | syl22anc 1319 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ ◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤))) |
281 | | eqcom 2617 |
. . . . . . . . 9
⊢ (◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤) ↔ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤)) |
282 | 281 | anbi2i 726 |
. . . . . . . 8
⊢ (((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ ◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤)) ↔ ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤))) |
283 | 280, 282 | sylib 207 |
. . . . . . 7
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤))) |
284 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑇) =
(Base‘𝑇) |
285 | | relfunc 16345 |
. . . . . . . . . . . 12
⊢ Rel
((𝑄
×c 𝑂) Func 𝑇) |
286 | | 1st2ndbr 7108 |
. . . . . . . . . . . 12
⊢ ((Rel
((𝑄
×c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st ‘𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝑍)) |
287 | 285, 22, 286 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝜑 → (1st
‘𝑍)((𝑄 ×c
𝑂) Func 𝑇)(2nd ‘𝑍)) |
288 | 8, 284, 287 | funcf1 16349 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)) |
289 | 13, 18 | setcbas 16551 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑉 = (Base‘𝑇)) |
290 | 289 | feq3d 5945 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st
‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))) |
291 | 288, 290 | mpbird 246 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉) |
292 | 291 | fovrnda 6703 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝑍)𝑤) ∈ 𝑉) |
293 | | 1st2ndbr 7108 |
. . . . . . . . . . . 12
⊢ ((Rel
((𝑄
×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st ‘𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝐸)) |
294 | 285, 23, 293 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝜑 → (1st
‘𝐸)((𝑄 ×c
𝑂) Func 𝑇)(2nd ‘𝐸)) |
295 | 8, 284, 294 | funcf1 16349 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)) |
296 | 289 | feq3d 5945 |
. . . . . . . . . 10
⊢ (𝜑 → ((1st
‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))) |
297 | 295, 296 | mpbird 246 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉) |
298 | 297 | fovrnda 6703 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝐸)𝑤) ∈ 𝑉) |
299 | 13, 29, 292, 298, 25 | setcinv 16563 |
. . . . . . 7
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤) ↔ ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤)))) |
300 | 283, 299 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤)) |
301 | 300 | ralrimivva 2954 |
. . . . 5
⊢ (𝜑 → ∀ℎ ∈ (𝑂 Func 𝑆)∀𝑤 ∈ 𝐵 (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤)) |
302 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑧 = 〈ℎ, 𝑤〉 → (𝑀‘𝑧) = (𝑀‘〈ℎ, 𝑤〉)) |
303 | | df-ov 6552 |
. . . . . . . 8
⊢ (ℎ𝑀𝑤) = (𝑀‘〈ℎ, 𝑤〉) |
304 | 302, 303 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑧 = 〈ℎ, 𝑤〉 → (𝑀‘𝑧) = (ℎ𝑀𝑤)) |
305 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = 〈ℎ, 𝑤〉 → ((1st ‘𝑍)‘𝑧) = ((1st ‘𝑍)‘〈ℎ, 𝑤〉)) |
306 | | df-ov 6552 |
. . . . . . . . 9
⊢ (ℎ(1st ‘𝑍)𝑤) = ((1st ‘𝑍)‘〈ℎ, 𝑤〉) |
307 | 305, 306 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑧 = 〈ℎ, 𝑤〉 → ((1st ‘𝑍)‘𝑧) = (ℎ(1st ‘𝑍)𝑤)) |
308 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = 〈ℎ, 𝑤〉 → ((1st ‘𝐸)‘𝑧) = ((1st ‘𝐸)‘〈ℎ, 𝑤〉)) |
309 | | df-ov 6552 |
. . . . . . . . 9
⊢ (ℎ(1st ‘𝐸)𝑤) = ((1st ‘𝐸)‘〈ℎ, 𝑤〉) |
310 | 308, 309 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑧 = 〈ℎ, 𝑤〉 → ((1st ‘𝐸)‘𝑧) = (ℎ(1st ‘𝐸)𝑤)) |
311 | 307, 310 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑧 = 〈ℎ, 𝑤〉 → (((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧)) = ((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))) |
312 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑧 = 〈ℎ, 𝑤〉 → (𝑁‘𝑧) = (𝑁‘〈ℎ, 𝑤〉)) |
313 | | df-ov 6552 |
. . . . . . . 8
⊢ (ℎ𝑁𝑤) = (𝑁‘〈ℎ, 𝑤〉) |
314 | 312, 313 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑧 = 〈ℎ, 𝑤〉 → (𝑁‘𝑧) = (ℎ𝑁𝑤)) |
315 | 304, 311,
314 | breq123d 4597 |
. . . . . 6
⊢ (𝑧 = 〈ℎ, 𝑤〉 → ((𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧) ↔ (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤))) |
316 | 315 | ralxp 5185 |
. . . . 5
⊢
(∀𝑧 ∈
((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧) ↔ ∀ℎ ∈ (𝑂 Func 𝑆)∀𝑤 ∈ 𝐵 (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤)) |
317 | 301, 316 | sylibr 223 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧)) |
318 | 317 | r19.21bi 2916 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)) → (𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧)) |
319 | 1, 8, 9, 22, 23, 24, 25, 27, 318 | invfuc 16457 |
. 2
⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)(𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧))) |
320 | | fvex 6113 |
. . . . 5
⊢
((1st ‘𝑓)‘𝑥) ∈ V |
321 | 320 | mptex 6390 |
. . . 4
⊢ (𝑢 ∈ ((1st
‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))) ∈ V |
322 | 42, 321 | fnmpt2i 7128 |
. . 3
⊢ 𝑁 Fn ((𝑂 Func 𝑆) × 𝐵) |
323 | | dffn5 6151 |
. . 3
⊢ (𝑁 Fn ((𝑂 Func 𝑆) × 𝐵) ↔ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧))) |
324 | 322, 323 | mpbi 219 |
. 2
⊢ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧)) |
325 | 319, 324 | syl6breqr 4625 |
1
⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)𝑁) |