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