Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-msr Structured version   Visualization version   GIF version

Definition df-msr 30645
Description: Define the reduct of a pre-statement. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-msr mStRed = (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
Distinct variable group:   ,𝑎,𝑠,𝑡,𝑧

Detailed syntax breakdown of Definition df-msr
StepHypRef Expression
1 cmsr 30625 . 2 class mStRed
2 vt . . 3 setvar 𝑡
3 cvv 3173 . . 3 class V
4 vs . . . 4 setvar 𝑠
52cv 1474 . . . . 5 class 𝑡
6 cmpst 30624 . . . . 5 class mPreSt
75, 6cfv 5804 . . . 4 class (mPreSt‘𝑡)
8 vh . . . . 5 setvar
94cv 1474 . . . . . . 7 class 𝑠
10 c1st 7057 . . . . . . 7 class 1st
119, 10cfv 5804 . . . . . 6 class (1st𝑠)
12 c2nd 7058 . . . . . 6 class 2nd
1311, 12cfv 5804 . . . . 5 class (2nd ‘(1st𝑠))
14 va . . . . . 6 setvar 𝑎
159, 12cfv 5804 . . . . . 6 class (2nd𝑠)
1611, 10cfv 5804 . . . . . . . 8 class (1st ‘(1st𝑠))
17 vz . . . . . . . . 9 setvar 𝑧
18 cmvrs 30620 . . . . . . . . . . . 12 class mVars
195, 18cfv 5804 . . . . . . . . . . 11 class (mVars‘𝑡)
208cv 1474 . . . . . . . . . . . 12 class
2114cv 1474 . . . . . . . . . . . . 13 class 𝑎
2221csn 4125 . . . . . . . . . . . 12 class {𝑎}
2320, 22cun 3538 . . . . . . . . . . 11 class ( ∪ {𝑎})
2419, 23cima 5041 . . . . . . . . . 10 class ((mVars‘𝑡) “ ( ∪ {𝑎}))
2524cuni 4372 . . . . . . . . 9 class ((mVars‘𝑡) “ ( ∪ {𝑎}))
2617cv 1474 . . . . . . . . . 10 class 𝑧
2726, 26cxp 5036 . . . . . . . . 9 class (𝑧 × 𝑧)
2817, 25, 27csb 3499 . . . . . . . 8 class ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)
2916, 28cin 3539 . . . . . . 7 class ((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧))
3029, 20, 21cotp 4133 . . . . . 6 class ⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎
3114, 15, 30csb 3499 . . . . 5 class (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎
328, 13, 31csb 3499 . . . 4 class (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎
334, 7, 32cmpt 4643 . . 3 class (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
342, 3, 33cmpt 4643 . 2 class (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
351, 34wceq 1475 1 wff mStRed = (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
Colors of variables: wff setvar class
This definition is referenced by:  msrfval  30688
  Copyright terms: Public domain W3C validator