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 𝑀 = ( toOMeas ‘ 𝑅 )
oms.o ( 𝜑𝑄𝑉 )
oms.r ( 𝜑𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
oms.d ( 𝜑 → ∅ ∈ dom 𝑅 )
oms.0 ( 𝜑 → ( 𝑅 ‘ ∅ ) = 0 )
Assertion oms0 ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )

Proof

Step Hyp Ref Expression
1 oms.m 𝑀 = ( toOMeas ‘ 𝑅 )
2 oms.o ( 𝜑𝑄𝑉 )
3 oms.r ( 𝜑𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
4 oms.d ( 𝜑 → ∅ ∈ dom 𝑅 )
5 oms.0 ( 𝜑 → ( 𝑅 ‘ ∅ ) = 0 )
6 1 fveq1i ( 𝑀 ‘ ∅ ) = ( ( toOMeas ‘ 𝑅 ) ‘ ∅ )
7 0ss ∅ ⊆ dom 𝑅
8 3 fdmd ( 𝜑 → dom 𝑅 = 𝑄 )
9 8 unieqd ( 𝜑 dom 𝑅 = 𝑄 )
10 7 9 sseqtrid ( 𝜑 → ∅ ⊆ 𝑄 )
11 omsfval ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ ∅ ⊆ 𝑄 ) → ( ( toOMeas ‘ 𝑅 ) ‘ ∅ ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) , ( 0 [,] +∞ ) , < ) )
12 2 3 10 11 syl3anc ( 𝜑 → ( ( toOMeas ‘ 𝑅 ) ‘ ∅ ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) , ( 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 𝑅 )
21 p0ex { ∅ } ∈ V
22 21 elpw ( { ∅ } ∈ 𝒫 dom 𝑅 ↔ { ∅ } ⊆ dom 𝑅 )
23 20 22 sylibr ( 𝜑 → { ∅ } ∈ 𝒫 dom 𝑅 )
24 0ss ∅ ⊆ { ∅ }
25 0ex ∅ ∈ V
26 snct ( ∅ ∈ V → { ∅ } ≼ ω )
27 25 26 ax-mp { ∅ } ≼ ω
28 24 27 pm3.2i ( ∅ ⊆ { ∅ } ∧ { ∅ } ≼ ω )
29 23 28 jctir ( 𝜑 → ( { ∅ } ∈ 𝒫 dom 𝑅 ∧ ( ∅ ⊆ { ∅ } ∧ { ∅ } ≼ ω ) ) )
30 unieq ( 𝑧 = { ∅ } → 𝑧 = { ∅ } )
31 30 sseq2d ( 𝑧 = { ∅ } → ( ∅ ⊆ 𝑧 ↔ ∅ ⊆ { ∅ } ) )
32 breq1 ( 𝑧 = { ∅ } → ( 𝑧 ≼ ω ↔ { ∅ } ≼ ω ) )
33 31 32 anbi12d ( 𝑧 = { ∅ } → ( ( ∅ ⊆ 𝑧𝑧 ≼ ω ) ↔ ( ∅ ⊆ { ∅ } ∧ { ∅ } ≼ ω ) ) )
34 33 elrab ( { ∅ } ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↔ ( { ∅ } ∈ 𝒫 dom 𝑅 ∧ ( ∅ ⊆ { ∅ } ∧ { ∅ } ≼ ω ) ) )
35 29 34 sylibr ( 𝜑 → { ∅ } ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } )
36 simpr ( ( 𝜑𝑦 = ∅ ) → 𝑦 = ∅ )
37 36 fveq2d ( ( 𝜑𝑦 = ∅ ) → ( 𝑅𝑦 ) = ( 𝑅 ‘ ∅ ) )
38 5 adantr ( ( 𝜑𝑦 = ∅ ) → ( 𝑅 ‘ ∅ ) = 0 )
39 37 38 eqtrd ( ( 𝜑𝑦 = ∅ ) → ( 𝑅𝑦 ) = 0 )
40 39 4 19 esumsn ( 𝜑 → Σ* 𝑦 ∈ { ∅ } ( 𝑅𝑦 ) = 0 )
41 40 eqcomd ( 𝜑 → 0 = Σ* 𝑦 ∈ { ∅ } ( 𝑅𝑦 ) )
42 esumeq1 ( 𝑥 = { ∅ } → Σ* 𝑦𝑥 ( 𝑅𝑦 ) = Σ* 𝑦 ∈ { ∅ } ( 𝑅𝑦 ) )
43 42 rspceeqv ( ( { ∅ } ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ∧ 0 = Σ* 𝑦 ∈ { ∅ } ( 𝑅𝑦 ) ) → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } 0 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) )
44 35 41 43 syl2anc ( 𝜑 → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } 0 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) )
45 0xr 0 ∈ ℝ*
46 eqid ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) = ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) )
47 46 elrnmpt ( 0 ∈ ℝ* → ( 0 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ↔ ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } 0 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) )
48 45 47 ax-mp ( 0 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ↔ ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } 0 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) )
49 44 48 sylibr ( 𝜑 → 0 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) )
50 nfv 𝑥 𝜑
51 nfmpt1 𝑥 ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) )
52 51 nfrn 𝑥 ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) )
53 52 nfcri 𝑥 𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) )
54 50 53 nfan 𝑥 ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) )
55 simpr ( ( ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ) ∧ 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) → 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) )
56 vex 𝑥 ∈ V
57 nfv 𝑦 𝜑
58 nfcv 𝑦 { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) }
59 nfcv 𝑦 𝑥
60 59 nfesum1 𝑦 Σ* 𝑦𝑥 ( 𝑅𝑦 )
61 58 60 nfmpt 𝑦 ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) )
62 61 nfrn 𝑦 ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) )
63 62 nfcri 𝑦 𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) )
64 57 63 nfan 𝑦 ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) )
65 nfv 𝑦 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) }
66 64 65 nfan 𝑦 ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } )
67 60 nfeq2 𝑦 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 )
68 66 67 nfan 𝑦 ( ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ) ∧ 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) )
69 3 ad4antr ( ( ( ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ) ∧ 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ∧ 𝑦𝑥 ) → 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
70 ssrab2 { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ⊆ 𝒫 dom 𝑅
71 simpllr ( ( ( ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ) ∧ 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ∧ 𝑦𝑥 ) → 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } )
72 70 71 sselid ( ( ( ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ) ∧ 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ∧ 𝑦𝑥 ) → 𝑥 ∈ 𝒫 dom 𝑅 )
73 8 pweqd ( 𝜑 → 𝒫 dom 𝑅 = 𝒫 𝑄 )
74 73 ad4antr ( ( ( ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ) ∧ 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ∧ 𝑦𝑥 ) → 𝒫 dom 𝑅 = 𝒫 𝑄 )
75 72 74 eleqtrd ( ( ( ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ) ∧ 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ∧ 𝑦𝑥 ) → 𝑥 ∈ 𝒫 𝑄 )
76 75 elpwid ( ( ( ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ) ∧ 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ∧ 𝑦𝑥 ) → 𝑥𝑄 )
77 simpr ( ( ( ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ) ∧ 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ∧ 𝑦𝑥 ) → 𝑦𝑥 )
78 76 77 sseldd ( ( ( ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ) ∧ 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ∧ 𝑦𝑥 ) → 𝑦𝑄 )
79 69 78 ffvelrnd ( ( ( ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ) ∧ 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ∧ 𝑦𝑥 ) → ( 𝑅𝑦 ) ∈ ( 0 [,] +∞ ) )
80 79 ex ( ( ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ) ∧ 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) → ( 𝑦𝑥 → ( 𝑅𝑦 ) ∈ ( 0 [,] +∞ ) ) )
81 68 80 ralrimi ( ( ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ) ∧ 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) → ∀ 𝑦𝑥 ( 𝑅𝑦 ) ∈ ( 0 [,] +∞ ) )
82 59 esumcl ( ( 𝑥 ∈ V ∧ ∀ 𝑦𝑥 ( 𝑅𝑦 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑦𝑥 ( 𝑅𝑦 ) ∈ ( 0 [,] +∞ ) )
83 56 81 82 sylancr ( ( ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ) ∧ 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) → Σ* 𝑦𝑥 ( 𝑅𝑦 ) ∈ ( 0 [,] +∞ ) )
84 55 83 eqeltrd ( ( ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ) ∧ 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) → 𝑎 ∈ ( 0 [,] +∞ ) )
85 vex 𝑎 ∈ V
86 46 elrnmpt ( 𝑎 ∈ V → ( 𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ↔ ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) )
87 85 86 ax-mp ( 𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ↔ ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) )
88 87 biimpi ( 𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) )
89 88 adantl ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) → ∃ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } 𝑎 = Σ* 𝑦𝑥 ( 𝑅𝑦 ) )
90 54 84 89 r19.29af ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) → 𝑎 ∈ ( 0 [,] +∞ ) )
91 pnfxr +∞ ∈ ℝ*
92 iccgelb ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ*𝑎 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝑎 )
93 45 91 92 mp3an12 ( 𝑎 ∈ ( 0 [,] +∞ ) → 0 ≤ 𝑎 )
94 90 93 syl ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) → 0 ≤ 𝑎 )
95 13 90 sselid ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) → 𝑎 ∈ ℝ* )
96 xrlenlt ( ( 0 ∈ ℝ*𝑎 ∈ ℝ* ) → ( 0 ≤ 𝑎 ↔ ¬ 𝑎 < 0 ) )
97 96 bicomd ( ( 0 ∈ ℝ*𝑎 ∈ ℝ* ) → ( ¬ 𝑎 < 0 ↔ 0 ≤ 𝑎 ) )
98 45 95 97 sylancr ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) → ( ¬ 𝑎 < 0 ↔ 0 ≤ 𝑎 ) )
99 94 98 mpbird ( ( 𝜑𝑎 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) ) → ¬ 𝑎 < 0 )
100 17 19 49 99 infmin ( 𝜑 → inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( ∅ ⊆ 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) , ( 0 [,] +∞ ) , < ) = 0 )
101 12 100 eqtrd ( 𝜑 → ( ( toOMeas ‘ 𝑅 ) ‘ ∅ ) = 0 )
102 6 101 syl5eq ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )