Metamath Proof Explorer


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 sselid ( ( 𝜑𝑎 ∈ 𝒫 dom 𝑂 ) → ( 𝑂𝑎 ) ∈ ℝ* )
21 20 xaddid2d ( ( 𝜑𝑎 ∈ 𝒫 dom 𝑂 ) → ( 0 +𝑒 ( 𝑂𝑎 ) ) = ( 𝑂𝑎 ) )
22 11 14 21 3eqtrd ( ( 𝜑𝑎 ∈ 𝒫 dom 𝑂 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ ∅ ) ) +𝑒 ( 𝑂 ‘ ( 𝑎 ∖ ∅ ) ) ) = ( 𝑂𝑎 ) )
23 1 3 2 5 22 carageneld ( 𝜑 → ∅ ∈ 𝑆 )