Metamath Proof Explorer

Theorem omsf

Description: A constructed outer measure is a function. (Contributed by Thierry Arnoux, 17-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Assertion omsf ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) → ( toOMeas ‘ 𝑅 ) : 𝒫 ∪ dom 𝑅 ⟶ ( 0 [,] +∞ ) )

Proof

Step Hyp Ref Expression
1 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
2 xrltso ⊢ < Or ℝ*
3 soss ⊢ ( ( 0 [,] +∞ ) ⊆ ℝ* → ( < Or ℝ* → < Or ( 0 [,] +∞ ) ) )
4 1 2 3 mp2 ⊢ < Or ( 0 [,] +∞ )
5 4 a1i ⊢ ( ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑅 ) → < Or ( 0 [,] +∞ ) )
6 omscl ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑅 ) → ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) ⊆ ( 0 [,] +∞ ) )
7 6 3expa ⊢ ( ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑅 ) → ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) ⊆ ( 0 [,] +∞ ) )
8 xrge0infss ⊢ ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) ⊆ ( 0 [,] +∞ ) → ∃ 𝑡 ∈ ( 0 [,] +∞ ) ( ∀ 𝑤 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) ¬ 𝑤 < 𝑡 ∧ ∀ 𝑤 ∈ ( 0 [,] +∞ ) ( 𝑡 < 𝑤 → ∃ 𝑠 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) 𝑠 < 𝑤 ) ) )
9 7 8 syl ⊢ ( ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑅 ) → ∃ 𝑡 ∈ ( 0 [,] +∞ ) ( ∀ 𝑤 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) ¬ 𝑤 < 𝑡 ∧ ∀ 𝑤 ∈ ( 0 [,] +∞ ) ( 𝑡 < 𝑤 → ∃ 𝑠 ∈ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) 𝑠 < 𝑤 ) ) )
10 5 9 infcl ⊢ ( ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑅 ) → inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) ∈ ( 0 [,] +∞ ) )
11 fex ⊢ ( ( 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝑄 ∈ 𝑉 ) → 𝑅 ∈ V )
12 11 ancoms ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) → 𝑅 ∈ V )
13 omsval ⊢ ( 𝑅 ∈ V → ( toOMeas ‘ 𝑅 ) = ( 𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) ) )
14 12 13 syl ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) → ( toOMeas ‘ 𝑅 ) = ( 𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) ) )
15 simpll ⊢ ( ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑅 ) → 𝑄 ∈ 𝑉 )
16 simplr ⊢ ( ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑅 ) → 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
17 simpr ⊢ ( ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑅 ) → 𝑎 ∈ 𝒫 ∪ dom 𝑅 )
18 fdm ⊢ ( 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) → dom 𝑅 = 𝑄 )
19 18 unieqd ⊢ ( 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) → ∪ dom 𝑅 = ∪ 𝑄 )
20 19 pweqd ⊢ ( 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) → 𝒫 ∪ dom 𝑅 = 𝒫 ∪ 𝑄 )
21 20 ad2antlr ⊢ ( ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑅 ) → 𝒫 ∪ dom 𝑅 = 𝒫 ∪ 𝑄 )
22 17 21 eleqtrd ⊢ ( ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑅 ) → 𝑎 ∈ 𝒫 ∪ 𝑄 )
23 elpwi ⊢ ( 𝑎 ∈ 𝒫 ∪ 𝑄 → 𝑎 ⊆ ∪ 𝑄 )
24 22 23 syl ⊢ ( ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑅 ) → 𝑎 ⊆ ∪ 𝑄 )
25 omsfval ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝑎 ⊆ ∪ 𝑄 ) → ( ( toOMeas ‘ 𝑅 ) ‘ 𝑎 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) )
26 15 16 24 25 syl3anc ⊢ ( ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑅 ) → ( ( toOMeas ‘ 𝑅 ) ‘ 𝑎 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) )
27 26 10 eqeltrd ⊢ ( ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑅 ) → ( ( toOMeas ‘ 𝑅 ) ‘ 𝑎 ) ∈ ( 0 [,] +∞ ) )
28 10 14 27 fmpt2d ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ) → ( toOMeas ‘ 𝑅 ) : 𝒫 ∪ dom 𝑅 ⟶ ( 0 [,] +∞ ) )