Definition df-msr

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

	Ref	Expression
Assertion	df-msr	⊢ mStRed = ( 𝑡 ∈ V ↦ ( 𝑠 ∈ ( mPreSt ‘ 𝑡 ) ↦ ⦋ ( 2nd ‘ ( 1st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1st ‘ ( 1st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmsr	⊢ mStRed
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		vs	⊢ 𝑠
4		cmpst	⊢ mPreSt
5	1	cv	⊢ 𝑡
6	5 4	cfv	⊢ ( mPreSt ‘ 𝑡 )
7		c2nd	⊢ 2nd
8		c1st	⊢ 1st
9	3	cv	⊢ 𝑠
10	9 8	cfv	⊢ ( 1st ‘ 𝑠 )
11	10 7	cfv	⊢ ( 2nd ‘ ( 1st ‘ 𝑠 ) )
12		vh	⊢ ℎ
13	9 7	cfv	⊢ ( 2nd ‘ 𝑠 )
14		va	⊢ 𝑎
15	10 8	cfv	⊢ ( 1st ‘ ( 1st ‘ 𝑠 ) )
16		cmvrs	⊢ mVars
17	5 16	cfv	⊢ ( mVars ‘ 𝑡 )
18	12	cv	⊢ ℎ
19	14	cv	⊢ 𝑎
20	19	csn	⊢ { 𝑎 }
21	18 20	cun	⊢ ( ℎ ∪ { 𝑎 } )
22	17 21	cima	⊢ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) )
23	22	cuni	⊢ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) )
24		vz	⊢ 𝑧
25	24	cv	⊢ 𝑧
26	25 25	cxp	⊢ ( 𝑧 × 𝑧 )
27	24 23 26	csb	⊢ ⦋ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 )
28	15 27	cin	⊢ ( ( 1st ‘ ( 1st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) )
29	28 18 19	cotp	⊢ ⟨ ( ( 1st ‘ ( 1st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩
30	14 13 29	csb	⊢ ⦋ ( 2nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1st ‘ ( 1st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩
31	12 11 30	csb	⊢ ⦋ ( 2nd ‘ ( 1st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1st ‘ ( 1st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩
32	3 6 31	cmpt	⊢ ( 𝑠 ∈ ( mPreSt ‘ 𝑡 ) ↦ ⦋ ( 2nd ‘ ( 1st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1st ‘ ( 1st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ )
33	1 2 32	cmpt	⊢ ( 𝑡 ∈ V ↦ ( 𝑠 ∈ ( mPreSt ‘ 𝑡 ) ↦ ⦋ ( 2nd ‘ ( 1st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1st ‘ ( 1st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ ) )
34	0 33	wceq	⊢ mStRed = ( 𝑡 ∈ V ↦ ( 𝑠 ∈ ( mPreSt ‘ 𝑡 ) ↦ ⦋ ( 2nd ‘ ( 1st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1st ‘ ( 1st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑡 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ ) )