Detailed syntax breakdown of Definition df-aj
| Step | Hyp | Ref
| Expression |
| 1 | | caj 30767 |
. 2
class
adj |
| 2 | | vu |
. . 3
setvar 𝑢 |
| 3 | | vw |
. . 3
setvar 𝑤 |
| 4 | | cnv 30603 |
. . 3
class
NrmCVec |
| 5 | 2 | cv 1539 |
. . . . . . 7
class 𝑢 |
| 6 | | cba 30605 |
. . . . . . 7
class
BaseSet |
| 7 | 5, 6 | cfv 6561 |
. . . . . 6
class
(BaseSet‘𝑢) |
| 8 | 3 | cv 1539 |
. . . . . . 7
class 𝑤 |
| 9 | 8, 6 | cfv 6561 |
. . . . . 6
class
(BaseSet‘𝑤) |
| 10 | | vt |
. . . . . . 7
setvar 𝑡 |
| 11 | 10 | cv 1539 |
. . . . . 6
class 𝑡 |
| 12 | 7, 9, 11 | wf 6557 |
. . . . 5
wff 𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) |
| 13 | | vs |
. . . . . . 7
setvar 𝑠 |
| 14 | 13 | cv 1539 |
. . . . . 6
class 𝑠 |
| 15 | 9, 7, 14 | wf 6557 |
. . . . 5
wff 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) |
| 16 | | vx |
. . . . . . . . . . 11
setvar 𝑥 |
| 17 | 16 | cv 1539 |
. . . . . . . . . 10
class 𝑥 |
| 18 | 17, 11 | cfv 6561 |
. . . . . . . . 9
class (𝑡‘𝑥) |
| 19 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
| 20 | 19 | cv 1539 |
. . . . . . . . 9
class 𝑦 |
| 21 | | cdip 30719 |
. . . . . . . . . 10
class
·𝑖OLD |
| 22 | 8, 21 | cfv 6561 |
. . . . . . . . 9
class
(·𝑖OLD‘𝑤) |
| 23 | 18, 20, 22 | co 7431 |
. . . . . . . 8
class ((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) |
| 24 | 20, 14 | cfv 6561 |
. . . . . . . . 9
class (𝑠‘𝑦) |
| 25 | 5, 21 | cfv 6561 |
. . . . . . . . 9
class
(·𝑖OLD‘𝑢) |
| 26 | 17, 24, 25 | co 7431 |
. . . . . . . 8
class (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)) |
| 27 | 23, 26 | wceq 1540 |
. . . . . . 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 1087 |
. . . 4
wff (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦))) |
| 31 | 30, 10, 13 | copab 5205 |
. . 3
class
{〈𝑡, 𝑠〉 ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))} |
| 32 | 2, 3, 4, 4, 31 | cmpo 7433 |
. 2
class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦
{〈𝑡, 𝑠〉 ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))}) |
| 33 | 1, 32 | wceq 1540 |
1
wff adj =
(𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦
{〈𝑡, 𝑠〉 ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))}) |