Metamath Proof Explorer


Theorem omsfval

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 QVR:Q0+∞AQtoOMeasRA=supranxz𝒫domR|Azzω*yxRy0+∞<

Proof

Step Hyp Ref Expression
1 simp2 QVR:Q0+∞AQR:Q0+∞
2 simp1 QVR:Q0+∞AQQV
3 1 2 fexd QVR:Q0+∞AQRV
4 omsval RVtoOMeasR=a𝒫domRsupranxz𝒫domR|azzω*yxRy0+∞<
5 3 4 syl QVR:Q0+∞AQtoOMeasR=a𝒫domRsupranxz𝒫domR|azzω*yxRy0+∞<
6 simpr QVR:Q0+∞AQa=Aa=A
7 6 sseq1d QVR:Q0+∞AQa=AazAz
8 7 anbi1d QVR:Q0+∞AQa=AazzωAzzω
9 8 rabbidv QVR:Q0+∞AQa=Az𝒫domR|azzω=z𝒫domR|Azzω
10 9 mpteq1d QVR:Q0+∞AQa=Axz𝒫domR|azzω*yxRy=xz𝒫domR|Azzω*yxRy
11 10 rneqd QVR:Q0+∞AQa=Aranxz𝒫domR|azzω*yxRy=ranxz𝒫domR|Azzω*yxRy
12 11 infeq1d QVR:Q0+∞AQa=Asupranxz𝒫domR|azzω*yxRy0+∞<=supranxz𝒫domR|Azzω*yxRy0+∞<
13 simp3 QVR:Q0+∞AQAQ
14 fdm R:Q0+∞domR=Q
15 14 3ad2ant2 QVR:Q0+∞AQdomR=Q
16 15 unieqd QVR:Q0+∞AQdomR=Q
17 13 16 sseqtrrd QVR:Q0+∞AQAdomR
18 2 uniexd QVR:Q0+∞AQQV
19 ssexg AQQVAV
20 13 18 19 syl2anc QVR:Q0+∞AQAV
21 elpwg AVA𝒫domRAdomR
22 20 21 syl QVR:Q0+∞AQA𝒫domRAdomR
23 17 22 mpbird QVR:Q0+∞AQA𝒫domR
24 xrltso <Or*
25 iccssxr 0+∞*
26 soss 0+∞*<Or*<Or0+∞
27 25 26 ax-mp <Or*<Or0+∞
28 24 27 mp1i QVR:Q0+∞AQ<Or0+∞
29 28 infexd QVR:Q0+∞AQsupranxz𝒫domR|Azzω*yxRy0+∞<V
30 5 12 23 29 fvmptd QVR:Q0+∞AQtoOMeasRA=supranxz𝒫domR|Azzω*yxRy0+∞<