Detailed syntax breakdown of Definition df-msa
Step | Hyp | Ref
| Expression |
1 | | cmsa 33284 |
. 2
class
mSA |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | cvv 3420 |
. . 3
class
V |
4 | | va |
. . . . . . . 8
setvar 𝑎 |
5 | 4 | cv 1542 |
. . . . . . 7
class 𝑎 |
6 | | cm0s 33283 |
. . . . . . 7
class
m0St |
7 | 5, 6 | cfv 6397 |
. . . . . 6
class
(m0St‘𝑎) |
8 | 2 | cv 1542 |
. . . . . . 7
class 𝑡 |
9 | | cmax 33163 |
. . . . . . 7
class
mAx |
10 | 8, 9 | cfv 6397 |
. . . . . 6
class
(mAx‘𝑡) |
11 | 7, 10 | wcel 2111 |
. . . . 5
wff
(m0St‘𝑎)
∈ (mAx‘𝑡) |
12 | | c1st 7777 |
. . . . . . 7
class
1st |
13 | 5, 12 | cfv 6397 |
. . . . . 6
class
(1st ‘𝑎) |
14 | | cmvt 33161 |
. . . . . . 7
class
mVT |
15 | 8, 14 | cfv 6397 |
. . . . . 6
class
(mVT‘𝑡) |
16 | 13, 15 | wcel 2111 |
. . . . 5
wff
(1st ‘𝑎) ∈ (mVT‘𝑡) |
17 | | c2nd 7778 |
. . . . . . . . 9
class
2nd |
18 | 5, 17 | cfv 6397 |
. . . . . . . 8
class
(2nd ‘𝑎) |
19 | 18 | ccnv 5564 |
. . . . . . 7
class ◡(2nd ‘𝑎) |
20 | | cmvar 33159 |
. . . . . . . 8
class
mVR |
21 | 8, 20 | cfv 6397 |
. . . . . . 7
class
(mVR‘𝑡) |
22 | 19, 21 | cres 5567 |
. . . . . 6
class (◡(2nd ‘𝑎) ↾ (mVR‘𝑡)) |
23 | 22 | wfun 6391 |
. . . . 5
wff Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡)) |
24 | 11, 16, 23 | w3a 1089 |
. . . 4
wff
((m0St‘𝑎)
∈ (mAx‘𝑡) ∧
(1st ‘𝑎)
∈ (mVT‘𝑡) ∧
Fun (◡(2nd ‘𝑎) ↾ (mVR‘𝑡))) |
25 | | cmex 33165 |
. . . . 5
class
mEx |
26 | 8, 25 | cfv 6397 |
. . . 4
class
(mEx‘𝑡) |
27 | 24, 4, 26 | crab 3066 |
. . 3
class {𝑎 ∈ (mEx‘𝑡) ∣ ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st
‘𝑎) ∈
(mVT‘𝑡) ∧ Fun
(◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))} |
28 | 2, 3, 27 | cmpt 5149 |
. 2
class (𝑡 ∈ V ↦ {𝑎 ∈ (mEx‘𝑡) ∣ ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st
‘𝑎) ∈
(mVT‘𝑡) ∧ Fun
(◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))}) |
29 | 1, 28 | wceq 1543 |
1
wff mSA =
(𝑡 ∈ V ↦ {𝑎 ∈ (mEx‘𝑡) ∣ ((m0St‘𝑎) ∈ (mAx‘𝑡) ∧ (1st
‘𝑎) ∈
(mVT‘𝑡) ∧ Fun
(◡(2nd ‘𝑎) ↾ (mVR‘𝑡)))}) |