Detailed syntax breakdown of Definition df-aj
Step | Hyp | Ref
| Expression |
1 | | caj 28829 |
. 2
class
adj |
2 | | vu |
. . 3
setvar 𝑢 |
3 | | vw |
. . 3
setvar 𝑤 |
4 | | cnv 28665 |
. . 3
class
NrmCVec |
5 | 2 | cv 1542 |
. . . . . . 7
class 𝑢 |
6 | | cba 28667 |
. . . . . . 7
class
BaseSet |
7 | 5, 6 | cfv 6380 |
. . . . . 6
class
(BaseSet‘𝑢) |
8 | 3 | cv 1542 |
. . . . . . 7
class 𝑤 |
9 | 8, 6 | cfv 6380 |
. . . . . 6
class
(BaseSet‘𝑤) |
10 | | vt |
. . . . . . 7
setvar 𝑡 |
11 | 10 | cv 1542 |
. . . . . 6
class 𝑡 |
12 | 7, 9, 11 | wf 6376 |
. . . . 5
wff 𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) |
13 | | vs |
. . . . . . 7
setvar 𝑠 |
14 | 13 | cv 1542 |
. . . . . 6
class 𝑠 |
15 | 9, 7, 14 | wf 6376 |
. . . . 5
wff 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) |
16 | | vx |
. . . . . . . . . . 11
setvar 𝑥 |
17 | 16 | cv 1542 |
. . . . . . . . . 10
class 𝑥 |
18 | 17, 11 | cfv 6380 |
. . . . . . . . 9
class (𝑡‘𝑥) |
19 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
20 | 19 | cv 1542 |
. . . . . . . . 9
class 𝑦 |
21 | | cdip 28781 |
. . . . . . . . . 10
class
·𝑖OLD |
22 | 8, 21 | cfv 6380 |
. . . . . . . . 9
class
(·𝑖OLD‘𝑤) |
23 | 18, 20, 22 | co 7213 |
. . . . . . . 8
class ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) |
24 | 20, 14 | cfv 6380 |
. . . . . . . . 9
class (𝑠‘𝑦) |
25 | 5, 21 | cfv 6380 |
. . . . . . . . 9
class
(·𝑖OLD‘𝑢) |
26 | 17, 24, 25 | co 7213 |
. . . . . . . 8
class (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)) |
27 | 23, 26 | wceq 1543 |
. . . . . . 7
wff ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)) |
28 | 27, 19, 9 | wral 3061 |
. . . . . 6
wff
∀𝑦 ∈
(BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)) |
29 | 28, 16, 7 | wral 3061 |
. . . . 5
wff
∀𝑥 ∈
(BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)) |
30 | 12, 15, 29 | w3a 1089 |
. . . 4
wff (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))) |
31 | 30, 10, 13 | copab 5115 |
. . 3
class
{〈𝑡, 𝑠〉 ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))} |
32 | 2, 3, 4, 4, 31 | cmpo 7215 |
. 2
class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦
{〈𝑡, 𝑠〉 ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))}) |
33 | 1, 32 | wceq 1543 |
1
wff adj =
(𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦
{〈𝑡, 𝑠〉 ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))}) |