Detailed syntax breakdown of Definition df-msr
Step | Hyp | Ref
| Expression |
1 | | cmsr 33444 |
. 2
class
mStRed |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | cvv 3429 |
. . 3
class
V |
4 | | vs |
. . . 4
setvar 𝑠 |
5 | 2 | cv 1538 |
. . . . 5
class 𝑡 |
6 | | cmpst 33443 |
. . . . 5
class
mPreSt |
7 | 5, 6 | cfv 6426 |
. . . 4
class
(mPreSt‘𝑡) |
8 | | vh |
. . . . 5
setvar ℎ |
9 | 4 | cv 1538 |
. . . . . . 7
class 𝑠 |
10 | | c1st 7818 |
. . . . . . 7
class
1st |
11 | 9, 10 | cfv 6426 |
. . . . . 6
class
(1st ‘𝑠) |
12 | | c2nd 7819 |
. . . . . 6
class
2nd |
13 | 11, 12 | cfv 6426 |
. . . . 5
class
(2nd ‘(1st ‘𝑠)) |
14 | | va |
. . . . . 6
setvar 𝑎 |
15 | 9, 12 | cfv 6426 |
. . . . . 6
class
(2nd ‘𝑠) |
16 | 11, 10 | cfv 6426 |
. . . . . . . 8
class
(1st ‘(1st ‘𝑠)) |
17 | | vz |
. . . . . . . . 9
setvar 𝑧 |
18 | | cmvrs 33439 |
. . . . . . . . . . . 12
class
mVars |
19 | 5, 18 | cfv 6426 |
. . . . . . . . . . 11
class
(mVars‘𝑡) |
20 | 8 | cv 1538 |
. . . . . . . . . . . 12
class ℎ |
21 | 14 | cv 1538 |
. . . . . . . . . . . . 13
class 𝑎 |
22 | 21 | csn 4561 |
. . . . . . . . . . . 12
class {𝑎} |
23 | 20, 22 | cun 3884 |
. . . . . . . . . . 11
class (ℎ ∪ {𝑎}) |
24 | 19, 23 | cima 5587 |
. . . . . . . . . 10
class
((mVars‘𝑡)
“ (ℎ ∪ {𝑎})) |
25 | 24 | cuni 4839 |
. . . . . . . . 9
class ∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) |
26 | 17 | cv 1538 |
. . . . . . . . . 10
class 𝑧 |
27 | 26, 26 | cxp 5582 |
. . . . . . . . 9
class (𝑧 × 𝑧) |
28 | 17, 25, 27 | csb 3831 |
. . . . . . . 8
class
⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧) |
29 | 16, 28 | cin 3885 |
. . . . . . 7
class
((1st ‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)) |
30 | 29, 20, 21 | cotp 4569 |
. . . . . 6
class
〈((1st ‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 |
31 | 14, 15, 30 | csb 3831 |
. . . . 5
class
⦋(2nd ‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 |
32 | 8, 13, 31 | csb 3831 |
. . . 4
class
⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉 |
33 | 4, 7, 32 | cmpt 5156 |
. . 3
class (𝑠 ∈ (mPreSt‘𝑡) ↦
⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉) |
34 | 2, 3, 33 | cmpt 5156 |
. 2
class (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦
⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉)) |
35 | 1, 34 | wceq 1539 |
1
wff mStRed =
(𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦
⦋(2nd ‘(1st ‘𝑠)) / ℎ⦌⦋(2nd
‘𝑠) / 𝑎⦌〈((1st
‘(1st ‘𝑠)) ∩ ⦋∪ ((mVars‘𝑡) “ (ℎ ∪ {𝑎})) / 𝑧⦌(𝑧 × 𝑧)), ℎ, 𝑎〉)) |