Metamath Proof Explorer

Theorem carsgsiga

Description: The Caratheodory measurable sets constructed from outer measures form a Sigma-algebra. Statement (iii) of Theorem 1.11.4 of Bogachev p. 42. (Contributed by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
carsgsiga.1 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
carsgsiga.2 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
carsgsiga.3 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
Assertion carsgsiga ( 𝜑 → ( toCaraSiga ‘ 𝑀 ) ∈ ( sigAlgebra ‘ 𝑂 ) )

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2 carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3 carsgsiga.1 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
4 carsgsiga.2 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
5 carsgsiga.3 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
6 1 2 carsgcl ⊢ ( 𝜑 → ( toCaraSiga ‘ 𝑀 ) ⊆ 𝒫 𝑂 )
7 1 2 3 baselcarsg ⊢ ( 𝜑 → 𝑂 ∈ ( toCaraSiga ‘ 𝑀 ) )
8 1 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) ) → 𝑂 ∈ 𝑉 )
9 2 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) ) → 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) )
11 8 9 10 difelcarsg ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) ) → ( 𝑂 ∖ 𝑔 ) ∈ ( toCaraSiga ‘ 𝑀 ) )
12 11 ralrimiva ⊢ ( 𝜑 → ∀ 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) ( 𝑂 ∖ 𝑔 ) ∈ ( toCaraSiga ‘ 𝑀 ) )
13 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) ) ∧ 𝑔 ≼ ω ) → 𝑂 ∈ 𝑉 )
14 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) ) ∧ 𝑔 ≼ ω ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
15 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) ) ∧ 𝑔 ≼ ω ) → ( 𝑀 ‘ ∅ ) = 0 )
16 4 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
17 16 3adant1r ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) ) ∧ 𝑔 ≼ ω ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
18 5 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) ) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
19 18 3adant1r ⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) ) ∧ 𝑔 ≼ ω ) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
20 simpr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) ) ∧ 𝑔 ≼ ω ) → 𝑔 ≼ ω )
21 elpwi ⊢ ( 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) → 𝑔 ⊆ ( toCaraSiga ‘ 𝑀 ) )
22 21 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) ) ∧ 𝑔 ≼ ω ) → 𝑔 ⊆ ( toCaraSiga ‘ 𝑀 ) )
23 13 14 15 17 19 20 22 carsgclctun ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) ) ∧ 𝑔 ≼ ω ) → ∪ 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) )
24 23 ex ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) ) → ( 𝑔 ≼ ω → ∪ 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) ) )
25 24 ralrimiva ⊢ ( 𝜑 → ∀ 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) ( 𝑔 ≼ ω → ∪ 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) ) )
26 7 12 25 3jca ⊢ ( 𝜑 → ( 𝑂 ∈ ( toCaraSiga ‘ 𝑀 ) ∧ ∀ 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) ( 𝑂 ∖ 𝑔 ) ∈ ( toCaraSiga ‘ 𝑀 ) ∧ ∀ 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) ( 𝑔 ≼ ω → ∪ 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) ) ) )
27 6 26 jca ⊢ ( 𝜑 → ( ( toCaraSiga ‘ 𝑀 ) ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ ( toCaraSiga ‘ 𝑀 ) ∧ ∀ 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) ( 𝑂 ∖ 𝑔 ) ∈ ( toCaraSiga ‘ 𝑀 ) ∧ ∀ 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) ( 𝑔 ≼ ω → ∪ 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) ) ) ) )
28 fvex ⊢ ( toCaraSiga ‘ 𝑀 ) ∈ V
29 issiga ⊢ ( ( toCaraSiga ‘ 𝑀 ) ∈ V → ( ( toCaraSiga ‘ 𝑀 ) ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( ( toCaraSiga ‘ 𝑀 ) ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ ( toCaraSiga ‘ 𝑀 ) ∧ ∀ 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) ( 𝑂 ∖ 𝑔 ) ∈ ( toCaraSiga ‘ 𝑀 ) ∧ ∀ 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) ( 𝑔 ≼ ω → ∪ 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) ) ) ) ) )
30 28 29 ax-mp ⊢ ( ( toCaraSiga ‘ 𝑀 ) ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( ( toCaraSiga ‘ 𝑀 ) ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ ( toCaraSiga ‘ 𝑀 ) ∧ ∀ 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) ( 𝑂 ∖ 𝑔 ) ∈ ( toCaraSiga ‘ 𝑀 ) ∧ ∀ 𝑔 ∈ 𝒫 ( toCaraSiga ‘ 𝑀 ) ( 𝑔 ≼ ω → ∪ 𝑔 ∈ ( toCaraSiga ‘ 𝑀 ) ) ) ) )
31 27 30 sylibr ⊢ ( 𝜑 → ( toCaraSiga ‘ 𝑀 ) ∈ ( sigAlgebra ‘ 𝑂 ) )