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 34152
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 34132 . 2 class mStRed
2 vt . . 3 setvar 𝑑
3 cvv 3447 . . 3 class V
4 vs . . . 4 setvar 𝑠
52cv 1541 . . . . 5 class 𝑑
6 cmpst 34131 . . . . 5 class mPreSt
75, 6cfv 6500 . . . 4 class (mPreStβ€˜π‘‘)
8 vh . . . . 5 setvar β„Ž
94cv 1541 . . . . . . 7 class 𝑠
10 c1st 7923 . . . . . . 7 class 1st
119, 10cfv 6500 . . . . . 6 class (1st β€˜π‘ )
12 c2nd 7924 . . . . . 6 class 2nd
1311, 12cfv 6500 . . . . 5 class (2nd β€˜(1st β€˜π‘ ))
14 va . . . . . 6 setvar π‘Ž
159, 12cfv 6500 . . . . . 6 class (2nd β€˜π‘ )
1611, 10cfv 6500 . . . . . . . 8 class (1st β€˜(1st β€˜π‘ ))
17 vz . . . . . . . . 9 setvar 𝑧
18 cmvrs 34127 . . . . . . . . . . . 12 class mVars
195, 18cfv 6500 . . . . . . . . . . 11 class (mVarsβ€˜π‘‘)
208cv 1541 . . . . . . . . . . . 12 class β„Ž
2114cv 1541 . . . . . . . . . . . . 13 class π‘Ž
2221csn 4590 . . . . . . . . . . . 12 class {π‘Ž}
2320, 22cun 3912 . . . . . . . . . . 11 class (β„Ž βˆͺ {π‘Ž})
2419, 23cima 5640 . . . . . . . . . 10 class ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž}))
2524cuni 4869 . . . . . . . . 9 class βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž}))
2617cv 1541 . . . . . . . . . 10 class 𝑧
2726, 26cxp 5635 . . . . . . . . 9 class (𝑧 Γ— 𝑧)
2817, 25, 27csb 3859 . . . . . . . 8 class ⦋βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž})) / π‘§β¦Œ(𝑧 Γ— 𝑧)
2916, 28cin 3913 . . . . . . 7 class ((1st β€˜(1st β€˜π‘ )) ∩ ⦋βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž})) / π‘§β¦Œ(𝑧 Γ— 𝑧))
3029, 20, 21cotp 4598 . . . . . 6 class ⟨((1st β€˜(1st β€˜π‘ )) ∩ ⦋βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž})) / π‘§β¦Œ(𝑧 Γ— 𝑧)), β„Ž, π‘ŽβŸ©
3114, 15, 30csb 3859 . . . . 5 class ⦋(2nd β€˜π‘ ) / π‘Žβ¦ŒβŸ¨((1st β€˜(1st β€˜π‘ )) ∩ ⦋βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž})) / π‘§β¦Œ(𝑧 Γ— 𝑧)), β„Ž, π‘ŽβŸ©
328, 13, 31csb 3859 . . . 4 class ⦋(2nd β€˜(1st β€˜π‘ )) / β„Žβ¦Œβ¦‹(2nd β€˜π‘ ) / π‘Žβ¦ŒβŸ¨((1st β€˜(1st β€˜π‘ )) ∩ ⦋βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž})) / π‘§β¦Œ(𝑧 Γ— 𝑧)), β„Ž, π‘ŽβŸ©
334, 7, 32cmpt 5192 . . 3 class (𝑠 ∈ (mPreStβ€˜π‘‘) ↦ ⦋(2nd β€˜(1st β€˜π‘ )) / β„Žβ¦Œβ¦‹(2nd β€˜π‘ ) / π‘Žβ¦ŒβŸ¨((1st β€˜(1st β€˜π‘ )) ∩ ⦋βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž})) / π‘§β¦Œ(𝑧 Γ— 𝑧)), β„Ž, π‘ŽβŸ©)
342, 3, 33cmpt 5192 . 2 class (𝑑 ∈ V ↦ (𝑠 ∈ (mPreStβ€˜π‘‘) ↦ ⦋(2nd β€˜(1st β€˜π‘ )) / β„Žβ¦Œβ¦‹(2nd β€˜π‘ ) / π‘Žβ¦ŒβŸ¨((1st β€˜(1st β€˜π‘ )) ∩ ⦋βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž})) / π‘§β¦Œ(𝑧 Γ— 𝑧)), β„Ž, π‘ŽβŸ©))
351, 34wceq 1542 1 wff mStRed = (𝑑 ∈ V ↦ (𝑠 ∈ (mPreStβ€˜π‘‘) ↦ ⦋(2nd β€˜(1st β€˜π‘ )) / β„Žβ¦Œβ¦‹(2nd β€˜π‘ ) / π‘Žβ¦ŒβŸ¨((1st β€˜(1st β€˜π‘ )) ∩ ⦋βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž})) / π‘§β¦Œ(𝑧 Γ— 𝑧)), β„Ž, π‘ŽβŸ©))
Colors of variables: wff setvar class
This definition is referenced by:  msrfval  34195
  Copyright terms: Public domain W3C validator