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 34480
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 34460 . 2 class mStRed
2 vt . . 3 setvar 𝑑
3 cvv 3474 . . 3 class V
4 vs . . . 4 setvar 𝑠
52cv 1540 . . . . 5 class 𝑑
6 cmpst 34459 . . . . 5 class mPreSt
75, 6cfv 6543 . . . 4 class (mPreStβ€˜π‘‘)
8 vh . . . . 5 setvar β„Ž
94cv 1540 . . . . . . 7 class 𝑠
10 c1st 7972 . . . . . . 7 class 1st
119, 10cfv 6543 . . . . . 6 class (1st β€˜π‘ )
12 c2nd 7973 . . . . . 6 class 2nd
1311, 12cfv 6543 . . . . 5 class (2nd β€˜(1st β€˜π‘ ))
14 va . . . . . 6 setvar π‘Ž
159, 12cfv 6543 . . . . . 6 class (2nd β€˜π‘ )
1611, 10cfv 6543 . . . . . . . 8 class (1st β€˜(1st β€˜π‘ ))
17 vz . . . . . . . . 9 setvar 𝑧
18 cmvrs 34455 . . . . . . . . . . . 12 class mVars
195, 18cfv 6543 . . . . . . . . . . 11 class (mVarsβ€˜π‘‘)
208cv 1540 . . . . . . . . . . . 12 class β„Ž
2114cv 1540 . . . . . . . . . . . . 13 class π‘Ž
2221csn 4628 . . . . . . . . . . . 12 class {π‘Ž}
2320, 22cun 3946 . . . . . . . . . . 11 class (β„Ž βˆͺ {π‘Ž})
2419, 23cima 5679 . . . . . . . . . 10 class ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž}))
2524cuni 4908 . . . . . . . . 9 class βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž}))
2617cv 1540 . . . . . . . . . 10 class 𝑧
2726, 26cxp 5674 . . . . . . . . 9 class (𝑧 Γ— 𝑧)
2817, 25, 27csb 3893 . . . . . . . 8 class ⦋βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž})) / π‘§β¦Œ(𝑧 Γ— 𝑧)
2916, 28cin 3947 . . . . . . 7 class ((1st β€˜(1st β€˜π‘ )) ∩ ⦋βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž})) / π‘§β¦Œ(𝑧 Γ— 𝑧))
3029, 20, 21cotp 4636 . . . . . 6 class ⟨((1st β€˜(1st β€˜π‘ )) ∩ ⦋βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž})) / π‘§β¦Œ(𝑧 Γ— 𝑧)), β„Ž, π‘ŽβŸ©
3114, 15, 30csb 3893 . . . . 5 class ⦋(2nd β€˜π‘ ) / π‘Žβ¦ŒβŸ¨((1st β€˜(1st β€˜π‘ )) ∩ ⦋βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž})) / π‘§β¦Œ(𝑧 Γ— 𝑧)), β„Ž, π‘ŽβŸ©
328, 13, 31csb 3893 . . . 4 class ⦋(2nd β€˜(1st β€˜π‘ )) / β„Žβ¦Œβ¦‹(2nd β€˜π‘ ) / π‘Žβ¦ŒβŸ¨((1st β€˜(1st β€˜π‘ )) ∩ ⦋βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž})) / π‘§β¦Œ(𝑧 Γ— 𝑧)), β„Ž, π‘ŽβŸ©
334, 7, 32cmpt 5231 . . 3 class (𝑠 ∈ (mPreStβ€˜π‘‘) ↦ ⦋(2nd β€˜(1st β€˜π‘ )) / β„Žβ¦Œβ¦‹(2nd β€˜π‘ ) / π‘Žβ¦ŒβŸ¨((1st β€˜(1st β€˜π‘ )) ∩ ⦋βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž})) / π‘§β¦Œ(𝑧 Γ— 𝑧)), β„Ž, π‘ŽβŸ©)
342, 3, 33cmpt 5231 . 2 class (𝑑 ∈ V ↦ (𝑠 ∈ (mPreStβ€˜π‘‘) ↦ ⦋(2nd β€˜(1st β€˜π‘ )) / β„Žβ¦Œβ¦‹(2nd β€˜π‘ ) / π‘Žβ¦ŒβŸ¨((1st β€˜(1st β€˜π‘ )) ∩ ⦋βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž})) / π‘§β¦Œ(𝑧 Γ— 𝑧)), β„Ž, π‘ŽβŸ©))
351, 34wceq 1541 1 wff mStRed = (𝑑 ∈ V ↦ (𝑠 ∈ (mPreStβ€˜π‘‘) ↦ ⦋(2nd β€˜(1st β€˜π‘ )) / β„Žβ¦Œβ¦‹(2nd β€˜π‘ ) / π‘Žβ¦ŒβŸ¨((1st β€˜(1st β€˜π‘ )) ∩ ⦋βˆͺ ((mVarsβ€˜π‘‘) β€œ (β„Ž βˆͺ {π‘Ž})) / π‘§β¦Œ(𝑧 Γ— 𝑧)), β„Ž, π‘ŽβŸ©))
Colors of variables: wff setvar class
This definition is referenced by:  msrfval  34523
  Copyright terms: Public domain W3C validator