fiunelcarsg

Description: The Caratheodory measurable sets are closed under finite union. (Contributed by Thierry Arnoux, 23-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)$
	fiunelcarsg.1	$⊢ φ \to A \in Fin$
	fiunelcarsg.2	$⊢ φ \to A \subseteq toCaraSiga (M)$
Assertion	fiunelcarsg	$⊢ φ \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		fiunelcarsg.1	$⊢ φ \to A \in Fin$
6		fiunelcarsg.2	$⊢ φ \to A \subseteq toCaraSiga (M)$
7		unieq	$⊢ a = \emptyset \to ⋃ a = ⋃ \emptyset$
8		eqidd	$⊢ a = \emptyset \to toCaraSiga (M) = toCaraSiga (M)$
9	7 8	eleq12d	$⊢ a = \emptyset \to (⋃ a \in toCaraSiga (M) \leftrightarrow ⋃ \emptyset \in toCaraSiga (M))$
10		unieq	$⊢ a = b \to ⋃ a = ⋃ b$
11		eqidd	$⊢ a = b \to toCaraSiga (M) = toCaraSiga (M)$
12	10 11	eleq12d	$⊢ a = b \to (⋃ a \in toCaraSiga (M) \leftrightarrow ⋃ b \in toCaraSiga (M))$
13		unieq	$⊢ a = b \cup \{x\} \to ⋃ a = ⋃ (b \cup \{x\})$
14		eqidd	$⊢ a = b \cup \{x\} \to toCaraSiga (M) = toCaraSiga (M)$
15	13 14	eleq12d	$⊢ a = b \cup \{x\} \to (⋃ a \in toCaraSiga (M) \leftrightarrow ⋃ (b \cup \{x\}) \in toCaraSiga (M))$
16		unieq	$⊢ a = A \to ⋃ a = ⋃ A$
17		eqidd	$⊢ a = A \to toCaraSiga (M) = toCaraSiga (M)$
18	16 17	eleq12d	$⊢ a = A \to (⋃ a \in toCaraSiga (M) \leftrightarrow ⋃ A \in toCaraSiga (M))$
19		uni0	$⊢ ⋃ \emptyset = \emptyset$
20		difid	$⊢ O ∖ O = \emptyset$
21	19 20	eqtr4i	$⊢ ⋃ \emptyset = O ∖ O$
22	1 2 3	baselcarsg	$⊢ φ \to O \in toCaraSiga (M)$
23	1 2 22	difelcarsg	$⊢ φ \to O ∖ O \in toCaraSiga (M)$
24	21 23	eqeltrid	$⊢ φ \to ⋃ \emptyset \in toCaraSiga (M)$
25		uniun	$⊢ ⋃ (b \cup \{x\}) = ⋃ b \cup ⋃ \{x\}$
26		unisnv	$⊢ ⋃ \{x\} = x$
27	26	uneq2i	$⊢ ⋃ b \cup ⋃ \{x\} = ⋃ b \cup x$
28	25 27	eqtri	$⊢ ⋃ (b \cup \{x\}) = ⋃ b \cup x$
29	1	ad2antrr	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land ⋃ b \in toCaraSiga (M)) \to O \in V$
30	2	ad2antrr	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land ⋃ b \in toCaraSiga (M)) \to M : 𝒫 O ⟶ [0, +∞]$
31		simpr	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land ⋃ b \in toCaraSiga (M)) \to ⋃ b \in toCaraSiga (M)$
32		simpll	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land ⋃ b \in toCaraSiga (M)) \to φ$
33	1 2 3 4	carsgsigalem	$⊢ (φ \land e \in 𝒫 O \land f \in 𝒫 O) \to M (e \cup f) \leq M (e) +_{𝑒} M (f)$
34	32 33	syl3an1	$⊢ (((φ \land (b \subseteq A \land x \in (A ∖ b))) \land ⋃ b \in toCaraSiga (M)) \land e \in 𝒫 O \land f \in 𝒫 O) \to M (e \cup f) \leq M (e) +_{𝑒} M (f)$
35	6	ad2antrr	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land ⋃ b \in toCaraSiga (M)) \to A \subseteq toCaraSiga (M)$
36		simplrr	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land ⋃ b \in toCaraSiga (M)) \to x \in (A ∖ b)$
37	36	eldifad	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land ⋃ b \in toCaraSiga (M)) \to x \in A$
38	35 37	sseldd	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land ⋃ b \in toCaraSiga (M)) \to x \in toCaraSiga (M)$
39	29 30 31 34 38	unelcarsg	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land ⋃ b \in toCaraSiga (M)) \to ⋃ b \cup x \in toCaraSiga (M)$
40	28 39	eqeltrid	$⊢ ((φ \land (b \subseteq A \land x \in (A ∖ b))) \land ⋃ b \in toCaraSiga (M)) \to ⋃ (b \cup \{x\}) \in toCaraSiga (M)$
41	40	ex	$⊢ (φ \land (b \subseteq A \land x \in (A ∖ b))) \to (⋃ b \in toCaraSiga (M) \to ⋃ (b \cup \{x\}) \in toCaraSiga (M))$
42	9 12 15 18 24 41 5	findcard2d	$⊢ φ \to ⋃ A \in toCaraSiga (M)$

Metamath Proof Explorer

Theorem fiunelcarsg

Proof