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 ⁡ t v ∈ mCN ⁡ t ∪ mVR ⁡ t ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmrsub class mRSubst
1 vt setvar t
2 cvv class V
3 vf setvar f
4 cmrex class mREx
5 1 cv setvar t
6 5 4 cfv class mREx ⁡ t
7 cpm class ↑ 𝑝𝑚
8 cmvar class mVR
9 5 8 cfv class mVR ⁡ t
10 6 9 7 co class mREx ⁡ t ↑ 𝑝𝑚 mVR ⁡ t
11 ve setvar e
12 cfrmd class freeMnd
13 cmcn class mCN
14 5 13 cfv class mCN ⁡ t
15 14 9 cun class mCN ⁡ t ∪ mVR ⁡ t
16 15 12 cfv class freeMnd ⁡ mCN ⁡ t ∪ mVR ⁡ t
17 cgsu class Σ𝑔
18 vv setvar v
19 18 cv setvar v
20 3 cv setvar f
21 20 cdm class dom ⁡ f
22 19 21 wcel wff v ∈ dom ⁡ f
23 19 20 cfv class f ⁡ v
24 19 cs1 class ⟨“ v ”⟩
25 22 23 24 cif class if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩
26 18 15 25 cmpt class v ∈ mCN ⁡ t ∪ mVR ⁡ t ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩
27 11 cv setvar e
28 26 27 ccom class v ∈ mCN ⁡ t ∪ mVR ⁡ t ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e
29 16 28 17 co class ∑ freeMnd ⁡ mCN ⁡ t ∪ mVR ⁡ t v ∈ mCN ⁡ t ∪ mVR ⁡ t ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e
30 11 6 29 cmpt class e ∈ mREx ⁡ t ⟼ ∑ freeMnd ⁡ mCN ⁡ t ∪ mVR ⁡ t v ∈ mCN ⁡ t ∪ mVR ⁡ t ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e
31 3 10 30 cmpt class f ∈ mREx ⁡ t ↑ 𝑝𝑚 mVR ⁡ t ⟼ e ∈ mREx ⁡ t ⟼ ∑ freeMnd ⁡ mCN ⁡ t ∪ mVR ⁡ t v ∈ mCN ⁡ t ∪ mVR ⁡ t ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e
32 1 2 31 cmpt class t ∈ V ⟼ f ∈ mREx ⁡ t ↑ 𝑝𝑚 mVR ⁡ t ⟼ e ∈ mREx ⁡ t ⟼ ∑ freeMnd ⁡ mCN ⁡ t ∪ mVR ⁡ t v ∈ mCN ⁡ t ∪ mVR ⁡ t ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e
33 0 32 wceq wff mRSubst = t ∈ V ⟼ f ∈ mREx ⁡ t ↑ 𝑝𝑚 mVR ⁡ t ⟼ e ∈ mREx ⁡ t ⟼ ∑ freeMnd ⁡ mCN ⁡ t ∪ mVR ⁡ t v ∈ mCN ⁡ t ∪ mVR ⁡ t ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e