Detailed syntax breakdown of Definition df-estrc
Step | Hyp | Ref
| Expression |
1 | | cestrc 17834 |
. 2
class
ExtStrCat |
2 | | vu |
. . 3
setvar 𝑢 |
3 | | cvv 3431 |
. . 3
class
V |
4 | | cnx 16890 |
. . . . . 6
class
ndx |
5 | | cbs 16908 |
. . . . . 6
class
Base |
6 | 4, 5 | cfv 6431 |
. . . . 5
class
(Base‘ndx) |
7 | 2 | cv 1541 |
. . . . 5
class 𝑢 |
8 | 6, 7 | cop 4573 |
. . . 4
class
〈(Base‘ndx), 𝑢〉 |
9 | | chom 16969 |
. . . . . 6
class
Hom |
10 | 4, 9 | cfv 6431 |
. . . . 5
class (Hom
‘ndx) |
11 | | vx |
. . . . . 6
setvar 𝑥 |
12 | | vy |
. . . . . 6
setvar 𝑦 |
13 | 12 | cv 1541 |
. . . . . . . 8
class 𝑦 |
14 | 13, 5 | cfv 6431 |
. . . . . . 7
class
(Base‘𝑦) |
15 | 11 | cv 1541 |
. . . . . . . 8
class 𝑥 |
16 | 15, 5 | cfv 6431 |
. . . . . . 7
class
(Base‘𝑥) |
17 | | cmap 8596 |
. . . . . . 7
class
↑m |
18 | 14, 16, 17 | co 7269 |
. . . . . 6
class
((Base‘𝑦)
↑m (Base‘𝑥)) |
19 | 11, 12, 7, 7, 18 | cmpo 7271 |
. . . . 5
class (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))) |
20 | 10, 19 | cop 4573 |
. . . 4
class
〈(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))〉 |
21 | | cco 16970 |
. . . . . 6
class
comp |
22 | 4, 21 | cfv 6431 |
. . . . 5
class
(comp‘ndx) |
23 | | vv |
. . . . . 6
setvar 𝑣 |
24 | | vz |
. . . . . 6
setvar 𝑧 |
25 | 7, 7 | cxp 5587 |
. . . . . 6
class (𝑢 × 𝑢) |
26 | | vg |
. . . . . . 7
setvar 𝑔 |
27 | | vf |
. . . . . . 7
setvar 𝑓 |
28 | 24 | cv 1541 |
. . . . . . . . 9
class 𝑧 |
29 | 28, 5 | cfv 6431 |
. . . . . . . 8
class
(Base‘𝑧) |
30 | 23 | cv 1541 |
. . . . . . . . . 10
class 𝑣 |
31 | | c2nd 7821 |
. . . . . . . . . 10
class
2nd |
32 | 30, 31 | cfv 6431 |
. . . . . . . . 9
class
(2nd ‘𝑣) |
33 | 32, 5 | cfv 6431 |
. . . . . . . 8
class
(Base‘(2nd ‘𝑣)) |
34 | 29, 33, 17 | co 7269 |
. . . . . . 7
class
((Base‘𝑧)
↑m (Base‘(2nd ‘𝑣))) |
35 | | c1st 7820 |
. . . . . . . . . 10
class
1st |
36 | 30, 35 | cfv 6431 |
. . . . . . . . 9
class
(1st ‘𝑣) |
37 | 36, 5 | cfv 6431 |
. . . . . . . 8
class
(Base‘(1st ‘𝑣)) |
38 | 33, 37, 17 | co 7269 |
. . . . . . 7
class
((Base‘(2nd ‘𝑣)) ↑m
(Base‘(1st ‘𝑣))) |
39 | 26 | cv 1541 |
. . . . . . . 8
class 𝑔 |
40 | 27 | cv 1541 |
. . . . . . . 8
class 𝑓 |
41 | 39, 40 | ccom 5593 |
. . . . . . 7
class (𝑔 ∘ 𝑓) |
42 | 26, 27, 34, 38, 41 | cmpo 7271 |
. . . . . 6
class (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)) |
43 | 23, 24, 25, 7, 42 | cmpo 7271 |
. . . . 5
class (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓))) |
44 | 22, 43 | cop 4573 |
. . . 4
class
〈(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))〉 |
45 | 8, 20, 44 | ctp 4571 |
. . 3
class
{〈(Base‘ndx), 𝑢〉, 〈(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))〉,
〈(comp‘ndx), (𝑣
∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))〉} |
46 | 2, 3, 45 | cmpt 5162 |
. 2
class (𝑢 ∈ V ↦
{〈(Base‘ndx), 𝑢〉, 〈(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))〉,
〈(comp‘ndx), (𝑣
∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))〉}) |
47 | 1, 46 | wceq 1542 |
1
wff ExtStrCat =
(𝑢 ∈ V ↦
{〈(Base‘ndx), 𝑢〉, 〈(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))〉,
〈(comp‘ndx), (𝑣
∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m
(Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd
‘𝑣))
↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))〉}) |