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 32638
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 32618 . 2 class mStRed
2 vt . . 3 setvar 𝑡
3 cvv 3492 . . 3 class V
4 vs . . . 4 setvar 𝑠
52cv 1527 . . . . 5 class 𝑡
6 cmpst 32617 . . . . 5 class mPreSt
75, 6cfv 6348 . . . 4 class (mPreSt‘𝑡)
8 vh . . . . 5 setvar
94cv 1527 . . . . . . 7 class 𝑠
10 c1st 7676 . . . . . . 7 class 1st
119, 10cfv 6348 . . . . . 6 class (1st𝑠)
12 c2nd 7677 . . . . . 6 class 2nd
1311, 12cfv 6348 . . . . 5 class (2nd ‘(1st𝑠))
14 va . . . . . 6 setvar 𝑎
159, 12cfv 6348 . . . . . 6 class (2nd𝑠)
1611, 10cfv 6348 . . . . . . . 8 class (1st ‘(1st𝑠))
17 vz . . . . . . . . 9 setvar 𝑧
18 cmvrs 32613 . . . . . . . . . . . 12 class mVars
195, 18cfv 6348 . . . . . . . . . . 11 class (mVars‘𝑡)
208cv 1527 . . . . . . . . . . . 12 class
2114cv 1527 . . . . . . . . . . . . 13 class 𝑎
2221csn 4557 . . . . . . . . . . . 12 class {𝑎}
2320, 22cun 3931 . . . . . . . . . . 11 class ( ∪ {𝑎})
2419, 23cima 5551 . . . . . . . . . 10 class ((mVars‘𝑡) “ ( ∪ {𝑎}))
2524cuni 4830 . . . . . . . . 9 class ((mVars‘𝑡) “ ( ∪ {𝑎}))
2617cv 1527 . . . . . . . . . 10 class 𝑧
2726, 26cxp 5546 . . . . . . . . 9 class (𝑧 × 𝑧)
2817, 25, 27csb 3880 . . . . . . . 8 class ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)
2916, 28cin 3932 . . . . . . 7 class ((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧))
3029, 20, 21cotp 4565 . . . . . 6 class ⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎
3114, 15, 30csb 3880 . . . . 5 class (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎
328, 13, 31csb 3880 . . . 4 class (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎
334, 7, 32cmpt 5137 . . 3 class (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
342, 3, 33cmpt 5137 . 2 class (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
351, 34wceq 1528 1 wff mStRed = (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
Colors of variables: wff setvar class
This definition is referenced by:  msrfval  32681
  Copyright terms: Public domain W3C validator