Step | Hyp | Ref
| Expression |
1 | | msrfval.v |
. . . 4
mVars |
2 | | msrfval.p |
. . . 4
mPreSt |
3 | | msrfval.r |
. . . 4
mStRed |
4 | 1, 2, 3 | msrfval 31434 |
. . 3
|
5 | 4 | a1i 11 |
. 2
|
6 | | fvexd 6203 |
. . 3
|
7 | | fvexd 6203 |
. . . 4
|
8 | | simpllr 799 |
. . . . . . . . 9
|
9 | 8 | fveq2d 6195 |
. . . . . . . 8
|
10 | 9 | fveq2d 6195 |
. . . . . . 7
|
11 | | eqid 2622 |
. . . . . . . . . . . . 13
mDV mDV |
12 | | eqid 2622 |
. . . . . . . . . . . . 13
mEx mEx |
13 | 11, 12, 2 | elmpst 31433 |
. . . . . . . . . . . 12
mDV
mEx
mEx |
14 | 13 | simp1bi 1076 |
. . . . . . . . . . 11
mDV
|
15 | 14 | simpld 475 |
. . . . . . . . . 10
mDV |
16 | 15 | ad3antrrr 766 |
. . . . . . . . 9
mDV |
17 | | fvex 6201 |
. . . . . . . . . 10
mDV |
18 | 17 | ssex 4802 |
. . . . . . . . 9
mDV
|
19 | 16, 18 | syl 17 |
. . . . . . . 8
|
20 | 13 | simp2bi 1077 |
. . . . . . . . . 10
mEx |
21 | 20 | simprd 479 |
. . . . . . . . 9
|
22 | 21 | ad3antrrr 766 |
. . . . . . . 8
|
23 | 13 | simp3bi 1078 |
. . . . . . . . 9
mEx |
24 | 23 | ad3antrrr 766 |
. . . . . . . 8
mEx |
25 | | ot1stg 7182 |
. . . . . . . 8
mEx
|
26 | 19, 22, 24, 25 | syl3anc 1326 |
. . . . . . 7
|
27 | 10, 26 | eqtrd 2656 |
. . . . . 6
|
28 | | fvex 6201 |
. . . . . . . . . . 11
mVars |
29 | 1, 28 | eqeltri 2697 |
. . . . . . . . . 10
|
30 | | imaexg 7103 |
. . . . . . . . . 10
|
31 | 29, 30 | ax-mp 5 |
. . . . . . . . 9
|
32 | 31 | uniex 6953 |
. . . . . . . 8
|
33 | 32 | a1i 11 |
. . . . . . 7
|
34 | | id 22 |
. . . . . . . . 9
|
35 | | simplr 792 |
. . . . . . . . . . . . . 14
|
36 | 9 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
37 | | ot2ndg 7183 |
. . . . . . . . . . . . . . 15
mEx
|
38 | 19, 22, 24, 37 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
39 | 35, 36, 38 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
|
40 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
41 | 8 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
42 | | ot3rdg 7184 |
. . . . . . . . . . . . . . . 16
mEx
|
43 | 24, 42 | syl 17 |
. . . . . . . . . . . . . . 15
|
44 | 40, 41, 43 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
|
45 | 44 | sneqd 4189 |
. . . . . . . . . . . . 13
|
46 | 39, 45 | uneq12d 3768 |
. . . . . . . . . . . 12
|
47 | 46 | imaeq2d 5466 |
. . . . . . . . . . 11
|
48 | 47 | unieqd 4446 |
. . . . . . . . . 10
|
49 | | msrval.z |
. . . . . . . . . 10
|
50 | 48, 49 | syl6eqr 2674 |
. . . . . . . . 9
|
51 | 34, 50 | sylan9eqr 2678 |
. . . . . . . 8
|
52 | 51 | sqxpeqd 5141 |
. . . . . . 7
|
53 | 33, 52 | csbied 3560 |
. . . . . 6
|
54 | 27, 53 | ineq12d 3815 |
. . . . 5
|
55 | 54, 39, 44 | oteq123d 4417 |
. . . 4
|
56 | 7, 55 | csbied 3560 |
. . 3
|
57 | 6, 56 | csbied 3560 |
. 2
|
58 | | id 22 |
. 2
|
59 | | otex 4933 |
. . 3
|
60 | 59 | a1i 11 |
. 2
|
61 | 5, 57, 58, 60 | fvmptd 6288 |
1
|