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 φ O OutMeas
caragen0.s S = CaraGen O
Assertion caragen0 φ S

Proof

Step Hyp Ref Expression
1 caragen0.o φ O OutMeas
2 caragen0.s S = CaraGen O
3 eqid dom O = dom O
4 0elpw 𝒫 dom O
5 4 a1i φ 𝒫 dom O
6 in0 a =
7 6 fveq2i O a = O
8 dif0 a = a
9 8 fveq2i O a = O a
10 7 9 oveq12i O a + 𝑒 O a = O + 𝑒 O a
11 10 a1i φ a 𝒫 dom O O a + 𝑒 O a = O + 𝑒 O a
12 1 ome0 φ O = 0
13 12 adantr φ a 𝒫 dom O O = 0
14 13 oveq1d φ a 𝒫 dom O O + 𝑒 O a = 0 + 𝑒 O a
15 iccssxr 0 +∞ *
16 1 adantr φ a 𝒫 dom O O OutMeas
17 elpwi a 𝒫 dom O a dom O
18 17 adantl φ a 𝒫 dom O a dom O
19 16 3 18 omecl φ a 𝒫 dom O O a 0 +∞
20 15 19 sseldi φ a 𝒫 dom O O a *
21 20 xaddid2d φ a 𝒫 dom O 0 + 𝑒 O a = O a
22 11 14 21 3eqtrd φ a 𝒫 dom O O a + 𝑒 O a = O a
23 1 3 2 5 22 carageneld φ S