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 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) )