df-msub

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

		Ref	Expression
	Assertion	df-msub	⊢ mSubst = ( 𝑡 ∈ V ↦ ( 𝑓 ∈ ( ( mREx ‘ 𝑡 ) ↑_pm ( mVR ‘ 𝑡 ) ) ↦ ( 𝑒 ∈ ( mEx ‘ 𝑡 ) ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑡 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )

Step	Hyp	Ref	Expression
0		cmsub	⊢ mSubst
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		cmex	⊢ mEx
13	5 12	cfv	⊢ ( mEx ‘ 𝑡 )
14		c1st	⊢ 1^st
15	11	cv	⊢ 𝑒
16	15 14	cfv	⊢ ( 1^st ‘ 𝑒 )
17		cmrsub	⊢ mRSubst
18	5 17	cfv	⊢ ( mRSubst ‘ 𝑡 )
19	3	cv	⊢ 𝑓
20	19 18	cfv	⊢ ( ( mRSubst ‘ 𝑡 ) ‘ 𝑓 )
21		c2nd	⊢ 2^nd
22	15 21	cfv	⊢ ( 2^nd ‘ 𝑒 )
23	22 20	cfv	⊢ ( ( ( mRSubst ‘ 𝑡 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) )
24	16 23	cop	⊢ ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑡 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩
25	11 13 24	cmpt	⊢ ( 𝑒 ∈ ( mEx ‘ 𝑡 ) ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑡 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ )
26	3 10 25	cmpt	⊢ ( 𝑓 ∈ ( ( mREx ‘ 𝑡 ) ↑_pm ( mVR ‘ 𝑡 ) ) ↦ ( 𝑒 ∈ ( mEx ‘ 𝑡 ) ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑡 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) )
27	1 2 26	cmpt	⊢ ( 𝑡 ∈ V ↦ ( 𝑓 ∈ ( ( mREx ‘ 𝑡 ) ↑_pm ( mVR ‘ 𝑡 ) ) ↦ ( 𝑒 ∈ ( mEx ‘ 𝑡 ) ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑡 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )
28	0 27	wceq	⊢ mSubst = ( 𝑡 ∈ V ↦ ( 𝑓 ∈ ( ( mREx ‘ 𝑡 ) ↑_pm ( mVR ‘ 𝑡 ) ) ↦ ( 𝑒 ∈ ( mEx ‘ 𝑡 ) ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑡 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )

Metamath Proof Explorer