carsgclctun

Description: The Caratheodory measurable sets are closed under countable union. (Contributed by Thierry Arnoux, 21-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)$
	carsgclctun.1	$⊢ φ \to A ≼ ω$
	carsgclctun.2	$⊢ φ \to A \subseteq toCaraSiga (M)$
Assertion	carsgclctun	$⊢ φ \to ⋃ A \in toCaraSiga (M)$

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		carsgclctun.1	$⊢ φ \to A ≼ ω$
7		carsgclctun.2	$⊢ φ \to A \subseteq toCaraSiga (M)$
8	7	unissd	$⊢ φ \to ⋃ A \subseteq ⋃ toCaraSiga (M)$
9	1 2 3	carsguni	$⊢ φ \to ⋃ toCaraSiga (M) = O$
10	8 9	sseqtrd	$⊢ φ \to ⋃ A \subseteq O$
11	1	adantr	$⊢ (φ \land e \in 𝒫 O) \to O \in V$
12	2	adantr	$⊢ (φ \land e \in 𝒫 O) \to M : 𝒫 O ⟶ [0, +∞]$
13	3	adantr	$⊢ (φ \land e \in 𝒫 O) \to M (\emptyset) = 0$
14	4	3adant1r	$⊢ ((φ \land e \in 𝒫 O) \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{*}} M (y)$
15	5	3adant1r	$⊢ ((φ \land e \in 𝒫 O) \land x \subseteq y \land y \in 𝒫 O) \to M (x) \leq M (y)$
16	6	adantr	$⊢ (φ \land e \in 𝒫 O) \to A ≼ ω$
17	7	adantr	$⊢ (φ \land e \in 𝒫 O) \to A \subseteq toCaraSiga (M)$
18		simpr	$⊢ (φ \land e \in 𝒫 O) \to e \in 𝒫 O$
19	11 12 13 14 15 16 17 18	carsgclctunlem3	$⊢ (φ \land e \in 𝒫 O) \to M (e \cap ⋃ A) +_{𝑒} M (e ∖ ⋃ A) \leq M (e)$
20		inex1g	$⊢ e \in 𝒫 O \to e \cap ⋃ A \in V$
21	20	adantl	$⊢ (φ \land e \in 𝒫 O) \to e \cap ⋃ A \in V$
22		difexg	$⊢ e \in 𝒫 O \to e ∖ ⋃ A \in V$
23	22	adantl	$⊢ (φ \land e \in 𝒫 O) \to e ∖ ⋃ A \in V$
24		prct	$⊢ (e \cap ⋃ A \in V \land e ∖ ⋃ A \in V) \to \{e \cap ⋃ A, e ∖ ⋃ A\} ≼ ω$
25	21 23 24	syl2anc	$⊢ (φ \land e \in 𝒫 O) \to \{e \cap ⋃ A, e ∖ ⋃ A\} ≼ ω$
26	18	elpwincl1	$⊢ (φ \land e \in 𝒫 O) \to e \cap ⋃ A \in 𝒫 O$
27	18	elpwdifcl	$⊢ (φ \land e \in 𝒫 O) \to e ∖ ⋃ A \in 𝒫 O$
28		prssi	$⊢ (e \cap ⋃ A \in 𝒫 O \land e ∖ ⋃ A \in 𝒫 O) \to \{e \cap ⋃ A, e ∖ ⋃ A\} \subseteq 𝒫 O$
29	26 27 28	syl2anc	$⊢ (φ \land e \in 𝒫 O) \to \{e \cap ⋃ A, e ∖ ⋃ A\} \subseteq 𝒫 O$
30		prex	$⊢ \{e \cap ⋃ A, e ∖ ⋃ A\} \in V$
31		breq1	$⊢ x = \{e \cap ⋃ A, e ∖ ⋃ A\} \to (x ≼ ω \leftrightarrow \{e \cap ⋃ A, e ∖ ⋃ A\} ≼ ω)$
32		sseq1	$⊢ x = \{e \cap ⋃ A, e ∖ ⋃ A\} \to (x \subseteq 𝒫 O \leftrightarrow \{e \cap ⋃ A, e ∖ ⋃ A\} \subseteq 𝒫 O)$
33	31 32	3anbi23d	$⊢ x = \{e \cap ⋃ A, e ∖ ⋃ A\} \to ((φ \land x ≼ ω \land x \subseteq 𝒫 O) \leftrightarrow (φ \land \{e \cap ⋃ A, e ∖ ⋃ A\} ≼ ω \land \{e \cap ⋃ A, e ∖ ⋃ A\} \subseteq 𝒫 O))$
34		unieq	$⊢ x = \{e \cap ⋃ A, e ∖ ⋃ A\} \to ⋃ x = ⋃ \{e \cap ⋃ A, e ∖ ⋃ A\}$
35	34	fveq2d	$⊢ x = \{e \cap ⋃ A, e ∖ ⋃ A\} \to M (⋃ x) = M (⋃ \{e \cap ⋃ A, e ∖ ⋃ A\})$
36		esumeq1	$⊢ x = \{e \cap ⋃ A, e ∖ ⋃ A\} \to \underset{y \in x}{\sum^{}} M (y) = \underset{y \in \{e \cap ⋃ A, e ∖ ⋃ A\}}{\sum^{}} M (y)$
37	35 36	breq12d	$⊢ x = \{e \cap ⋃ A, e ∖ ⋃ A\} \to (M (⋃ x) \leq \underset{y \in x}{\sum^{}} M (y) \leftrightarrow M (⋃ \{e \cap ⋃ A, e ∖ ⋃ A\}) \leq \underset{y \in \{e \cap ⋃ A, e ∖ ⋃ A\}}{\sum^{}} M (y))$
38	33 37	imbi12d	$⊢ x = \{e \cap ⋃ A, e ∖ ⋃ A\} \to (((φ \land x ≼ ω \land x \subseteq 𝒫 O) \to M (⋃ x) \leq \underset{y \in x}{\sum^{}} M (y)) \leftrightarrow ((φ \land \{e \cap ⋃ A, e ∖ ⋃ A\} ≼ ω \land \{e \cap ⋃ A, e ∖ ⋃ A\} \subseteq 𝒫 O) \to M (⋃ \{e \cap ⋃ A, e ∖ ⋃ A\}) \leq \underset{y \in \{e \cap ⋃ A, e ∖ ⋃ A\}}{\sum^{}} M (y)))$
39	38 4	vtoclg	$⊢ \{e \cap ⋃ A, e ∖ ⋃ A\} \in V \to ((φ \land \{e \cap ⋃ A, e ∖ ⋃ A\} ≼ ω \land \{e \cap ⋃ A, e ∖ ⋃ A\} \subseteq 𝒫 O) \to M (⋃ \{e \cap ⋃ A, e ∖ ⋃ A\}) \leq \underset{y \in \{e \cap ⋃ A, e ∖ ⋃ A\}}{\sum^{*}} M (y))$
40	30 39	ax-mp	$⊢ (φ \land \{e \cap ⋃ A, e ∖ ⋃ A\} ≼ ω \land \{e \cap ⋃ A, e ∖ ⋃ A\} \subseteq 𝒫 O) \to M (⋃ \{e \cap ⋃ A, e ∖ ⋃ A\}) \leq \underset{y \in \{e \cap ⋃ A, e ∖ ⋃ A\}}{\sum^{*}} M (y)$
41	40	3adant1r	$⊢ ((φ \land e \in 𝒫 O) \land \{e \cap ⋃ A, e ∖ ⋃ A\} ≼ ω \land \{e \cap ⋃ A, e ∖ ⋃ A\} \subseteq 𝒫 O) \to M (⋃ \{e \cap ⋃ A, e ∖ ⋃ A\}) \leq \underset{y \in \{e \cap ⋃ A, e ∖ ⋃ A\}}{\sum^{*}} M (y)$
42	25 29 41	mpd3an23	$⊢ (φ \land e \in 𝒫 O) \to M (⋃ \{e \cap ⋃ A, e ∖ ⋃ A\}) \leq \underset{y \in \{e \cap ⋃ A, e ∖ ⋃ A\}}{\sum^{*}} M (y)$
43		uniprg	$⊢ (e \cap ⋃ A \in 𝒫 O \land e ∖ ⋃ A \in 𝒫 O) \to ⋃ \{e \cap ⋃ A, e ∖ ⋃ A\} = (e \cap ⋃ A) \cup (e ∖ ⋃ A)$
44	26 27 43	syl2anc	$⊢ (φ \land e \in 𝒫 O) \to ⋃ \{e \cap ⋃ A, e ∖ ⋃ A\} = (e \cap ⋃ A) \cup (e ∖ ⋃ A)$
45		inundif	$⊢ (e \cap ⋃ A) \cup (e ∖ ⋃ A) = e$
46	44 45	eqtrdi	$⊢ (φ \land e \in 𝒫 O) \to ⋃ \{e \cap ⋃ A, e ∖ ⋃ A\} = e$
47	46	fveq2d	$⊢ (φ \land e \in 𝒫 O) \to M (⋃ \{e \cap ⋃ A, e ∖ ⋃ A\}) = M (e)$
48		simpr	$⊢ ((φ \land e \in 𝒫 O) \land y = e \cap ⋃ A) \to y = e \cap ⋃ A$
49	48	fveq2d	$⊢ ((φ \land e \in 𝒫 O) \land y = e \cap ⋃ A) \to M (y) = M (e \cap ⋃ A)$
50		simpr	$⊢ ((φ \land e \in 𝒫 O) \land y = e ∖ ⋃ A) \to y = e ∖ ⋃ A$
51	50	fveq2d	$⊢ ((φ \land e \in 𝒫 O) \land y = e ∖ ⋃ A) \to M (y) = M (e ∖ ⋃ A)$
52	12 26	ffvelrnd	$⊢ (φ \land e \in 𝒫 O) \to M (e \cap ⋃ A) \in [0, +∞]$
53	12 27	ffvelrnd	$⊢ (φ \land e \in 𝒫 O) \to M (e ∖ ⋃ A) \in [0, +∞]$
54		ineq2	$⊢ e \cap ⋃ A = e ∖ ⋃ A \to (e \cap ⋃ A) \cap (e \cap ⋃ A) = (e \cap ⋃ A) \cap (e ∖ ⋃ A)$
55		inidm	$⊢ (e \cap ⋃ A) \cap (e \cap ⋃ A) = e \cap ⋃ A$
56		inindif	$⊢ (e \cap ⋃ A) \cap (e ∖ ⋃ A) = \emptyset$
57	54 55 56	3eqtr3g	$⊢ e \cap ⋃ A = e ∖ ⋃ A \to e \cap ⋃ A = \emptyset$
58	57	adantl	$⊢ ((φ \land e \in 𝒫 O) \land e \cap ⋃ A = e ∖ ⋃ A) \to e \cap ⋃ A = \emptyset$
59	58	fveq2d	$⊢ ((φ \land e \in 𝒫 O) \land e \cap ⋃ A = e ∖ ⋃ A) \to M (e \cap ⋃ A) = M (\emptyset)$
60	3	ad2antrr	$⊢ ((φ \land e \in 𝒫 O) \land e \cap ⋃ A = e ∖ ⋃ A) \to M (\emptyset) = 0$
61	59 60	eqtrd	$⊢ ((φ \land e \in 𝒫 O) \land e \cap ⋃ A = e ∖ ⋃ A) \to M (e \cap ⋃ A) = 0$
62	61	orcd	$⊢ ((φ \land e \in 𝒫 O) \land e \cap ⋃ A = e ∖ ⋃ A) \to (M (e \cap ⋃ A) = 0 \lor M (e \cap ⋃ A) = +∞)$
63	62	ex	$⊢ (φ \land e \in 𝒫 O) \to (e \cap ⋃ A = e ∖ ⋃ A \to (M (e \cap ⋃ A) = 0 \lor M (e \cap ⋃ A) = +∞))$
64	49 51 26 27 52 53 63	esumpr2	$⊢ (φ \land e \in 𝒫 O) \to \underset{y \in \{e \cap ⋃ A, e ∖ ⋃ A\}}{\sum^{*}} M (y) = M (e \cap ⋃ A) +_{𝑒} M (e ∖ ⋃ A)$
65	42 47 64	3brtr3d	$⊢ (φ \land e \in 𝒫 O) \to M (e) \leq M (e \cap ⋃ A) +_{𝑒} M (e ∖ ⋃ A)$
66	19 65	jca	$⊢ (φ \land e \in 𝒫 O) \to (M (e \cap ⋃ A) +_{𝑒} M (e ∖ ⋃ A) \leq M (e) \land M (e) \leq M (e \cap ⋃ A) +_{𝑒} M (e ∖ ⋃ A))$
67		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
68	67 52	sseldi	$⊢ (φ \land e \in 𝒫 O) \to M (e \cap ⋃ A) \in ℝ^{*}$
69	67 53	sseldi	$⊢ (φ \land e \in 𝒫 O) \to M (e ∖ ⋃ A) \in ℝ^{*}$
70	68 69	xaddcld	$⊢ (φ \land e \in 𝒫 O) \to M (e \cap ⋃ A) +_{𝑒} M (e ∖ ⋃ A) \in ℝ^{*}$
71	2	ffvelrnda	$⊢ (φ \land e \in 𝒫 O) \to M (e) \in [0, +∞]$
72	67 71	sseldi	$⊢ (φ \land e \in 𝒫 O) \to M (e) \in ℝ^{*}$
73		xrletri3	$⊢ (M (e \cap ⋃ A) +_{𝑒} M (e ∖ ⋃ A) \in ℝ^{} \land M (e) \in ℝ^{}) \to (M (e \cap ⋃ A) +_{𝑒} M (e ∖ ⋃ A) = M (e) \leftrightarrow (M (e \cap ⋃ A) +_{𝑒} M (e ∖ ⋃ A) \leq M (e) \land M (e) \leq M (e \cap ⋃ A) +_{𝑒} M (e ∖ ⋃ A)))$
74	70 72 73	syl2anc	$⊢ (φ \land e \in 𝒫 O) \to (M (e \cap ⋃ A) +_{𝑒} M (e ∖ ⋃ A) = M (e) \leftrightarrow (M (e \cap ⋃ A) +_{𝑒} M (e ∖ ⋃ A) \leq M (e) \land M (e) \leq M (e \cap ⋃ A) +_{𝑒} M (e ∖ ⋃ A)))$
75	66 74	mpbird	$⊢ (φ \land e \in 𝒫 O) \to M (e \cap ⋃ A) +_{𝑒} M (e ∖ ⋃ A) = M (e)$
76	75	ralrimiva	$⊢ φ \to \forall e \in 𝒫 O M (e \cap ⋃ A) +_{𝑒} M (e ∖ ⋃ A) = M (e)$
77	1 2	elcarsg	$⊢ φ \to (⋃ A \in toCaraSiga (M) \leftrightarrow (⋃ A \subseteq O \land \forall e \in 𝒫 O M (e \cap ⋃ A) +_{𝑒} M (e ∖ ⋃ A) = M (e)))$
78	10 76 77	mpbir2and	$⊢ φ \to ⋃ A \in toCaraSiga (M)$

Metamath Proof Explorer

Theorem carsgclctun

Proof