Metamath Proof Explorer


Theorem omsfval

Description: Value of the outer measure evaluated for a given set A . (Contributed by Thierry Arnoux, 15-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Assertion omsfval ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → ( ( toOMeas ‘ 𝑅 ) ‘ 𝐴 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) , ( 0 [,] +∞ ) , < ) )

Proof

Step Hyp Ref Expression
1 simp2 ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) )
2 simp1 ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → 𝑄𝑉 )
3 1 2 fexd ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → 𝑅 ∈ V )
4 omsval ( 𝑅 ∈ V → ( toOMeas ‘ 𝑅 ) = ( 𝑎 ∈ 𝒫 dom 𝑅 ↦ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) , ( 0 [,] +∞ ) , < ) ) )
5 3 4 syl ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → ( toOMeas ‘ 𝑅 ) = ( 𝑎 ∈ 𝒫 dom 𝑅 ↦ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) , ( 0 [,] +∞ ) , < ) ) )
6 simpr ( ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) ∧ 𝑎 = 𝐴 ) → 𝑎 = 𝐴 )
7 6 sseq1d ( ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) ∧ 𝑎 = 𝐴 ) → ( 𝑎 𝑧𝐴 𝑧 ) )
8 7 anbi1d ( ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) ∧ 𝑎 = 𝐴 ) → ( ( 𝑎 𝑧𝑧 ≼ ω ) ↔ ( 𝐴 𝑧𝑧 ≼ ω ) ) )
9 8 rabbidv ( ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) ∧ 𝑎 = 𝐴 ) → { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 𝑧𝑧 ≼ ω ) } = { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } )
10 9 mpteq1d ( ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) ∧ 𝑎 = 𝐴 ) → ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) = ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) )
11 10 rneqd ( ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) ∧ 𝑎 = 𝐴 ) → ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) = ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) )
12 11 infeq1d ( ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) ∧ 𝑎 = 𝐴 ) → inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) , ( 0 [,] +∞ ) , < ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) , ( 0 [,] +∞ ) , < ) )
13 simp3 ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → 𝐴 𝑄 )
14 fdm ( 𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) → dom 𝑅 = 𝑄 )
15 14 3ad2ant2 ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → dom 𝑅 = 𝑄 )
16 15 unieqd ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → dom 𝑅 = 𝑄 )
17 13 16 sseqtrrd ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → 𝐴 dom 𝑅 )
18 2 uniexd ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → 𝑄 ∈ V )
19 ssexg ( ( 𝐴 𝑄 𝑄 ∈ V ) → 𝐴 ∈ V )
20 13 18 19 syl2anc ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → 𝐴 ∈ V )
21 elpwg ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 dom 𝑅𝐴 dom 𝑅 ) )
22 20 21 syl ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → ( 𝐴 ∈ 𝒫 dom 𝑅𝐴 dom 𝑅 ) )
23 17 22 mpbird ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → 𝐴 ∈ 𝒫 dom 𝑅 )
24 xrltso < Or ℝ*
25 iccssxr ( 0 [,] +∞ ) ⊆ ℝ*
26 soss ( ( 0 [,] +∞ ) ⊆ ℝ* → ( < Or ℝ* → < Or ( 0 [,] +∞ ) ) )
27 25 26 ax-mp ( < Or ℝ* → < Or ( 0 [,] +∞ ) )
28 24 27 mp1i ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → < Or ( 0 [,] +∞ ) )
29 28 infexd ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) , ( 0 [,] +∞ ) , < ) ∈ V )
30 5 12 23 29 fvmptd ( ( 𝑄𝑉𝑅 : 𝑄 ⟶ ( 0 [,] +∞ ) ∧ 𝐴 𝑄 ) → ( ( toOMeas ‘ 𝑅 ) ‘ 𝐴 ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝐴 𝑧𝑧 ≼ ω ) } ↦ Σ* 𝑦𝑥 ( 𝑅𝑦 ) ) , ( 0 [,] +∞ ) , < ) )