Description: A truth holds almost everywhere. (Contributed by Thierry Arnoux, 20-Oct-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | truae.1 | |
|
truae.2 | |
||
truae.3 | |
||
Assertion | truae | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | truae.1 | |
|
2 | truae.2 | |
|
3 | truae.3 | |
|
4 | 3 | pm2.24d | |
5 | 4 | ralrimivw | |
6 | rabss | |
|
7 | 5 6 | sylibr | |
8 | ss0 | |
|
9 | 7 8 | syl | |
10 | 9 | fveq2d | |
11 | measbasedom | |
|
12 | measvnul | |
|
13 | 11 12 | sylbi | |
14 | 2 13 | syl | |
15 | 10 14 | eqtrd | |
16 | 1 | braew | |
17 | 2 16 | syl | |
18 | 15 17 | mpbird | |