Metamath Proof Explorer

Theorem omsval

Description: Value of the function mapping a content function to the corresponding outer measure. (Contributed by Thierry Arnoux, 15-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Assertion omsval ( 𝑅 ∈ V → ( toOMeas ‘ 𝑅 ) = ( 𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) ) )

Proof

Step Hyp Ref Expression
1 df-oms ⊢ toOMeas = ( 𝑟 ∈ V ↦ ( 𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑟 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑟 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) ) )
2 dmeq ⊢ ( 𝑟 = 𝑅 → dom 𝑟 = dom 𝑅 )
3 2 unieqd ⊢ ( 𝑟 = 𝑅 → ∪ dom 𝑟 = ∪ dom 𝑅 )
4 3 pweqd ⊢ ( 𝑟 = 𝑅 → 𝒫 ∪ dom 𝑟 = 𝒫 ∪ dom 𝑅 )
5 2 pweqd ⊢ ( 𝑟 = 𝑅 → 𝒫 dom 𝑟 = 𝒫 dom 𝑅 )
6 rabeq ⊢ ( 𝒫 dom 𝑟 = 𝒫 dom 𝑅 → { 𝑧 ∈ 𝒫 dom 𝑟 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } = { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } )
7 5 6 syl ⊢ ( 𝑟 = 𝑅 → { 𝑧 ∈ 𝒫 dom 𝑟 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } = { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } )
8 simpl ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑦 ∈ 𝑥 ) → 𝑟 = 𝑅 )
9 8 fveq1d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑦 ∈ 𝑥 ) → ( 𝑟 ‘ 𝑦 ) = ( 𝑅 ‘ 𝑦 ) )
10 9 esumeq2dv ⊢ ( 𝑟 = 𝑅 → Σ* 𝑦 ∈ 𝑥 ( 𝑟 ‘ 𝑦 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) )
11 7 10 mpteq12dv ⊢ ( 𝑟 = 𝑅 → ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑟 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑟 ‘ 𝑦 ) ) = ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) )
12 11 rneqd ⊢ ( 𝑟 = 𝑅 → ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑟 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑟 ‘ 𝑦 ) ) = ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) )
13 12 infeq1d ⊢ ( 𝑟 = 𝑅 → inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑟 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑟 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) = inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) )
14 4 13 mpteq12dv ⊢ ( 𝑟 = 𝑅 → ( 𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑟 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑟 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) ) = ( 𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) ) )
15 id ⊢ ( 𝑅 ∈ V → 𝑅 ∈ V )
16 dmexg ⊢ ( 𝑅 ∈ V → dom 𝑅 ∈ V )
17 uniexg ⊢ ( dom 𝑅 ∈ V → ∪ dom 𝑅 ∈ V )
18 pwexg ⊢ ( ∪ dom 𝑅 ∈ V → 𝒫 ∪ dom 𝑅 ∈ V )
19 mptexg ⊢ ( 𝒫 ∪ dom 𝑅 ∈ V → ( 𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) ) ∈ V )
20 16 17 18 19 4syl ⊢ ( 𝑅 ∈ V → ( 𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) ) ∈ V )
21 1 14 15 20 fvmptd3 ⊢ ( 𝑅 ∈ V → ( toOMeas ‘ 𝑅 ) = ( 𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑅 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑅 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) ) )