msrfval

Description: Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	msrfval.v	⊢ 𝑉 = ( mVars ‘ 𝑇 )
	msrfval.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
	msrfval.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
Assertion	msrfval	⊢ 𝑅 = ( 𝑠 ∈ 𝑃 ↦ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		msrfval.v	⊢ 𝑉 = ( mVars ‘ 𝑇 )
2		msrfval.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
3		msrfval.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
4		fveq2	⊢ ( 𝑡 = 𝑇 → ( mPreSt ‘ 𝑡 ) = ( mPreSt ‘ 𝑇 ) )
5	4 2	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mPreSt ‘ 𝑡 ) = 𝑃 )
6		fveq2	⊢ ( 𝑡 = 𝑇 → ( mVars ‘ 𝑡 ) = ( mVars ‘ 𝑇 ) )
7	6 1	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mVars ‘ 𝑡 ) = 𝑉 )
8	7	imaeq1d	⊢ ( 𝑡 = 𝑇 → ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) = ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) )
9	8	unieqd	⊢ ( 𝑡 = 𝑇 → ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) = ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) )
10	9	csbeq1d	⊢ ( 𝑡 = 𝑇 → ⦋ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) = ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) )
11	10	ineq2d	⊢ ( 𝑡 = 𝑇 → ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) )
12	11	oteq1d	⊢ ( 𝑡 = 𝑇 → ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ = ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ )
13	12	csbeq2dv	⊢ ( 𝑡 = 𝑇 → ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ = ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ )
14	13	csbeq2dv	⊢ ( 𝑡 = 𝑇 → ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ = ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ )
15	5 14	mpteq12dv	⊢ ( 𝑡 = 𝑇 → ( 𝑠 ∈ ( mPreSt ‘ 𝑡 ) ↦ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ ) = ( 𝑠 ∈ 𝑃 ↦ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ ) )
16		df-msr	⊢ mStRed = ( 𝑡 ∈ V ↦ ( 𝑠 ∈ ( mPreSt ‘ 𝑡 ) ↦ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ ) )
17	15 16 2	mptfvmpt	⊢ ( 𝑇 ∈ V → ( mStRed ‘ 𝑇 ) = ( 𝑠 ∈ 𝑃 ↦ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ ) )
18		mpt0	⊢ ( 𝑠 ∈ ∅ ↦ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ ) = ∅
19	18	eqcomi	⊢ ∅ = ( 𝑠 ∈ ∅ ↦ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ )
20		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mStRed ‘ 𝑇 ) = ∅ )
21		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mPreSt ‘ 𝑇 ) = ∅ )
22	2 21	syl5eq	⊢ ( ¬ 𝑇 ∈ V → 𝑃 = ∅ )
23	22	mpteq1d	⊢ ( ¬ 𝑇 ∈ V → ( 𝑠 ∈ 𝑃 ↦ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ ) = ( 𝑠 ∈ ∅ ↦ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ ) )
24	19 20 23	3eqtr4a	⊢ ( ¬ 𝑇 ∈ V → ( mStRed ‘ 𝑇 ) = ( 𝑠 ∈ 𝑃 ↦ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ ) )
25	17 24	pm2.61i	⊢ ( mStRed ‘ 𝑇 ) = ( 𝑠 ∈ 𝑃 ↦ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ )
26	3 25	eqtri	⊢ 𝑅 = ( 𝑠 ∈ 𝑃 ↦ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ )

Metamath Proof Explorer

Theorem msrfval

Proof