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 
|- ( ph -> O e. OutMeas )
caragen0.s 
|- S = ( CaraGen ` O )
Assertion caragen0 
|- ( ph -> (/) e. S )

Proof

Step Hyp Ref Expression
1 caragen0.o 
 |-  ( ph -> O e. OutMeas )
2 caragen0.s 
 |-  S = ( CaraGen ` O )
3 eqid 
 |-  U. dom O = U. dom O
4 0elpw 
 |-  (/) e. ~P U. dom O
5 4 a1i 
 |-  ( ph -> (/) e. ~P U. dom O )
6 in0 
 |-  ( a i^i (/) ) = (/)
7 6 fveq2i 
 |-  ( O ` ( a i^i (/) ) ) = ( O ` (/) )
8 dif0 
 |-  ( a \ (/) ) = a
9 8 fveq2i 
 |-  ( O ` ( a \ (/) ) ) = ( O ` a )
10 7 9 oveq12i 
 |-  ( ( O ` ( a i^i (/) ) ) +e ( O ` ( a \ (/) ) ) ) = ( ( O ` (/) ) +e ( O ` a ) )
11 10 a1i 
 |-  ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i (/) ) ) +e ( O ` ( a \ (/) ) ) ) = ( ( O ` (/) ) +e ( O ` a ) ) )
12 1 ome0 
 |-  ( ph -> ( O ` (/) ) = 0 )
13 12 adantr 
 |-  ( ( ph /\ a e. ~P U. dom O ) -> ( O ` (/) ) = 0 )
14 13 oveq1d 
 |-  ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` (/) ) +e ( O ` a ) ) = ( 0 +e ( O ` a ) ) )
15 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
16 1 adantr 
 |-  ( ( ph /\ a e. ~P U. dom O ) -> O e. OutMeas )
17 elpwi 
 |-  ( a e. ~P U. dom O -> a C_ U. dom O )
18 17 adantl 
 |-  ( ( ph /\ a e. ~P U. dom O ) -> a C_ U. dom O )
19 16 3 18 omecl 
 |-  ( ( ph /\ a e. ~P U. dom O ) -> ( O ` a ) e. ( 0 [,] +oo ) )
20 15 19 sseldi 
 |-  ( ( ph /\ a e. ~P U. dom O ) -> ( O ` a ) e. RR* )
21 20 xaddid2d 
 |-  ( ( ph /\ a e. ~P U. dom O ) -> ( 0 +e ( O ` a ) ) = ( O ` a ) )
22 11 14 21 3eqtrd 
 |-  ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i (/) ) ) +e ( O ` ( a \ (/) ) ) ) = ( O ` a ) )
23 1 3 2 5 22 carageneld 
 |-  ( ph -> (/) e. S )