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 33464
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 33444 . 2 class mStRed
2 vt . . 3 setvar 𝑡
3 cvv 3429 . . 3 class V
4 vs . . . 4 setvar 𝑠
52cv 1538 . . . . 5 class 𝑡
6 cmpst 33443 . . . . 5 class mPreSt
75, 6cfv 6426 . . . 4 class (mPreSt‘𝑡)
8 vh . . . . 5 setvar
94cv 1538 . . . . . . 7 class 𝑠
10 c1st 7818 . . . . . . 7 class 1st
119, 10cfv 6426 . . . . . 6 class (1st𝑠)
12 c2nd 7819 . . . . . 6 class 2nd
1311, 12cfv 6426 . . . . 5 class (2nd ‘(1st𝑠))
14 va . . . . . 6 setvar 𝑎
159, 12cfv 6426 . . . . . 6 class (2nd𝑠)
1611, 10cfv 6426 . . . . . . . 8 class (1st ‘(1st𝑠))
17 vz . . . . . . . . 9 setvar 𝑧
18 cmvrs 33439 . . . . . . . . . . . 12 class mVars
195, 18cfv 6426 . . . . . . . . . . 11 class (mVars‘𝑡)
208cv 1538 . . . . . . . . . . . 12 class
2114cv 1538 . . . . . . . . . . . . 13 class 𝑎
2221csn 4561 . . . . . . . . . . . 12 class {𝑎}
2320, 22cun 3884 . . . . . . . . . . 11 class ( ∪ {𝑎})
2419, 23cima 5587 . . . . . . . . . 10 class ((mVars‘𝑡) “ ( ∪ {𝑎}))
2524cuni 4839 . . . . . . . . 9 class ((mVars‘𝑡) “ ( ∪ {𝑎}))
2617cv 1538 . . . . . . . . . 10 class 𝑧
2726, 26cxp 5582 . . . . . . . . 9 class (𝑧 × 𝑧)
2817, 25, 27csb 3831 . . . . . . . 8 class ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)
2916, 28cin 3885 . . . . . . 7 class ((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧))
3029, 20, 21cotp 4569 . . . . . 6 class ⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎
3114, 15, 30csb 3831 . . . . 5 class (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎
328, 13, 31csb 3831 . . . 4 class (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎
334, 7, 32cmpt 5156 . . 3 class (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
342, 3, 33cmpt 5156 . 2 class (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
351, 34wceq 1539 1 wff mStRed = (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
Colors of variables: wff setvar class
This definition is referenced by:  msrfval  33507
  Copyright terms: Public domain W3C validator