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 sseldi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 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 sseldi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 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 )