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 ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q → toOMeas ⁡ R ⁡ A = inf ran ⁡ x ∈ z ∈ 𝒫 dom ⁡ R | A ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x R ⁡ y 0 +∞ <

Proof

Step Hyp Ref Expression
1 simp2 ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q → R : Q ⟶ 0 +∞
2 simp1 ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q → Q ∈ V
3 1 2 fexd ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q → R ∈ V
4 omsval ⊢ R ∈ V → toOMeas ⁡ R = a ∈ 𝒫 ⋃ dom ⁡ R ⟼ inf ran ⁡ x ∈ z ∈ 𝒫 dom ⁡ R | a ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x R ⁡ y 0 +∞ <
5 3 4 syl ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q → toOMeas ⁡ R = a ∈ 𝒫 ⋃ dom ⁡ R ⟼ inf ran ⁡ x ∈ z ∈ 𝒫 dom ⁡ R | a ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x R ⁡ y 0 +∞ <
6 simpr ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q ∧ a = A → a = A
7 6 sseq1d ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q ∧ a = A → a ⊆ ⋃ z ↔ A ⊆ ⋃ z
8 7 anbi1d ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q ∧ a = A → a ⊆ ⋃ z ∧ z ≼ ω ↔ A ⊆ ⋃ z ∧ z ≼ ω
9 8 rabbidv ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q ∧ a = A → z ∈ 𝒫 dom ⁡ R | a ⊆ ⋃ z ∧ z ≼ ω = z ∈ 𝒫 dom ⁡ R | A ⊆ ⋃ z ∧ z ≼ ω
10 9 mpteq1d ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q ∧ a = A → x ∈ z ∈ 𝒫 dom ⁡ R | a ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x R ⁡ y = x ∈ z ∈ 𝒫 dom ⁡ R | A ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x R ⁡ y
11 10 rneqd ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q ∧ a = A → ran ⁡ x ∈ z ∈ 𝒫 dom ⁡ R | a ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x R ⁡ y = ran ⁡ x ∈ z ∈ 𝒫 dom ⁡ R | A ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x R ⁡ y
12 11 infeq1d ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q ∧ a = A → inf ran ⁡ x ∈ z ∈ 𝒫 dom ⁡ R | a ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x R ⁡ y 0 +∞ < = inf ran ⁡ x ∈ z ∈ 𝒫 dom ⁡ R | A ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x R ⁡ y 0 +∞ <
13 simp3 ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q → A ⊆ ⋃ Q
14 fdm ⊢ R : Q ⟶ 0 +∞ → dom ⁡ R = Q
15 14 3ad2ant2 ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q → dom ⁡ R = Q
16 15 unieqd ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q → ⋃ dom ⁡ R = ⋃ Q
17 13 16 sseqtrrd ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q → A ⊆ ⋃ dom ⁡ R
18 2 uniexd ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q → ⋃ Q ∈ V
19 ssexg ⊢ A ⊆ ⋃ Q ∧ ⋃ Q ∈ V → A ∈ V
20 13 18 19 syl2anc ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q → A ∈ V
21 elpwg ⊢ A ∈ V → A ∈ 𝒫 ⋃ dom ⁡ R ↔ A ⊆ ⋃ dom ⁡ R
22 20 21 syl ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q → A ∈ 𝒫 ⋃ dom ⁡ R ↔ A ⊆ ⋃ dom ⁡ R
23 17 22 mpbird ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q → A ∈ 𝒫 ⋃ dom ⁡ R
24 xrltso ⊢ < Or ℝ *
25 iccssxr ⊢ 0 +∞ ⊆ ℝ *
26 soss ⊢ 0 +∞ ⊆ ℝ * → < Or ℝ * → < Or 0 +∞
27 25 26 ax-mp ⊢ < Or ℝ * → < Or 0 +∞
28 24 27 mp1i ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q → < Or 0 +∞
29 28 infexd ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q → inf ran ⁡ x ∈ z ∈ 𝒫 dom ⁡ R | A ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x R ⁡ y 0 +∞ < ∈ V
30 5 12 23 29 fvmptd ⊢ Q ∈ V ∧ R : Q ⟶ 0 +∞ ∧ A ⊆ ⋃ Q → toOMeas ⁡ R ⁡ A = inf ran ⁡ x ∈ z ∈ 𝒫 dom ⁡ R | A ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x R ⁡ y 0 +∞ <