Step | Hyp | Ref
| Expression |
1 | | chof 17490 |
. 2
class
Hom_{F} |
2 | | vc |
. . 3
setvar 𝑐 |
3 | | ccat 16927 |
. . 3
class
Cat |
4 | 2 | cv 1537 |
. . . . 5
class 𝑐 |
5 | | chomf 16929 |
. . . . 5
class
Hom_{f} |
6 | 4, 5 | cfv 6324 |
. . . 4
class
(Hom_{f} ‘𝑐) |
7 | | vb |
. . . . 5
setvar 𝑏 |
8 | | cbs 16475 |
. . . . . 6
class
Base |
9 | 4, 8 | cfv 6324 |
. . . . 5
class
(Base‘𝑐) |
10 | | vx |
. . . . . 6
setvar 𝑥 |
11 | | vy |
. . . . . 6
setvar 𝑦 |
12 | 7 | cv 1537 |
. . . . . . 7
class 𝑏 |
13 | 12, 12 | cxp 5517 |
. . . . . 6
class (𝑏 × 𝑏) |
14 | | vf |
. . . . . . 7
setvar 𝑓 |
15 | | vg |
. . . . . . 7
setvar 𝑔 |
16 | 11 | cv 1537 |
. . . . . . . . 9
class 𝑦 |
17 | | c1st 7669 |
. . . . . . . . 9
class
1^{st} |
18 | 16, 17 | cfv 6324 |
. . . . . . . 8
class
(1^{st} ‘𝑦) |
19 | 10 | cv 1537 |
. . . . . . . . 9
class 𝑥 |
20 | 19, 17 | cfv 6324 |
. . . . . . . 8
class
(1^{st} ‘𝑥) |
21 | | chom 16568 |
. . . . . . . . 9
class
Hom |
22 | 4, 21 | cfv 6324 |
. . . . . . . 8
class (Hom
‘𝑐) |
23 | 18, 20, 22 | co 7135 |
. . . . . . 7
class
((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)) |
24 | | c2nd 7670 |
. . . . . . . . 9
class
2^{nd} |
25 | 19, 24 | cfv 6324 |
. . . . . . . 8
class
(2^{nd} ‘𝑥) |
26 | 16, 24 | cfv 6324 |
. . . . . . . 8
class
(2^{nd} ‘𝑦) |
27 | 25, 26, 22 | co 7135 |
. . . . . . 7
class
((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) |
28 | | vh |
. . . . . . . 8
setvar ℎ |
29 | 19, 22 | cfv 6324 |
. . . . . . . 8
class ((Hom
‘𝑐)‘𝑥) |
30 | 15 | cv 1537 |
. . . . . . . . . 10
class 𝑔 |
31 | 28 | cv 1537 |
. . . . . . . . . 10
class ℎ |
32 | | cco 16569 |
. . . . . . . . . . . 12
class
comp |
33 | 4, 32 | cfv 6324 |
. . . . . . . . . . 11
class
(comp‘𝑐) |
34 | 19, 26, 33 | co 7135 |
. . . . . . . . . 10
class (𝑥(comp‘𝑐)(2^{nd} ‘𝑦)) |
35 | 30, 31, 34 | co 7135 |
. . . . . . . . 9
class (𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ) |
36 | 14 | cv 1537 |
. . . . . . . . 9
class 𝑓 |
37 | 18, 20 | cop 4531 |
. . . . . . . . . 10
class
⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩ |
38 | 37, 26, 33 | co 7135 |
. . . . . . . . 9
class
(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦)) |
39 | 35, 36, 38 | co 7135 |
. . . . . . . 8
class ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓) |
40 | 28, 29, 39 | cmpt 5110 |
. . . . . . 7
class (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓)) |
41 | 14, 15, 23, 27, 40 | cmpo 7137 |
. . . . . 6
class (𝑓 ∈ ((1^{st}
‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓))) |
42 | 10, 11, 13, 13, 41 | cmpo 7137 |
. . . . 5
class (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓)))) |
43 | 7, 9, 42 | csb 3828 |
. . . 4
class
⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓)))) |
44 | 6, 43 | cop 4531 |
. . 3
class
⟨(Hom_{f} ‘𝑐), ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓))))⟩ |
45 | 2, 3, 44 | cmpt 5110 |
. 2
class (𝑐 ∈ Cat ↦
⟨(Hom_{f} ‘𝑐), ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓))))⟩) |
46 | 1, 45 | wceq 1538 |
1
wff
Hom_{F} = (𝑐 ∈ Cat ↦
⟨(Hom_{f} ‘𝑐), ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓))))⟩) |