msubffval

Description: A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	msubffval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	msubffval.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
	msubffval.s	⊢ 𝑆 = ( mSubst ‘ 𝑇 )
	msubffval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
	msubffval.o	⊢ 𝑂 = ( mRSubst ‘ 𝑇 )
Assertion	msubffval	⊢ ( 𝑇 ∈ 𝑊 → 𝑆 = ( 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )

Proof

Step	Hyp	Ref	Expression
1		msubffval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
2		msubffval.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
3		msubffval.s	⊢ 𝑆 = ( mSubst ‘ 𝑇 )
4		msubffval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
5		msubffval.o	⊢ 𝑂 = ( mRSubst ‘ 𝑇 )
6		elex	⊢ ( 𝑇 ∈ 𝑊 → 𝑇 ∈ V )
7		fveq2	⊢ ( 𝑡 = 𝑇 → ( mREx ‘ 𝑡 ) = ( mREx ‘ 𝑇 ) )
8	7 2	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mREx ‘ 𝑡 ) = 𝑅 )
9		fveq2	⊢ ( 𝑡 = 𝑇 → ( mVR ‘ 𝑡 ) = ( mVR ‘ 𝑇 ) )
10	9 1	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mVR ‘ 𝑡 ) = 𝑉 )
11	8 10	oveq12d	⊢ ( 𝑡 = 𝑇 → ( ( mREx ‘ 𝑡 ) ↑_pm ( mVR ‘ 𝑡 ) ) = ( 𝑅 ↑_pm 𝑉 ) )
12		fveq2	⊢ ( 𝑡 = 𝑇 → ( mEx ‘ 𝑡 ) = ( mEx ‘ 𝑇 ) )
13	12 4	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mEx ‘ 𝑡 ) = 𝐸 )
14		fveq2	⊢ ( 𝑡 = 𝑇 → ( mRSubst ‘ 𝑡 ) = ( mRSubst ‘ 𝑇 ) )
15	14 5	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mRSubst ‘ 𝑡 ) = 𝑂 )
16	15	fveq1d	⊢ ( 𝑡 = 𝑇 → ( ( mRSubst ‘ 𝑡 ) ‘ 𝑓 ) = ( 𝑂 ‘ 𝑓 ) )
17	16	fveq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( mRSubst ‘ 𝑡 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) )
18	17	opeq2d	⊢ ( 𝑡 = 𝑇 → ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑡 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ = ⟨ ( 1^st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ )
19	13 18	mpteq12dv	⊢ ( 𝑡 = 𝑇 → ( 𝑒 ∈ ( mEx ‘ 𝑡 ) ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑡 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) )
20	11 19	mpteq12dv	⊢ ( 𝑡 = 𝑇 → ( 𝑓 ∈ ( ( mREx ‘ 𝑡 ) ↑_pm ( mVR ‘ 𝑡 ) ) ↦ ( 𝑒 ∈ ( mEx ‘ 𝑡 ) ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑡 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) = ( 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )
21		df-msub	⊢ mSubst = ( 𝑡 ∈ V ↦ ( 𝑓 ∈ ( ( mREx ‘ 𝑡 ) ↑_pm ( mVR ‘ 𝑡 ) ) ↦ ( 𝑒 ∈ ( mEx ‘ 𝑡 ) ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑡 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )
22		ovex	⊢ ( 𝑅 ↑_pm 𝑉 ) ∈ V
23	22	mptex	⊢ ( 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) ∈ V
24	20 21 23	fvmpt	⊢ ( 𝑇 ∈ V → ( mSubst ‘ 𝑇 ) = ( 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )
25	3 24	syl5eq	⊢ ( 𝑇 ∈ V → 𝑆 = ( 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )
26	6 25	syl	⊢ ( 𝑇 ∈ 𝑊 → 𝑆 = ( 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )

Metamath Proof Explorer

Theorem msubffval

Proof