Description: Value of the outer measure evaluated for a given set A . (Contributed by Thierry Arnoux, 15-Sep-2019) (Revised by AV, 4-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | omsfval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2 | |
|
2 | simp1 | |
|
3 | 1 2 | fexd | |
4 | omsval | |
|
5 | 3 4 | syl | |
6 | simpr | |
|
7 | 6 | sseq1d | |
8 | 7 | anbi1d | |
9 | 8 | rabbidv | |
10 | 9 | mpteq1d | |
11 | 10 | rneqd | |
12 | 11 | infeq1d | |
13 | simp3 | |
|
14 | fdm | |
|
15 | 14 | 3ad2ant2 | |
16 | 15 | unieqd | |
17 | 13 16 | sseqtrrd | |
18 | 2 | uniexd | |
19 | ssexg | |
|
20 | 13 18 19 | syl2anc | |
21 | elpwg | |
|
22 | 20 21 | syl | |
23 | 17 22 | mpbird | |
24 | xrltso | |
|
25 | iccssxr | |
|
26 | soss | |
|
27 | 25 26 | ax-mp | |
28 | 24 27 | mp1i | |
29 | 28 | infexd | |
30 | 5 12 23 29 | fvmptd | |