Theorem 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	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	caragen0.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
Assertion	caragen0	⊢ ( 𝜑 → ∅ ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		caragen0.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		caragen0.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
3		eqid	⊢ ∪ dom 𝑂 = ∪ dom 𝑂
4		0elpw	⊢ ∅ ∈ 𝒫 ∪ dom 𝑂
5	4	a1i	⊢ ( 𝜑 → ∅ ∈ 𝒫 ∪ dom 𝑂 )
6		in0	⊢ ( 𝑎 ∩ ∅ ) = ∅
7	6	fveq2i	⊢ ( 𝑂 ‘ ( 𝑎 ∩ ∅ ) ) = ( 𝑂 ‘ ∅ )
8		dif0	⊢ ( 𝑎 ∖ ∅ ) = 𝑎
9	8	fveq2i	⊢ ( 𝑂 ‘ ( 𝑎 ∖ ∅ ) ) = ( 𝑂 ‘ 𝑎 )
10	7 9	oveq12i	⊢ ( ( 𝑂 ‘ ( 𝑎 ∩ ∅ ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ ∅ ) ) ) = ( ( 𝑂 ‘ ∅ ) +𝑒 ( 𝑂 ‘ 𝑎 ) )
11	10	a1i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ ∅ ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ ∅ ) ) ) = ( ( 𝑂 ‘ ∅ ) +𝑒 ( 𝑂 ‘ 𝑎 ) ) )
12	1	ome0	⊢ ( 𝜑 → ( 𝑂 ‘ ∅ ) = 0 )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑂 ‘ ∅ ) = 0 )
14	13	oveq1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( ( 𝑂 ‘ ∅ ) +𝑒 ( 𝑂 ‘ 𝑎 ) ) = ( 0 +𝑒 ( 𝑂 ‘ 𝑎 ) ) )
15		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
16	1	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → 𝑂 ∈ OutMeas )
17		elpwi	⊢ ( 𝑎 ∈ 𝒫 ∪ dom 𝑂 → 𝑎 ⊆ ∪ dom 𝑂 )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → 𝑎 ⊆ ∪ dom 𝑂 )
19	16 3 18	omecl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑂 ‘ 𝑎 ) ∈ ( 0 [,] +∞ ) )
20	15 19	sseldi	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑂 ‘ 𝑎 ) ∈ ℝ* )
21	20	xaddid2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 0 +𝑒 ( 𝑂 ‘ 𝑎 ) ) = ( 𝑂 ‘ 𝑎 ) )
22	11 14 21	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ ∅ ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ ∅ ) ) ) = ( 𝑂 ‘ 𝑎 ) )
23	1 3 2 5 22	carageneld	⊢ ( 𝜑 → ∅ ∈ 𝑆 )