Metamath Proof Explorer

Definition df-mrsub

Description: Define a substitution of raw expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mrsub ⊢mRSubst=t∈V⟼f∈mREx⁡t↑𝑝𝑚mVR⁡t⟼e∈mREx⁡t⟼∑freeMnd⁡mCN⁡t∪mVR⁡tv∈mCN⁡t∪mVR⁡t⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmrsub classmRSubst
1 vt setvart
2 cvv classV
3 vf setvarf
4 cmrex classmREx
5 1 cv setvart
6 5 4 cfv classmREx⁡t
7 cpm class↑𝑝𝑚
8 cmvar classmVR
9 5 8 cfv classmVR⁡t
10 6 9 7 co classmREx⁡t↑𝑝𝑚mVR⁡t
11 ve setvare
12 cfrmd classfreeMnd
13 cmcn classmCN
14 5 13 cfv classmCN⁡t
15 14 9 cun classmCN⁡t∪mVR⁡t
16 15 12 cfv classfreeMnd⁡mCN⁡t∪mVR⁡t
17 cgsu classΣ𝑔
18 vv setvarv
19 18 cv setvarv
20 3 cv setvarf
21 20 cdm classdom⁡f
22 19 21 wcel wffv∈dom⁡f
23 19 20 cfv classf⁡v
24 19 cs1 class⟨“v”⟩
25 22 23 24 cif classifv∈dom⁡ff⁡v⟨“v”⟩
26 18 15 25 cmpt classv∈mCN⁡t∪mVR⁡t⟼ifv∈dom⁡ff⁡v⟨“v”⟩
27 11 cv setvare
28 26 27 ccom classv∈mCN⁡t∪mVR⁡t⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e
29 16 28 17 co class∑freeMnd⁡mCN⁡t∪mVR⁡tv∈mCN⁡t∪mVR⁡t⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e
30 11 6 29 cmpt classe∈mREx⁡t⟼∑freeMnd⁡mCN⁡t∪mVR⁡tv∈mCN⁡t∪mVR⁡t⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e
31 3 10 30 cmpt classf∈mREx⁡t↑𝑝𝑚mVR⁡t⟼e∈mREx⁡t⟼∑freeMnd⁡mCN⁡t∪mVR⁡tv∈mCN⁡t∪mVR⁡t⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e
32 1 2 31 cmpt classt∈V⟼f∈mREx⁡t↑𝑝𝑚mVR⁡t⟼e∈mREx⁡t⟼∑freeMnd⁡mCN⁡t∪mVR⁡tv∈mCN⁡t∪mVR⁡t⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e
33 0 32 wceq wffmRSubst=t∈V⟼f∈mREx⁡t↑𝑝𝑚mVR⁡t⟼e∈mREx⁡t⟼∑freeMnd⁡mCN⁡t∪mVR⁡tv∈mCN⁡t∪mVR⁡t⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e