Detailed syntax breakdown of Definition df-mrsub
Step | Hyp | Ref
| Expression |
1 | | cmrsub 33419 |
. 2
class
mRSubst |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | cvv 3431 |
. . 3
class
V |
4 | | vf |
. . . 4
setvar 𝑓 |
5 | 2 | cv 1538 |
. . . . . 6
class 𝑡 |
6 | | cmrex 33415 |
. . . . . 6
class
mREx |
7 | 5, 6 | cfv 6428 |
. . . . 5
class
(mREx‘𝑡) |
8 | | cmvar 33410 |
. . . . . 6
class
mVR |
9 | 5, 8 | cfv 6428 |
. . . . 5
class
(mVR‘𝑡) |
10 | | cpm 8605 |
. . . . 5
class
↑pm |
11 | 7, 9, 10 | co 7269 |
. . . 4
class
((mREx‘𝑡)
↑pm (mVR‘𝑡)) |
12 | | ve |
. . . . 5
setvar 𝑒 |
13 | | cmcn 33409 |
. . . . . . . . 9
class
mCN |
14 | 5, 13 | cfv 6428 |
. . . . . . . 8
class
(mCN‘𝑡) |
15 | 14, 9 | cun 3886 |
. . . . . . 7
class
((mCN‘𝑡) ∪
(mVR‘𝑡)) |
16 | | cfrmd 18475 |
. . . . . . 7
class
freeMnd |
17 | 15, 16 | cfv 6428 |
. . . . . 6
class
(freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) |
18 | | vv |
. . . . . . . 8
setvar 𝑣 |
19 | 18 | cv 1538 |
. . . . . . . . . 10
class 𝑣 |
20 | 4 | cv 1538 |
. . . . . . . . . . 11
class 𝑓 |
21 | 20 | cdm 5586 |
. . . . . . . . . 10
class dom 𝑓 |
22 | 19, 21 | wcel 2106 |
. . . . . . . . 9
wff 𝑣 ∈ dom 𝑓 |
23 | 19, 20 | cfv 6428 |
. . . . . . . . 9
class (𝑓‘𝑣) |
24 | 19 | cs1 14289 |
. . . . . . . . 9
class
〈“𝑣”〉 |
25 | 22, 23, 24 | cif 4461 |
. . . . . . . 8
class if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉) |
26 | 18, 15, 25 | cmpt 5158 |
. . . . . . 7
class (𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) |
27 | 12 | cv 1538 |
. . . . . . 7
class 𝑒 |
28 | 26, 27 | ccom 5590 |
. . . . . 6
class ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒) |
29 | | cgsu 17140 |
. . . . . 6
class
Σg |
30 | 17, 28, 29 | co 7269 |
. . . . 5
class
((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)) |
31 | 12, 7, 30 | cmpt 5158 |
. . . 4
class (𝑒 ∈ (mREx‘𝑡) ↦
((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))) |
32 | 4, 11, 31 | cmpt 5158 |
. . 3
class (𝑓 ∈ ((mREx‘𝑡) ↑pm
(mVR‘𝑡)) ↦
(𝑒 ∈ (mREx‘𝑡) ↦
((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒)))) |
33 | 2, 3, 32 | cmpt 5158 |
. 2
class (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm
(mVR‘𝑡)) ↦
(𝑒 ∈ (mREx‘𝑡) ↦
((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))))) |
34 | 1, 33 | wceq 1539 |
1
wff mRSubst =
(𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm
(mVR‘𝑡)) ↦
(𝑒 ∈ (mREx‘𝑡) ↦
((freeMnd‘((mCN‘𝑡) ∪ (mVR‘𝑡))) Σg ((𝑣 ∈ ((mCN‘𝑡) ∪ (mVR‘𝑡)) ↦ if(𝑣 ∈ dom 𝑓, (𝑓‘𝑣), 〈“𝑣”〉)) ∘ 𝑒))))) |