Theorem msubfval

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	msubfval	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) → ( 𝑆 ‘ 𝐹 ) = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) )

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	msubffval	⊢ ( 𝑇 ∈ V → 𝑆 = ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ) )
7	6	adantr	⊢ ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) → 𝑆 = ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ) )
8		simplr	⊢ ( ( ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑒 ∈ 𝐸 ) → 𝑓 = 𝐹 )
9	8	fveq2d	⊢ ( ( ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝑂 ‘ 𝑓 ) = ( 𝑂 ‘ 𝐹 ) )
10	9	fveq1d	⊢ ( ( ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑒 ∈ 𝐸 ) → ( ( 𝑂 ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑒 ) ) )
11	10	opeq2d	⊢ ( ( ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑒 ∈ 𝐸 ) → ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ = ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ )
12	11	mpteq2dva	⊢ ( ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) )
13	2	fvexi	⊢ 𝑅 ∈ V
14	1	fvexi	⊢ 𝑉 ∈ V
15	13 14	pm3.2i	⊢ ( 𝑅 ∈ V ∧ 𝑉 ∈ V )
16	15	a1i	⊢ ( 𝑇 ∈ V → ( 𝑅 ∈ V ∧ 𝑉 ∈ V ) )
17		elpm2r	⊢ ( ( ( 𝑅 ∈ V ∧ 𝑉 ∈ V ) ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) → 𝐹 ∈ ( 𝑅 ↑pm 𝑉 ) )
18	16 17	sylan	⊢ ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) → 𝐹 ∈ ( 𝑅 ↑pm 𝑉 ) )
19	4	fvexi	⊢ 𝐸 ∈ V
20	19	mptex	⊢ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ∈ V
21	20	a1i	⊢ ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) → ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ∈ V )
22	7 12 18 21	fvmptd	⊢ ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) → ( 𝑆 ‘ 𝐹 ) = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) )
23	22	ex	⊢ ( 𝑇 ∈ V → ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) → ( 𝑆 ‘ 𝐹 ) = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ) )
24		0fv	⊢ ( ∅ ‘ 𝐹 ) = ∅
25		mpt0	⊢ ( 𝑒 ∈ ∅ ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) = ∅
26	24 25	eqtr4i	⊢ ( ∅ ‘ 𝐹 ) = ( 𝑒 ∈ ∅ ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ )
27		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mSubst ‘ 𝑇 ) = ∅ )
28	3 27	syl5eq	⊢ ( ¬ 𝑇 ∈ V → 𝑆 = ∅ )
29	28	fveq1d	⊢ ( ¬ 𝑇 ∈ V → ( 𝑆 ‘ 𝐹 ) = ( ∅ ‘ 𝐹 ) )
30		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mEx ‘ 𝑇 ) = ∅ )
31	4 30	syl5eq	⊢ ( ¬ 𝑇 ∈ V → 𝐸 = ∅ )
32	31	mpteq1d	⊢ ( ¬ 𝑇 ∈ V → ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) = ( 𝑒 ∈ ∅ ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) )
33	26 29 32	3eqtr4a	⊢ ( ¬ 𝑇 ∈ V → ( 𝑆 ‘ 𝐹 ) = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) )
34	33	a1d	⊢ ( ¬ 𝑇 ∈ V → ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) → ( 𝑆 ‘ 𝐹 ) = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ) )
35	23 34	pm2.61i	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) → ( 𝑆 ‘ 𝐹 ) = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) )