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 = ( 𝑡 ∈ V ↦ ( 𝑓 ∈ ( ( mREx ‘ 𝑡 ) ↑pm ( mVR ‘ 𝑡 ) ) ↦ ( 𝑒 ∈ ( mREx ‘ 𝑡 ) ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmrsub mRSubst
1 vt 𝑡
2 cvv V
3 vf 𝑓
4 cmrex mREx
5 1 cv 𝑡
6 5 4 cfv ( mREx ‘ 𝑡 )
7 cpm pm
8 cmvar mVR
9 5 8 cfv ( mVR ‘ 𝑡 )
10 6 9 7 co ( ( mREx ‘ 𝑡 ) ↑pm ( mVR ‘ 𝑡 ) )
11 ve 𝑒
12 cfrmd freeMnd
13 cmcn mCN
14 5 13 cfv ( mCN ‘ 𝑡 )
15 14 9 cun ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) )
16 15 12 cfv ( freeMnd ‘ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) )
17 cgsu Σg
18 vv 𝑣
19 18 cv 𝑣
20 3 cv 𝑓
21 20 cdm dom 𝑓
22 19 21 wcel 𝑣 ∈ dom 𝑓
23 19 20 cfv ( 𝑓𝑣 )
24 19 cs1 ⟨“ 𝑣 ”⟩
25 22 23 24 cif if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ )
26 18 15 25 cmpt ( 𝑣 ∈ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) )
27 11 cv 𝑒
28 26 27 ccom ( ( 𝑣 ∈ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 )
29 16 28 17 co ( ( freeMnd ‘ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) )
30 11 6 29 cmpt ( 𝑒 ∈ ( mREx ‘ 𝑡 ) ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) )
31 3 10 30 cmpt ( 𝑓 ∈ ( ( mREx ‘ 𝑡 ) ↑pm ( mVR ‘ 𝑡 ) ) ↦ ( 𝑒 ∈ ( mREx ‘ 𝑡 ) ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) )
32 1 2 31 cmpt ( 𝑡 ∈ V ↦ ( 𝑓 ∈ ( ( mREx ‘ 𝑡 ) ↑pm ( mVR ‘ 𝑡 ) ) ↦ ( 𝑒 ∈ ( mREx ‘ 𝑡 ) ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) )
33 0 32 wceq mRSubst = ( 𝑡 ∈ V ↦ ( 𝑓 ∈ ( ( mREx ‘ 𝑡 ) ↑pm ( mVR ‘ 𝑡 ) ) ↦ ( 𝑒 ∈ ( mREx ‘ 𝑡 ) ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) )