Step | Hyp | Ref
| Expression |
1 | | yoneda.y |
. . . . 5
⊢ 𝑌 = (Yon‘𝐶) |
2 | | yoneda.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐶) |
3 | | yoneda.1 |
. . . . 5
⊢ 1 =
(Id‘𝐶) |
4 | | yoneda.o |
. . . . 5
⊢ 𝑂 = (oppCat‘𝐶) |
5 | | yoneda.s |
. . . . 5
⊢ 𝑆 = (SetCat‘𝑈) |
6 | | yoneda.t |
. . . . 5
⊢ 𝑇 = (SetCat‘𝑉) |
7 | | yoneda.q |
. . . . 5
⊢ 𝑄 = (𝑂 FuncCat 𝑆) |
8 | | yoneda.h |
. . . . 5
⊢ 𝐻 =
(HomF‘𝑄) |
9 | | yoneda.r |
. . . . 5
⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇) |
10 | | yoneda.e |
. . . . 5
⊢ 𝐸 = (𝑂 evalF 𝑆) |
11 | | yoneda.z |
. . . . 5
⊢ 𝑍 = (𝐻 ∘func
((〈(1st ‘𝑌), tpos (2nd ‘𝑌)〉
∘func (𝑄 2ndF 𝑂))
〈,〉F (𝑄 1stF 𝑂))) |
12 | | yoneda.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ Cat) |
13 | | yoneda.w |
. . . . 5
⊢ (𝜑 → 𝑉 ∈ 𝑊) |
14 | | yoneda.u |
. . . . 5
⊢ (𝜑 → ran
(Homf ‘𝐶) ⊆ 𝑈) |
15 | | yoneda.v |
. . . . 5
⊢ (𝜑 → (ran
(Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉) |
16 | | yonedalem21.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆)) |
17 | | yonedalem21.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
18 | | yonedalem4.n |
. . . . 5
⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢))))) |
19 | | yonedalem4.p |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ((1st ‘𝐹)‘𝑋)) |
20 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18, 19 | yonedalem4a 16915 |
. . . 4
⊢ (𝜑 → ((𝐹𝑁𝑋)‘𝐴) = (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑦)‘𝑔)‘𝐴)))) |
21 | | oveq1 6657 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (𝑦(Hom ‘𝐶)𝑋) = (𝑧(Hom ‘𝐶)𝑋)) |
22 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝑋(2nd ‘𝐹)𝑦) = (𝑋(2nd ‘𝐹)𝑧)) |
23 | 22 | fveq1d 6193 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ((𝑋(2nd ‘𝐹)𝑦)‘𝑔) = ((𝑋(2nd ‘𝐹)𝑧)‘𝑔)) |
24 | 23 | fveq1d 6193 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (((𝑋(2nd ‘𝐹)𝑦)‘𝑔)‘𝐴) = (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) |
25 | 21, 24 | mpteq12dv 4733 |
. . . . 5
⊢ (𝑦 = 𝑧 → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑦)‘𝑔)‘𝐴)) = (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) |
26 | 25 | cbvmptv 4750 |
. . . 4
⊢ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑦)‘𝑔)‘𝐴))) = (𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) |
27 | 20, 26 | syl6eq 2672 |
. . 3
⊢ (𝜑 → ((𝐹𝑁𝑋)‘𝐴) = (𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)))) |
28 | 4, 2 | oppcbas 16378 |
. . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑂) |
29 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (Hom
‘𝑂) = (Hom
‘𝑂) |
30 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (Hom
‘𝑆) = (Hom
‘𝑆) |
31 | | relfunc 16522 |
. . . . . . . . . . . . . . 15
⊢ Rel
(𝑂 Func 𝑆) |
32 | | 1st2ndbr 7217 |
. . . . . . . . . . . . . . 15
⊢ ((Rel
(𝑂 Func 𝑆) ∧ 𝐹 ∈ (𝑂 Func 𝑆)) → (1st ‘𝐹)(𝑂 Func 𝑆)(2nd ‘𝐹)) |
33 | 31, 16, 32 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1st
‘𝐹)(𝑂 Func 𝑆)(2nd ‘𝐹)) |
34 | 33 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (1st ‘𝐹)(𝑂 Func 𝑆)(2nd ‘𝐹)) |
35 | 17 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
36 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵) |
37 | 28, 29, 30, 34, 35, 36 | funcf2 16528 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑋(2nd ‘𝐹)𝑧):(𝑋(Hom ‘𝑂)𝑧)⟶(((1st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) |
38 | 37 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (𝑋(2nd ‘𝐹)𝑧):(𝑋(Hom ‘𝑂)𝑧)⟶(((1st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) |
39 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) |
40 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
41 | 40, 4 | oppchom 16375 |
. . . . . . . . . . . 12
⊢ (𝑋(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑋) |
42 | 39, 41 | syl6eleqr 2712 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑔 ∈ (𝑋(Hom ‘𝑂)𝑧)) |
43 | 38, 42 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd ‘𝐹)𝑧)‘𝑔) ∈ (((1st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) |
44 | 15 | unssbd 3791 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ⊆ 𝑉) |
45 | 13, 44 | ssexd 4805 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ V) |
46 | 45 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑈 ∈ V) |
47 | 46 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑈 ∈ V) |
48 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑆) =
(Base‘𝑆) |
49 | 28, 48, 33 | funcf1 16526 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1st
‘𝐹):𝐵⟶(Base‘𝑆)) |
50 | 5, 45 | setcbas 16728 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 = (Base‘𝑆)) |
51 | 50 | feq3d 6032 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((1st
‘𝐹):𝐵⟶𝑈 ↔ (1st ‘𝐹):𝐵⟶(Base‘𝑆))) |
52 | 49, 51 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1st
‘𝐹):𝐵⟶𝑈) |
53 | 52, 17 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1st
‘𝐹)‘𝑋) ∈ 𝑈) |
54 | 53 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((1st ‘𝐹)‘𝑋) ∈ 𝑈) |
55 | 52 | ffvelrnda 6359 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘𝐹)‘𝑧) ∈ 𝑈) |
56 | 55 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((1st ‘𝐹)‘𝑧) ∈ 𝑈) |
57 | 5, 47, 30, 54, 56 | elsetchom 16731 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑋(2nd ‘𝐹)𝑧)‘𝑔) ∈ (((1st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧)) ↔ ((𝑋(2nd ‘𝐹)𝑧)‘𝑔):((1st ‘𝐹)‘𝑋)⟶((1st ‘𝐹)‘𝑧))) |
58 | 43, 57 | mpbid 222 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd ‘𝐹)𝑧)‘𝑔):((1st ‘𝐹)‘𝑋)⟶((1st ‘𝐹)‘𝑧)) |
59 | 19 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝐴 ∈ ((1st ‘𝐹)‘𝑋)) |
60 | 58, 59 | ffvelrnd 6360 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴) ∈ ((1st ‘𝐹)‘𝑧)) |
61 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) = (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) |
62 | 60, 61 | fmptd 6385 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)):(𝑧(Hom ‘𝐶)𝑋)⟶((1st ‘𝐹)‘𝑧)) |
63 | 12 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐶 ∈ Cat) |
64 | 1, 2, 63, 35, 40, 36 | yon11 16904 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) = (𝑧(Hom ‘𝐶)𝑋)) |
65 | 64 | feq2d 6031 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧) ↔ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)):(𝑧(Hom ‘𝐶)𝑋)⟶((1st ‘𝐹)‘𝑧))) |
66 | 62, 65 | mpbird 247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧)) |
67 | 1, 2, 12, 17, 4, 5, 45, 14 | yon1cl 16903 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1st
‘𝑌)‘𝑋) ∈ (𝑂 Func 𝑆)) |
68 | | 1st2ndbr 7217 |
. . . . . . . . . . 11
⊢ ((Rel
(𝑂 Func 𝑆) ∧ ((1st ‘𝑌)‘𝑋) ∈ (𝑂 Func 𝑆)) → (1st
‘((1st ‘𝑌)‘𝑋))(𝑂 Func 𝑆)(2nd ‘((1st
‘𝑌)‘𝑋))) |
69 | 31, 67, 68 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘((1st ‘𝑌)‘𝑋))(𝑂 Func 𝑆)(2nd ‘((1st
‘𝑌)‘𝑋))) |
70 | 28, 48, 69 | funcf1 16526 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘((1st ‘𝑌)‘𝑋)):𝐵⟶(Base‘𝑆)) |
71 | 50 | feq3d 6032 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘((1st ‘𝑌)‘𝑋)):𝐵⟶𝑈 ↔ (1st
‘((1st ‘𝑌)‘𝑋)):𝐵⟶(Base‘𝑆))) |
72 | 70, 71 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘((1st ‘𝑌)‘𝑋)):𝐵⟶𝑈) |
73 | 72 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ∈ 𝑈) |
74 | 5, 46, 30, 73, 55 | elsetchom 16731 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) ∈ (((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧)) ↔ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧))) |
75 | 66, 74 | mpbird 247 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) ∈ (((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) |
76 | 75 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) ∈ (((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) |
77 | | fvex 6201 |
. . . . . 6
⊢
(Base‘𝐶)
∈ V |
78 | 2, 77 | eqeltri 2697 |
. . . . 5
⊢ 𝐵 ∈ V |
79 | | mptelixpg 7945 |
. . . . 5
⊢ (𝐵 ∈ V → ((𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) ∈ (((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧)))) |
80 | 78, 79 | ax-mp 5 |
. . . 4
⊢ ((𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) ∈ (((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) |
81 | 76, 80 | sylibr 224 |
. . 3
⊢ (𝜑 → (𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) |
82 | 27, 81 | eqeltrd 2701 |
. 2
⊢ (𝜑 → ((𝐹𝑁𝑋)‘𝐴) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) |
83 | 12 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → 𝐶 ∈ Cat) |
84 | 17 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → 𝑋 ∈ 𝐵) |
85 | | simpr1 1067 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → 𝑧 ∈ 𝐵) |
86 | 1, 2, 83, 84, 40, 85 | yon11 16904 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) = (𝑧(Hom ‘𝐶)𝑋)) |
87 | 86 | eleq2d 2687 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ↔ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋))) |
88 | 87 | biimpa 501 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) |
89 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(comp‘𝑂) =
(comp‘𝑂) |
90 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(comp‘𝑆) =
(comp‘𝑆) |
91 | 33 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (1st ‘𝐹)(𝑂 Func 𝑆)(2nd ‘𝐹)) |
92 | 91 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (1st ‘𝐹)(𝑂 Func 𝑆)(2nd ‘𝐹)) |
93 | 84 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑋 ∈ 𝐵) |
94 | 85 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑧 ∈ 𝐵) |
95 | | simpr2 1068 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → 𝑤 ∈ 𝐵) |
96 | 95 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑤 ∈ 𝐵) |
97 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) |
98 | 97, 41 | syl6eleqr 2712 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑘 ∈ (𝑋(Hom ‘𝑂)𝑧)) |
99 | | simplr3 1105 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)) |
100 | 28, 29, 89, 90, 92, 93, 94, 96, 98, 99 | funcco 16531 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd ‘𝐹)𝑤)‘(ℎ(〈𝑋, 𝑧〉(comp‘𝑂)𝑤)𝑘)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑧)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))((𝑋(2nd ‘𝐹)𝑧)‘𝑘))) |
101 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(comp‘𝐶) =
(comp‘𝐶) |
102 | 2, 101, 4, 93, 94, 96 | oppcco 16377 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (ℎ(〈𝑋, 𝑧〉(comp‘𝑂)𝑤)𝑘) = (𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ)) |
103 | 102 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd ‘𝐹)𝑤)‘(ℎ(〈𝑋, 𝑧〉(comp‘𝑂)𝑤)𝑘)) = ((𝑋(2nd ‘𝐹)𝑤)‘(𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ))) |
104 | 45 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → 𝑈 ∈ V) |
105 | 104 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑈 ∈ V) |
106 | 53 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((1st ‘𝐹)‘𝑋) ∈ 𝑈) |
107 | 55 | 3ad2antr1 1226 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((1st ‘𝐹)‘𝑧) ∈ 𝑈) |
108 | 107 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((1st ‘𝐹)‘𝑧) ∈ 𝑈) |
109 | 52 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (1st ‘𝐹):𝐵⟶𝑈) |
110 | 109, 95 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((1st ‘𝐹)‘𝑤) ∈ 𝑈) |
111 | 110 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((1st ‘𝐹)‘𝑤) ∈ 𝑈) |
112 | 28, 29, 30, 91, 84, 85 | funcf2 16528 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (𝑋(2nd ‘𝐹)𝑧):(𝑋(Hom ‘𝑂)𝑧)⟶(((1st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) |
113 | 112 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (𝑋(2nd ‘𝐹)𝑧):(𝑋(Hom ‘𝑂)𝑧)⟶(((1st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) |
114 | 113, 98 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd ‘𝐹)𝑧)‘𝑘) ∈ (((1st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) |
115 | 5, 105, 30, 106, 108 | elsetchom 16731 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑋(2nd ‘𝐹)𝑧)‘𝑘) ∈ (((1st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧)) ↔ ((𝑋(2nd ‘𝐹)𝑧)‘𝑘):((1st ‘𝐹)‘𝑋)⟶((1st ‘𝐹)‘𝑧))) |
116 | 114, 115 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd ‘𝐹)𝑧)‘𝑘):((1st ‘𝐹)‘𝑋)⟶((1st ‘𝐹)‘𝑧)) |
117 | 28, 29, 30, 91, 85, 95 | funcf2 16528 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (𝑧(2nd ‘𝐹)𝑤):(𝑧(Hom ‘𝑂)𝑤)⟶(((1st ‘𝐹)‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑤))) |
118 | | simpr3 1069 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)) |
119 | 117, 118 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∈ (((1st ‘𝐹)‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑤))) |
120 | 5, 104, 30, 107, 110 | elsetchom 16731 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∈ (((1st ‘𝐹)‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑤)) ↔ ((𝑧(2nd ‘𝐹)𝑤)‘ℎ):((1st ‘𝐹)‘𝑧)⟶((1st ‘𝐹)‘𝑤))) |
121 | 119, 120 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((𝑧(2nd ‘𝐹)𝑤)‘ℎ):((1st ‘𝐹)‘𝑧)⟶((1st ‘𝐹)‘𝑤)) |
122 | 121 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑧(2nd ‘𝐹)𝑤)‘ℎ):((1st ‘𝐹)‘𝑧)⟶((1st ‘𝐹)‘𝑤)) |
123 | 5, 105, 90, 106, 108, 111, 116, 122 | setcco 16733 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑧)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))((𝑋(2nd ‘𝐹)𝑧)‘𝑘)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ ((𝑋(2nd ‘𝐹)𝑧)‘𝑘))) |
124 | 100, 103,
123 | 3eqtr3d 2664 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd ‘𝐹)𝑤)‘(𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ ((𝑋(2nd ‘𝐹)𝑧)‘𝑘))) |
125 | 124 | fveq1d 6193 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑋(2nd ‘𝐹)𝑤)‘(𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ))‘𝐴) = ((((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ ((𝑋(2nd ‘𝐹)𝑧)‘𝑘))‘𝐴)) |
126 | 19 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝐴 ∈ ((1st ‘𝐹)‘𝑋)) |
127 | | fvco3 6275 |
. . . . . . . . . 10
⊢ ((((𝑋(2nd ‘𝐹)𝑧)‘𝑘):((1st ‘𝐹)‘𝑋)⟶((1st ‘𝐹)‘𝑧) ∧ 𝐴 ∈ ((1st ‘𝐹)‘𝑋)) → ((((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ ((𝑋(2nd ‘𝐹)𝑧)‘𝑘))‘𝐴) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘(((𝑋(2nd ‘𝐹)𝑧)‘𝑘)‘𝐴))) |
128 | 116, 126,
127 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ ((𝑋(2nd ‘𝐹)𝑧)‘𝑘))‘𝐴) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘(((𝑋(2nd ‘𝐹)𝑧)‘𝑘)‘𝐴))) |
129 | 125, 128 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑋(2nd ‘𝐹)𝑤)‘(𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ))‘𝐴) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘(((𝑋(2nd ‘𝐹)𝑧)‘𝑘)‘𝐴))) |
130 | 83 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝐶 ∈ Cat) |
131 | 40, 4 | oppchom 16375 |
. . . . . . . . . . . 12
⊢ (𝑧(Hom ‘𝑂)𝑤) = (𝑤(Hom ‘𝐶)𝑧) |
132 | 99, 131 | syl6eleq 2711 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ℎ ∈ (𝑤(Hom ‘𝐶)𝑧)) |
133 | 1, 2, 130, 93, 40, 94, 101, 96, 132, 97 | yon12 16905 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)‘𝑘) = (𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ)) |
134 | 133 | fveq2d 6195 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)‘𝑘)) = ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ))) |
135 | 13 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑉 ∈ 𝑊) |
136 | 14 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ran (Homf
‘𝐶) ⊆ 𝑈) |
137 | 15 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (ran (Homf
‘𝑄) ∪ 𝑈) ⊆ 𝑉) |
138 | 16 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝐹 ∈ (𝑂 Func 𝑆)) |
139 | 2, 40, 101, 130, 96, 94, 93, 132, 97 | catcocl 16346 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ) ∈ (𝑤(Hom ‘𝐶)𝑋)) |
140 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 130, 135, 136, 137, 138, 93, 18, 126, 96, 139 | yonedalem4b 16916 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ)) = (((𝑋(2nd ‘𝐹)𝑤)‘(𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ))‘𝐴)) |
141 | 134, 140 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)‘𝑘)) = (((𝑋(2nd ‘𝐹)𝑤)‘(𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ))‘𝐴)) |
142 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 130, 135, 136, 137, 138, 93, 18, 126, 94, 97 | yonedalem4b 16916 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘) = (((𝑋(2nd ‘𝐹)𝑧)‘𝑘)‘𝐴)) |
143 | 142 | fveq2d 6195 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘(((𝑋(2nd ‘𝐹)𝑧)‘𝑘)‘𝐴))) |
144 | 129, 141,
143 | 3eqtr4d 2666 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)‘𝑘)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘))) |
145 | 88, 144 | syldan 487 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)‘𝑘)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘))) |
146 | 145 | mpteq2dva 4744 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ↦ ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)‘𝑘))) = (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ↦ (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘)))) |
147 | 27 | fveq1d 6193 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐹𝑁𝑋)‘𝐴)‘𝑧) = ((𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)))‘𝑧)) |
148 | | ovex 6678 |
. . . . . . . . . . . . . 14
⊢ (𝑧(Hom ‘𝐶)𝑋) ∈ V |
149 | 148 | mptex 6486 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) ∈ V |
150 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) = (𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) |
151 | 150 | fvmpt2 6291 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐵 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) ∈ V) → ((𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)))‘𝑧) = (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) |
152 | 149, 151 | mpan2 707 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝐵 → ((𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)))‘𝑧) = (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) |
153 | 147, 152 | sylan9eq 2676 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (((𝐹𝑁𝑋)‘𝐴)‘𝑧) = (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) |
154 | 153 | feq1d 6030 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧) ↔ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧))) |
155 | 66, 154 | mpbird 247 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧)) |
156 | 155 | ralrimiva 2966 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 (((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧)) |
157 | 156 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ∀𝑧 ∈ 𝐵 (((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧)) |
158 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → (((𝐹𝑁𝑋)‘𝐴)‘𝑧) = (((𝐹𝑁𝑋)‘𝐴)‘𝑤)) |
159 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) = ((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)) |
160 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → ((1st ‘𝐹)‘𝑧) = ((1st ‘𝐹)‘𝑤)) |
161 | 158, 159,
160 | feq123d 6034 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → ((((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧) ↔ (((𝐹𝑁𝑋)‘𝐴)‘𝑤):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)⟶((1st ‘𝐹)‘𝑤))) |
162 | 161 | rspcv 3305 |
. . . . . . 7
⊢ (𝑤 ∈ 𝐵 → (∀𝑧 ∈ 𝐵 (((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧) → (((𝐹𝑁𝑋)‘𝐴)‘𝑤):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)⟶((1st ‘𝐹)‘𝑤))) |
163 | 95, 157, 162 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝐹𝑁𝑋)‘𝐴)‘𝑤):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)⟶((1st ‘𝐹)‘𝑤)) |
164 | 69 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (1st
‘((1st ‘𝑌)‘𝑋))(𝑂 Func 𝑆)(2nd ‘((1st
‘𝑌)‘𝑋))) |
165 | 28, 29, 30, 164, 85, 95 | funcf2 16528 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤):(𝑧(Hom ‘𝑂)𝑤)⟶(((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤))) |
166 | 165, 118 | ffvelrnd 6360 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ) ∈ (((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤))) |
167 | 73 | 3ad2antr1 1226 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ∈ 𝑈) |
168 | 72 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (1st
‘((1st ‘𝑌)‘𝑋)):𝐵⟶𝑈) |
169 | 168, 95 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑤) ∈ 𝑈) |
170 | 5, 104, 30, 167, 169 | elsetchom 16731 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ) ∈ (((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)) ↔ ((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st
‘((1st ‘𝑌)‘𝑋))‘𝑤))) |
171 | 166, 170 | mpbid 222 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st
‘((1st ‘𝑌)‘𝑋))‘𝑤)) |
172 | | fcompt 6400 |
. . . . . 6
⊢
(((((𝐹𝑁𝑋)‘𝐴)‘𝑤):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)⟶((1st ‘𝐹)‘𝑤) ∧ ((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st
‘((1st ‘𝑌)‘𝑋))‘𝑤)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤) ∘ ((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)) = (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ↦ ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)‘𝑘)))) |
173 | 163, 171,
172 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤) ∘ ((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)) = (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ↦ ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)‘𝑘)))) |
174 | 155 | 3ad2antr1 1226 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧)) |
175 | | fcompt 6400 |
. . . . . 6
⊢ ((((𝑧(2nd ‘𝐹)𝑤)‘ℎ):((1st ‘𝐹)‘𝑧)⟶((1st ‘𝐹)‘𝑤) ∧ (((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧)) → (((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ (((𝐹𝑁𝑋)‘𝐴)‘𝑧)) = (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ↦ (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘)))) |
176 | 121, 174,
175 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ (((𝐹𝑁𝑋)‘𝐴)‘𝑧)) = (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ↦ (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘)))) |
177 | 146, 173,
176 | 3eqtr4d 2666 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤) ∘ ((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ (((𝐹𝑁𝑋)‘𝐴)‘𝑧))) |
178 | 5, 104, 90, 167, 169, 110, 171, 163 | setcco 16733 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)(〈((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧), ((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)) = ((((𝐹𝑁𝑋)‘𝐴)‘𝑤) ∘ ((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ))) |
179 | 5, 104, 90, 167, 107, 110, 174, 121 | setcco 16733 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)(〈((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧), ((1st ‘𝐹)‘𝑧)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))(((𝐹𝑁𝑋)‘𝐴)‘𝑧)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ (((𝐹𝑁𝑋)‘𝐴)‘𝑧))) |
180 | 177, 178,
179 | 3eqtr4d 2666 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)(〈((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧), ((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)(〈((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧), ((1st ‘𝐹)‘𝑧)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))(((𝐹𝑁𝑋)‘𝐴)‘𝑧))) |
181 | 180 | ralrimivvva 2972 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ∀ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)((((𝐹𝑁𝑋)‘𝐴)‘𝑤)(〈((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧), ((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)(〈((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧), ((1st ‘𝐹)‘𝑧)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))(((𝐹𝑁𝑋)‘𝐴)‘𝑧))) |
182 | | eqid 2622 |
. . 3
⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆) |
183 | 182, 28, 29, 30, 90, 67, 16 | isnat2 16608 |
. 2
⊢ (𝜑 → (((𝐹𝑁𝑋)‘𝐴) ∈ (((1st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↔ (((𝐹𝑁𝑋)‘𝐴) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧)) ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ∀ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)((((𝐹𝑁𝑋)‘𝐴)‘𝑤)(〈((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧), ((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)(〈((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧), ((1st ‘𝐹)‘𝑧)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))(((𝐹𝑁𝑋)‘𝐴)‘𝑧))))) |
184 | 82, 181, 183 | mpbir2and 957 |
1
⊢ (𝜑 → ((𝐹𝑁𝑋)‘𝐴) ∈ (((1st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) |