Metamath Proof Explorer

Theorem msubval

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	msubval	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) → ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) = ⟨ ( 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	1 2 3 4 5	msubfval	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) → ( 𝑆 ‘ 𝐹 ) = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) )
7	6	3adant3	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) → ( 𝑆 ‘ 𝐹 ) = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) )
8		simpr	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑒 = 𝑋 ) → 𝑒 = 𝑋 )
9	8	fveq2d	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑒 = 𝑋 ) → ( 1^st ‘ 𝑒 ) = ( 1^st ‘ 𝑋 ) )
10	8	fveq2d	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑒 = 𝑋 ) → ( 2^nd ‘ 𝑒 ) = ( 2^nd ‘ 𝑋 ) )
11	10	fveq2d	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑒 = 𝑋 ) → ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2^nd ‘ 𝑒 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2^nd ‘ 𝑋 ) ) )
12	9 11	opeq12d	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑒 = 𝑋 ) → ⟨ ( 1^st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ = ⟨ ( 1^st ‘ 𝑋 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ )
13		simp3	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) → 𝑋 ∈ 𝐸 )
14		opex	⊢ ⟨ ( 1^st ‘ 𝑋 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ ∈ V
15	14	a1i	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) → ⟨ ( 1^st ‘ 𝑋 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ ∈ V )
16	7 12 13 15	fvmptd	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) → ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) = ⟨ ( 1^st ‘ 𝑋 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2^nd ‘ 𝑋 ) ) ⟩ )