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	$⊢ φ \to O \in V$
	carsgval.2	$⊢ φ \to M : 𝒫 O ⟶ [0, +∞]$
	carsgsiga.1	$⊢ φ \to M (\emptyset) = 0$
	carsgsiga.2	$⊢ (φ \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
	carsgsiga.3	$⊢ (φ \land x \subseteq y \land y \in 𝒫 O) \to M (x) \leq M (y)$
Assertion	carsgsiga	$⊢ φ \to toCaraSiga (M) \in sigAlgebra (O)$

Proof

Step	Hyp	Ref	Expression
1		carsgval.1	$⊢ φ \to O \in V$
2		carsgval.2	$⊢ φ \to M : 𝒫 O ⟶ [0, +∞]$
3		carsgsiga.1	$⊢ φ \to M (\emptyset) = 0$
4		carsgsiga.2	$⊢ (φ \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
5		carsgsiga.3	$⊢ (φ \land x \subseteq y \land y \in 𝒫 O) \to M (x) \leq M (y)$
6	1 2	carsgcl	$⊢ φ \to toCaraSiga (M) \subseteq 𝒫 O$
7	1 2 3	baselcarsg	$⊢ φ \to O \in toCaraSiga (M)$
8	1	adantr	$⊢ (φ \land g \in toCaraSiga (M)) \to O \in V$
9	2	adantr	$⊢ (φ \land g \in toCaraSiga (M)) \to M : 𝒫 O ⟶ [0, +∞]$
10		simpr	$⊢ (φ \land g \in toCaraSiga (M)) \to g \in toCaraSiga (M)$
11	8 9 10	difelcarsg	$⊢ (φ \land g \in toCaraSiga (M)) \to O ∖ g \in toCaraSiga (M)$
12	11	ralrimiva	$⊢ φ \to \forall g \in toCaraSiga (M) O ∖ g \in toCaraSiga (M)$
13	1	ad2antrr	$⊢ ((φ \land g \in 𝒫 toCaraSiga (M)) \land g ≼ ω) \to O \in V$
14	2	ad2antrr	$⊢ ((φ \land g \in 𝒫 toCaraSiga (M)) \land g ≼ ω) \to M : 𝒫 O ⟶ [0, +∞]$
15	3	ad2antrr	$⊢ ((φ \land g \in 𝒫 toCaraSiga (M)) \land g ≼ ω) \to M (\emptyset) = 0$
16	4	3adant1r	$⊢ ((φ \land g \in 𝒫 toCaraSiga (M)) \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
17	16	3adant1r	$⊢ (((φ \land g \in 𝒫 toCaraSiga (M)) \land g ≼ ω) \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
18	5	3adant1r	$⊢ ((φ \land g \in 𝒫 toCaraSiga (M)) \land x \subseteq y \land y \in 𝒫 O) \to M (x) \leq M (y)$
19	18	3adant1r	$⊢ (((φ \land g \in 𝒫 toCaraSiga (M)) \land g ≼ ω) \land x \subseteq y \land y \in 𝒫 O) \to M (x) \leq M (y)$
20		simpr	$⊢ ((φ \land g \in 𝒫 toCaraSiga (M)) \land g ≼ ω) \to g ≼ ω$
21		elpwi	$⊢ g \in 𝒫 toCaraSiga (M) \to g \subseteq toCaraSiga (M)$
22	21	ad2antlr	$⊢ ((φ \land g \in 𝒫 toCaraSiga (M)) \land g ≼ ω) \to g \subseteq toCaraSiga (M)$
23	13 14 15 17 19 20 22	carsgclctun	$⊢ ((φ \land g \in 𝒫 toCaraSiga (M)) \land g ≼ ω) \to ⋃ g \in toCaraSiga (M)$
24	23	ex	$⊢ (φ \land g \in 𝒫 toCaraSiga (M)) \to (g ≼ ω \to ⋃ g \in toCaraSiga (M))$
25	24	ralrimiva	$⊢ φ \to \forall g \in 𝒫 toCaraSiga (M) (g ≼ ω \to ⋃ g \in toCaraSiga (M))$
26	7 12 25	3jca	$⊢ φ \to (O \in toCaraSiga (M) \land \forall g \in toCaraSiga (M) O ∖ g \in toCaraSiga (M) \land \forall g \in 𝒫 toCaraSiga (M) (g ≼ ω \to ⋃ g \in toCaraSiga (M)))$
27	6 26	jca	$⊢ φ \to (toCaraSiga (M) \subseteq 𝒫 O \land (O \in toCaraSiga (M) \land \forall g \in toCaraSiga (M) O ∖ g \in toCaraSiga (M) \land \forall g \in 𝒫 toCaraSiga (M) (g ≼ ω \to ⋃ g \in toCaraSiga (M))))$
28		fvex	$⊢ toCaraSiga (M) \in V$
29		issiga	$⊢ toCaraSiga (M) \in V \to (toCaraSiga (M) \in sigAlgebra (O) \leftrightarrow (toCaraSiga (M) \subseteq 𝒫 O \land (O \in toCaraSiga (M) \land \forall g \in toCaraSiga (M) O ∖ g \in toCaraSiga (M) \land \forall g \in 𝒫 toCaraSiga (M) (g ≼ ω \to ⋃ g \in toCaraSiga (M)))))$
30	28 29	ax-mp	$⊢ toCaraSiga (M) \in sigAlgebra (O) \leftrightarrow (toCaraSiga (M) \subseteq 𝒫 O \land (O \in toCaraSiga (M) \land \forall g \in toCaraSiga (M) O ∖ g \in toCaraSiga (M) \land \forall g \in 𝒫 toCaraSiga (M) (g ≼ ω \to ⋃ g \in toCaraSiga (M))))$
31	27 30	sylibr	$⊢ φ \to toCaraSiga (M) \in sigAlgebra (O)$

Metamath Proof Explorer

Theorem carsgsiga

Proof