caragen0

Description: The empty set belongs to any Caratheodory's construction. First part of Step (b) in the proof of Theorem 113C of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	caragen0.o	$⊢ φ \to O \in OutMeas$
	caragen0.s	$⊢ S = CaraGen (O)$
Assertion	caragen0	$⊢ φ \to \emptyset \in S$

Proof

Step	Hyp	Ref	Expression
1		caragen0.o	$⊢ φ \to O \in OutMeas$
2		caragen0.s	$⊢ S = CaraGen (O)$
3		eqid	$⊢ ⋃ dom O = ⋃ dom O$
4		0elpw	$⊢ \emptyset \in 𝒫 ⋃ dom O$
5	4	a1i	$⊢ φ \to \emptyset \in 𝒫 ⋃ dom O$
6		in0	$⊢ a \cap \emptyset = \emptyset$
7	6	fveq2i	$⊢ O (a \cap \emptyset) = O (\emptyset)$
8		dif0	$⊢ a ∖ \emptyset = a$
9	8	fveq2i	$⊢ O (a ∖ \emptyset) = O (a)$
10	7 9	oveq12i	$⊢ O (a \cap \emptyset) +_{𝑒} O (a ∖ \emptyset) = O (\emptyset) +_{𝑒} O (a)$
11	10	a1i	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (a \cap \emptyset) +_{𝑒} O (a ∖ \emptyset) = O (\emptyset) +_{𝑒} O (a)$
12	1	ome0	$⊢ φ \to O (\emptyset) = 0$
13	12	adantr	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (\emptyset) = 0$
14	13	oveq1d	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (\emptyset) +_{𝑒} O (a) = 0 +_{𝑒} O (a)$
15		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
16	1	adantr	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O \in OutMeas$
17		elpwi	$⊢ a \in 𝒫 ⋃ dom O \to a \subseteq ⋃ dom O$
18	17	adantl	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to a \subseteq ⋃ dom O$
19	16 3 18	omecl	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (a) \in [0, +∞]$
20	15 19	sselid	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (a) \in ℝ^{*}$
21	20	xaddlidd	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to 0 +_{𝑒} O (a) = O (a)$
22	11 14 21	3eqtrd	$⊢ (φ \land a \in 𝒫 ⋃ dom O) \to O (a \cap \emptyset) +_{𝑒} O (a ∖ \emptyset) = O (a)$
23	1 3 2 5 22	carageneld	$⊢ φ \to \emptyset \in S$

Metamath Proof Explorer

Theorem caragen0

Proof