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 32749
 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 32729 . 2 class mStRed
2 vt . . 3 setvar 𝑡
3 cvv 3471 . . 3 class V
4 vs . . . 4 setvar 𝑠
52cv 1537 . . . . 5 class 𝑡
6 cmpst 32728 . . . . 5 class mPreSt
75, 6cfv 6328 . . . 4 class (mPreSt‘𝑡)
8 vh . . . . 5 setvar
94cv 1537 . . . . . . 7 class 𝑠
10 c1st 7662 . . . . . . 7 class 1st
119, 10cfv 6328 . . . . . 6 class (1st𝑠)
12 c2nd 7663 . . . . . 6 class 2nd
1311, 12cfv 6328 . . . . 5 class (2nd ‘(1st𝑠))
14 va . . . . . 6 setvar 𝑎
159, 12cfv 6328 . . . . . 6 class (2nd𝑠)
1611, 10cfv 6328 . . . . . . . 8 class (1st ‘(1st𝑠))
17 vz . . . . . . . . 9 setvar 𝑧
18 cmvrs 32724 . . . . . . . . . . . 12 class mVars
195, 18cfv 6328 . . . . . . . . . . 11 class (mVars‘𝑡)
208cv 1537 . . . . . . . . . . . 12 class
2114cv 1537 . . . . . . . . . . . . 13 class 𝑎
2221csn 4540 . . . . . . . . . . . 12 class {𝑎}
2320, 22cun 3908 . . . . . . . . . . 11 class ( ∪ {𝑎})
2419, 23cima 5531 . . . . . . . . . 10 class ((mVars‘𝑡) “ ( ∪ {𝑎}))
2524cuni 4811 . . . . . . . . 9 class ((mVars‘𝑡) “ ( ∪ {𝑎}))
2617cv 1537 . . . . . . . . . 10 class 𝑧
2726, 26cxp 5526 . . . . . . . . 9 class (𝑧 × 𝑧)
2817, 25, 27csb 3857 . . . . . . . 8 class ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)
2916, 28cin 3909 . . . . . . 7 class ((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧))
3029, 20, 21cotp 4548 . . . . . 6 class ⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎
3114, 15, 30csb 3857 . . . . 5 class (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎
328, 13, 31csb 3857 . . . 4 class (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎
334, 7, 32cmpt 5119 . . 3 class (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩)
342, 3, 33cmpt 5119 . 2 class (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
351, 34wceq 1538 1 wff mStRed = (𝑡 ∈ V ↦ (𝑠 ∈ (mPreSt‘𝑡) ↦ (2nd ‘(1st𝑠)) / (2nd𝑠) / 𝑎⟨((1st ‘(1st𝑠)) ∩ ((mVars‘𝑡) “ ( ∪ {𝑎})) / 𝑧(𝑧 × 𝑧)), , 𝑎⟩))
 Colors of variables: wff setvar class This definition is referenced by:  msrfval  32792
 Copyright terms: Public domain W3C validator