Metamath Proof Explorer


Theorem oms0

Description: A constructed outer measure evaluates to zero for the empty set. (Contributed by Thierry Arnoux, 15-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Hypotheses oms.m M = toOMeas R
oms.o φ Q V
oms.r φ R : Q 0 +∞
oms.d φ dom R
oms.0 φ R = 0
Assertion oms0 φ M = 0

Proof

Step Hyp Ref Expression
1 oms.m M = toOMeas R
2 oms.o φ Q V
3 oms.r φ R : Q 0 +∞
4 oms.d φ dom R
5 oms.0 φ R = 0
6 1 fveq1i M = toOMeas R
7 0ss dom R
8 3 fdmd φ dom R = Q
9 8 unieqd φ dom R = Q
10 7 9 sseqtrid φ Q
11 omsfval Q V R : Q 0 +∞ Q toOMeas R = sup ran x z 𝒫 dom R | z z ω * y x R y 0 +∞ <
12 2 3 10 11 syl3anc φ toOMeas R = sup ran x z 𝒫 dom R | z z ω * y x R y 0 +∞ <
13 iccssxr 0 +∞ *
14 xrltso < Or *
15 soss 0 +∞ * < Or * < Or 0 +∞
16 13 14 15 mp2 < Or 0 +∞
17 16 a1i φ < Or 0 +∞
18 0e0iccpnf 0 0 +∞
19 18 a1i φ 0 0 +∞
20 4 snssd φ dom R
21 p0ex V
22 21 elpw 𝒫 dom R dom R
23 20 22 sylibr φ 𝒫 dom R
24 0ss
25 0ex V
26 snct V ω
27 25 26 ax-mp ω
28 24 27 pm3.2i ω
29 23 28 jctir φ 𝒫 dom R ω
30 unieq z = z =
31 30 sseq2d z = z
32 breq1 z = z ω ω
33 31 32 anbi12d z = z z ω ω
34 33 elrab z 𝒫 dom R | z z ω 𝒫 dom R ω
35 29 34 sylibr φ z 𝒫 dom R | z z ω
36 simpr φ y = y =
37 36 fveq2d φ y = R y = R
38 5 adantr φ y = R = 0
39 37 38 eqtrd φ y = R y = 0
40 39 4 19 esumsn φ * y R y = 0
41 40 eqcomd φ 0 = * y R y
42 esumeq1 x = * y x R y = * y R y
43 42 rspceeqv z 𝒫 dom R | z z ω 0 = * y R y x z 𝒫 dom R | z z ω 0 = * y x R y
44 35 41 43 syl2anc φ x z 𝒫 dom R | z z ω 0 = * y x R y
45 0xr 0 *
46 eqid x z 𝒫 dom R | z z ω * y x R y = x z 𝒫 dom R | z z ω * y x R y
47 46 elrnmpt 0 * 0 ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω 0 = * y x R y
48 45 47 ax-mp 0 ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω 0 = * y x R y
49 44 48 sylibr φ 0 ran x z 𝒫 dom R | z z ω * y x R y
50 nfv x φ
51 nfmpt1 _ x x z 𝒫 dom R | z z ω * y x R y
52 51 nfrn _ x ran x z 𝒫 dom R | z z ω * y x R y
53 52 nfcri x a ran x z 𝒫 dom R | z z ω * y x R y
54 50 53 nfan x φ a ran x z 𝒫 dom R | z z ω * y x R y
55 simpr φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y a = * y x R y
56 vex x V
57 nfv y φ
58 nfcv _ y z 𝒫 dom R | z z ω
59 nfcv _ y x
60 59 nfesum1 _ y * y x R y
61 58 60 nfmpt _ y x z 𝒫 dom R | z z ω * y x R y
62 61 nfrn _ y ran x z 𝒫 dom R | z z ω * y x R y
63 62 nfcri y a ran x z 𝒫 dom R | z z ω * y x R y
64 57 63 nfan y φ a ran x z 𝒫 dom R | z z ω * y x R y
65 nfv y x z 𝒫 dom R | z z ω
66 64 65 nfan y φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω
67 60 nfeq2 y a = * y x R y
68 66 67 nfan y φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y
69 3 ad4antr φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y y x R : Q 0 +∞
70 ssrab2 z 𝒫 dom R | z z ω 𝒫 dom R
71 simpllr φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y y x x z 𝒫 dom R | z z ω
72 70 71 sselid φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y y x x 𝒫 dom R
73 8 pweqd φ 𝒫 dom R = 𝒫 Q
74 73 ad4antr φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y y x 𝒫 dom R = 𝒫 Q
75 72 74 eleqtrd φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y y x x 𝒫 Q
76 75 elpwid φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y y x x Q
77 simpr φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y y x y x
78 76 77 sseldd φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y y x y Q
79 69 78 ffvelrnd φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y y x R y 0 +∞
80 79 ex φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y y x R y 0 +∞
81 68 80 ralrimi φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y y x R y 0 +∞
82 59 esumcl x V y x R y 0 +∞ * y x R y 0 +∞
83 56 81 82 sylancr φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y * y x R y 0 +∞
84 55 83 eqeltrd φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y a 0 +∞
85 vex a V
86 46 elrnmpt a V a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y
87 85 86 ax-mp a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y
88 87 biimpi a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y
89 88 adantl φ a ran x z 𝒫 dom R | z z ω * y x R y x z 𝒫 dom R | z z ω a = * y x R y
90 54 84 89 r19.29af φ a ran x z 𝒫 dom R | z z ω * y x R y a 0 +∞
91 pnfxr +∞ *
92 iccgelb 0 * +∞ * a 0 +∞ 0 a
93 45 91 92 mp3an12 a 0 +∞ 0 a
94 90 93 syl φ a ran x z 𝒫 dom R | z z ω * y x R y 0 a
95 13 90 sselid φ a ran x z 𝒫 dom R | z z ω * y x R y a *
96 xrlenlt 0 * a * 0 a ¬ a < 0
97 96 bicomd 0 * a * ¬ a < 0 0 a
98 45 95 97 sylancr φ a ran x z 𝒫 dom R | z z ω * y x R y ¬ a < 0 0 a
99 94 98 mpbird φ a ran x z 𝒫 dom R | z z ω * y x R y ¬ a < 0
100 17 19 49 99 infmin φ sup ran x z 𝒫 dom R | z z ω * y x R y 0 +∞ < = 0
101 12 100 eqtrd φ toOMeas R = 0
102 6 101 syl5eq φ M = 0