Metamath Proof Explorer

Theorem omsmon

Description: A constructed outer measure is monotone. Note in Example 1.5.2 of Bogachev p. 17. (Contributed by Thierry Arnoux, 15-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Hypotheses oms.m ⊢ 𝑀 = ( toOMeas ‘ 𝑅 )
oms.o ⊢ ( 𝜑 → 𝑄 ∈ 𝑉 )
oms.r ⊢ ( 𝜑 → 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
omsmon.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
omsmon.b ⊢ ( 𝜑 → 𝐵 ⊆ ∪ 𝑄 )
Assertion omsmon ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≤ ( 𝑀 ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 oms.m ⊢ 𝑀 = ( toOMeas ‘ 𝑅 )
2 oms.o ⊢ ( 𝜑 → 𝑄 ∈ 𝑉 )
3 oms.r ⊢ ( 𝜑 → 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
4 omsmon.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
5 omsmon.b ⊢ ( 𝜑 → 𝐵 ⊆ ∪ 𝑄 )
6 4 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 dom 𝑅 ) → 𝐴 ⊆ 𝐵 )
7 sstr2 ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 ⊆ ∪ 𝑧 → 𝐴 ⊆ ∪ 𝑧 ) )
8 6 7 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 dom 𝑅 ) → ( 𝐵 ⊆ ∪ 𝑧 → 𝐴 ⊆ ∪ 𝑧 ) )
9 8 anim1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 dom 𝑅 ) → ( ( 𝐵 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) → ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) ) )
10 9 ss2rabdv ⊢ ( 𝜑 → { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐵 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ⊆ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } )
11 resmpt ⊢ ( { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐵 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ⊆ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } → ( ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) ↾ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐵 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ) = ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐵 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) )
12 10 11 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) ↾ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐵 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ) = ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐵 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) )
13 resss ⊢ ( ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) ↾ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐵 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ) ⊆ ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) )
14 12 13 eqsstrrdi ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐵 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) ⊆ ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) )
15 rnss ⊢ ( ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐵 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) ⊆ ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) → ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐵 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) ⊆ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) )
16 14 15 syl ⊢ ( 𝜑 → ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐵 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) ⊆ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) )
17 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ) ∧ 𝑦 ∈ 𝑥 ) → 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
18 ssrab2 ⊢ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ⊆ 𝒫 dom 𝑅
19 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } )
20 18 19 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ 𝒫 dom 𝑅 )
21 elpwi ⊢ ( 𝑥 ∈ 𝒫 dom 𝑅 → 𝑥 ⊆ dom 𝑅 )
22 20 21 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ⊆ dom 𝑅 )
23 3 fdmd ⊢ ( 𝜑 → dom 𝑅 = 𝑄 )
24 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ) ∧ 𝑦 ∈ 𝑥 ) → dom 𝑅 = 𝑄 )
25 22 24 sseqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ⊆ 𝑄 )
26 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
27 25 26 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑄 )
28 17 27 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
29 28 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ) → ∀ 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
30 vex ⊢ 𝑥 ∈ V
31 nfcv ⊢ Ⅎ 𝑦 𝑥
32 31 esumcl ⊢ ( ( 𝑥 ∈ V ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
33 30 32 mpan ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) → Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
34 29 33 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ) → Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
35 34 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
36 eqid ⊢ ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) = ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) )
37 36 rnmptss ⊢ ( ∀ 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) → ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) ⊆ ( 0 [,] +∞ ) )
38 35 37 syl ⊢ ( 𝜑 → ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) ⊆ ( 0 [,] +∞ ) )
39 16 38 xrge0infssd ⊢ ( 𝜑 → inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) ≤ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐵 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) )
40 4 5 sstrd ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑄 )
41 omsfval ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 ⊆ ∪ 𝑄 ) → ( ( toOMeas ‘ 𝑅 ) ‘ 𝐴 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) )
42 2 3 40 41 syl3anc ⊢ ( 𝜑 → ( ( toOMeas ‘ 𝑅 ) ‘ 𝐴 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) )
43 omsfval ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐵 ⊆ ∪ 𝑄 ) → ( ( toOMeas ‘ 𝑅 ) ‘ 𝐵 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐵 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) )
44 2 3 5 43 syl3anc ⊢ ( 𝜑 → ( ( toOMeas ‘ 𝑅 ) ‘ 𝐵 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐵 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) )
45 39 42 44 3brtr4d ⊢ ( 𝜑 → ( ( toOMeas ‘ 𝑅 ) ‘ 𝐴 ) ≤ ( ( toOMeas ‘ 𝑅 ) ‘ 𝐵 ) )
46 1 fveq1i ⊢ ( 𝑀 ‘ 𝐴 ) = ( ( toOMeas ‘ 𝑅 ) ‘ 𝐴 )
47 1 fveq1i ⊢ ( 𝑀 ‘ 𝐵 ) = ( ( toOMeas ‘ 𝑅 ) ‘ 𝐵 )
48 45 46 47 3brtr4g ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≤ ( 𝑀 ‘ 𝐵 ) )