Theorem mrsubfval

Description: The substitution of some variables for expressions in a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mrsubffval.c	⊢ 𝐶 = ( mCN ‘ 𝑇 )
	mrsubffval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mrsubffval.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
	mrsubffval.s	⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
	mrsubffval.g	⊢ 𝐺 = ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) )
Assertion	mrsubfval	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) → ( 𝑆 ‘ 𝐹 ) = ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mrsubffval.c	⊢ 𝐶 = ( mCN ‘ 𝑇 )
2		mrsubffval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
3		mrsubffval.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
4		mrsubffval.s	⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
5		mrsubffval.g	⊢ 𝐺 = ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) )
6	1 2 3 4 5	mrsubffval	⊢ ( 𝑇 ∈ V → 𝑆 = ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) )
7	6	adantr	⊢ ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) → 𝑆 = ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) )
8		dmeq	⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
9		fdm	⊢ ( 𝐹 : 𝐴 ⟶ 𝑅 → dom 𝐹 = 𝐴 )
10	9	ad2antrl	⊢ ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) → dom 𝐹 = 𝐴 )
11	8 10	sylan9eqr	⊢ ( ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → dom 𝑓 = 𝐴 )
12	11	eleq2d	⊢ ( ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → ( 𝑣 ∈ dom 𝑓 ↔ 𝑣 ∈ 𝐴 ) )
13		simpr	⊢ ( ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
14	13	fveq1d	⊢ ( ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → ( 𝑓 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑣 ) )
15	12 14	ifbieq1d	⊢ ( ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) = if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) )
16	15	mpteq2dv	⊢ ( ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) = ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) )
17	16	coeq1d	⊢ ( ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) = ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) )
18	17	oveq2d	⊢ ( ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) = ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) )
19	18	mpteq2dv	⊢ ( ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) = ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) )
20	3	fvexi	⊢ 𝑅 ∈ V
21	20	a1i	⊢ ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) → 𝑅 ∈ V )
22	2	fvexi	⊢ 𝑉 ∈ V
23	22	a1i	⊢ ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) → 𝑉 ∈ V )
24		simprl	⊢ ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) → 𝐹 : 𝐴 ⟶ 𝑅 )
25		simprr	⊢ ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) → 𝐴 ⊆ 𝑉 )
26		elpm2r	⊢ ( ( ( 𝑅 ∈ V ∧ 𝑉 ∈ V ) ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) → 𝐹 ∈ ( 𝑅 ↑pm 𝑉 ) )
27	21 23 24 25 26	syl22anc	⊢ ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) → 𝐹 ∈ ( 𝑅 ↑pm 𝑉 ) )
28	20	mptex	⊢ ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ∈ V
29	28	a1i	⊢ ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) → ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ∈ V )
30	7 19 27 29	fvmptd	⊢ ( ( 𝑇 ∈ V ∧ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) ) → ( 𝑆 ‘ 𝐹 ) = ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) )
31	30	ex	⊢ ( 𝑇 ∈ V → ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) → ( 𝑆 ‘ 𝐹 ) = ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) )
32		0fv	⊢ ( ∅ ‘ 𝐹 ) = ∅
33		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mRSubst ‘ 𝑇 ) = ∅ )
34	4 33	syl5eq	⊢ ( ¬ 𝑇 ∈ V → 𝑆 = ∅ )
35	34	fveq1d	⊢ ( ¬ 𝑇 ∈ V → ( 𝑆 ‘ 𝐹 ) = ( ∅ ‘ 𝐹 ) )
36		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mREx ‘ 𝑇 ) = ∅ )
37	3 36	syl5eq	⊢ ( ¬ 𝑇 ∈ V → 𝑅 = ∅ )
38	37	mpteq1d	⊢ ( ¬ 𝑇 ∈ V → ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) = ( 𝑒 ∈ ∅ ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) )
39		mpt0	⊢ ( 𝑒 ∈ ∅ ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) = ∅
40	38 39	eqtrdi	⊢ ( ¬ 𝑇 ∈ V → ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) = ∅ )
41	32 35 40	3eqtr4a	⊢ ( ¬ 𝑇 ∈ V → ( 𝑆 ‘ 𝐹 ) = ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) )
42	41	a1d	⊢ ( ¬ 𝑇 ∈ V → ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) → ( 𝑆 ‘ 𝐹 ) = ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) )
43	31 42	pm2.61i	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) → ( 𝑆 ‘ 𝐹 ) = ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) )