Metamath Proof Explorer


Theorem msrval

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

Ref Expression
Hypotheses msrfval.v V = mVars T
msrfval.p P = mPreSt T
msrfval.r R = mStRed T
msrval.z Z = V H A
Assertion msrval D H A P R D H A = D Z × Z H A

Proof

Step Hyp Ref Expression
1 msrfval.v V = mVars T
2 msrfval.p P = mPreSt T
3 msrfval.r R = mStRed T
4 msrval.z Z = V H A
5 1 2 3 msrfval R = s P 2 nd 1 st s / h 2 nd s / a 1 st 1 st s V h a / z z × z h a
6 5 a1i D H A P R = s P 2 nd 1 st s / h 2 nd s / a 1 st 1 st s V h a / z z × z h a
7 fvexd D H A P s = D H A 2 nd 1 st s V
8 fvexd D H A P s = D H A h = 2 nd 1 st s 2 nd s V
9 simpllr D H A P s = D H A h = 2 nd 1 st s a = 2 nd s s = D H A
10 9 fveq2d D H A P s = D H A h = 2 nd 1 st s a = 2 nd s 1 st s = 1 st D H A
11 10 fveq2d D H A P s = D H A h = 2 nd 1 st s a = 2 nd s 1 st 1 st s = 1 st 1 st D H A
12 eqid mDV T = mDV T
13 eqid mEx T = mEx T
14 12 13 2 elmpst D H A P D mDV T D -1 = D H mEx T H Fin A mEx T
15 14 simp1bi D H A P D mDV T D -1 = D
16 15 simpld D H A P D mDV T
17 16 ad3antrrr D H A P s = D H A h = 2 nd 1 st s a = 2 nd s D mDV T
18 fvex mDV T V
19 18 ssex D mDV T D V
20 17 19 syl D H A P s = D H A h = 2 nd 1 st s a = 2 nd s D V
21 14 simp2bi D H A P H mEx T H Fin
22 21 simprd D H A P H Fin
23 22 ad3antrrr D H A P s = D H A h = 2 nd 1 st s a = 2 nd s H Fin
24 14 simp3bi D H A P A mEx T
25 24 ad3antrrr D H A P s = D H A h = 2 nd 1 st s a = 2 nd s A mEx T
26 ot1stg D V H Fin A mEx T 1 st 1 st D H A = D
27 20 23 25 26 syl3anc D H A P s = D H A h = 2 nd 1 st s a = 2 nd s 1 st 1 st D H A = D
28 11 27 eqtrd D H A P s = D H A h = 2 nd 1 st s a = 2 nd s 1 st 1 st s = D
29 1 fvexi V V
30 imaexg V V V h a V
31 29 30 ax-mp V h a V
32 31 uniex V h a V
33 32 a1i D H A P s = D H A h = 2 nd 1 st s a = 2 nd s V h a V
34 id z = V h a z = V h a
35 simplr D H A P s = D H A h = 2 nd 1 st s a = 2 nd s h = 2 nd 1 st s
36 10 fveq2d D H A P s = D H A h = 2 nd 1 st s a = 2 nd s 2 nd 1 st s = 2 nd 1 st D H A
37 ot2ndg D V H Fin A mEx T 2 nd 1 st D H A = H
38 20 23 25 37 syl3anc D H A P s = D H A h = 2 nd 1 st s a = 2 nd s 2 nd 1 st D H A = H
39 35 36 38 3eqtrd D H A P s = D H A h = 2 nd 1 st s a = 2 nd s h = H
40 simpr D H A P s = D H A h = 2 nd 1 st s a = 2 nd s a = 2 nd s
41 9 fveq2d D H A P s = D H A h = 2 nd 1 st s a = 2 nd s 2 nd s = 2 nd D H A
42 ot3rdg A mEx T 2 nd D H A = A
43 25 42 syl D H A P s = D H A h = 2 nd 1 st s a = 2 nd s 2 nd D H A = A
44 40 41 43 3eqtrd D H A P s = D H A h = 2 nd 1 st s a = 2 nd s a = A
45 44 sneqd D H A P s = D H A h = 2 nd 1 st s a = 2 nd s a = A
46 39 45 uneq12d D H A P s = D H A h = 2 nd 1 st s a = 2 nd s h a = H A
47 46 imaeq2d D H A P s = D H A h = 2 nd 1 st s a = 2 nd s V h a = V H A
48 47 unieqd D H A P s = D H A h = 2 nd 1 st s a = 2 nd s V h a = V H A
49 48 4 syl6eqr D H A P s = D H A h = 2 nd 1 st s a = 2 nd s V h a = Z
50 34 49 sylan9eqr D H A P s = D H A h = 2 nd 1 st s a = 2 nd s z = V h a z = Z
51 50 sqxpeqd D H A P s = D H A h = 2 nd 1 st s a = 2 nd s z = V h a z × z = Z × Z
52 33 51 csbied D H A P s = D H A h = 2 nd 1 st s a = 2 nd s V h a / z z × z = Z × Z
53 28 52 ineq12d D H A P s = D H A h = 2 nd 1 st s a = 2 nd s 1 st 1 st s V h a / z z × z = D Z × Z
54 53 39 44 oteq123d D H A P s = D H A h = 2 nd 1 st s a = 2 nd s 1 st 1 st s V h a / z z × z h a = D Z × Z H A
55 8 54 csbied D H A P s = D H A h = 2 nd 1 st s 2 nd s / a 1 st 1 st s V h a / z z × z h a = D Z × Z H A
56 7 55 csbied D H A P s = D H A 2 nd 1 st s / h 2 nd s / a 1 st 1 st s V h a / z z × z h a = D Z × Z H A
57 id D H A P D H A P
58 otex D Z × Z H A V
59 58 a1i D H A P D Z × Z H A V
60 6 56 57 59 fvmptd D H A P R D H A = D Z × Z H A