Metamath Proof Explorer


Definition df-msr

Description: Define the reduct of a pre-statement. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-msr mStRed = t V s mPreSt t 2 nd 1 st s / h 2 nd s / a 1 st 1 st s mVars t h a / z z × z h a

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmsr class mStRed
1 vt setvar t
2 cvv class V
3 vs setvar s
4 cmpst class mPreSt
5 1 cv setvar t
6 5 4 cfv class mPreSt t
7 c2nd class 2 nd
8 c1st class 1 st
9 3 cv setvar s
10 9 8 cfv class 1 st s
11 10 7 cfv class 2 nd 1 st s
12 vh setvar h
13 9 7 cfv class 2 nd s
14 va setvar a
15 10 8 cfv class 1 st 1 st s
16 cmvrs class mVars
17 5 16 cfv class mVars t
18 12 cv setvar h
19 14 cv setvar a
20 19 csn class a
21 18 20 cun class h a
22 17 21 cima class mVars t h a
23 22 cuni class mVars t h a
24 vz setvar z
25 24 cv setvar z
26 25 25 cxp class z × z
27 24 23 26 csb class mVars t h a / z z × z
28 15 27 cin class 1 st 1 st s mVars t h a / z z × z
29 28 18 19 cotp class 1 st 1 st s mVars t h a / z z × z h a
30 14 13 29 csb class 2 nd s / a 1 st 1 st s mVars t h a / z z × z h a
31 12 11 30 csb class 2 nd 1 st s / h 2 nd s / a 1 st 1 st s mVars t h a / z z × z h a
32 3 6 31 cmpt class s mPreSt t 2 nd 1 st s / h 2 nd s / a 1 st 1 st s mVars t h a / z z × z h a
33 1 2 32 cmpt class t V s mPreSt t 2 nd 1 st s / h 2 nd s / a 1 st 1 st s mVars t h a / z z × z h a
34 0 33 wceq wff mStRed = t V s mPreSt t 2 nd 1 st s / h 2 nd s / a 1 st 1 st s mVars t h a / z z × z h a