Metamath Proof Explorer

Theorem uniiccmbl

Description: An almost-disjoint union of closed intervals is measurable. (This proof does not use countable choice, unlike iunmbl .) (Contributed by Mario Carneiro, 25-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
uniioombl.2 
|- ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) )
uniioombl.3 
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
Assertion uniiccmbl 
|- ( ph -> U. ran ( [,] o. F ) e. dom vol )

Proof

Step Hyp Ref Expression
1 uniioombl.1 
 |-  ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
2 uniioombl.2 
 |-  ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) )
3 uniioombl.3 
 |-  S = seq 1 ( + , ( ( abs o. - ) o. F ) )
4 1 uniiccdif 
 |-  ( ph -> ( U. ran ( (,) o. F ) C_ U. ran ( [,] o. F ) /\ ( vol* ` ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ) = 0 ) )
5 4 simpld 
 |-  ( ph -> U. ran ( (,) o. F ) C_ U. ran ( [,] o. F ) )
6 undif 
 |-  ( U. ran ( (,) o. F ) C_ U. ran ( [,] o. F ) <-> ( U. ran ( (,) o. F ) u. ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ) = U. ran ( [,] o. F ) )
7 5 6 sylib 
 |-  ( ph -> ( U. ran ( (,) o. F ) u. ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ) = U. ran ( [,] o. F ) )
8 1 2 3 uniioombl 
 |-  ( ph -> U. ran ( (,) o. F ) e. dom vol )
9 ovolficcss 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> U. ran ( [,] o. F ) C_ RR )
10 1 9 syl 
 |-  ( ph -> U. ran ( [,] o. F ) C_ RR )
11 10 ssdifssd 
 |-  ( ph -> ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) C_ RR )
12 4 simprd 
 |-  ( ph -> ( vol* ` ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ) = 0 )
13 nulmbl 
 |-  ( ( ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) C_ RR /\ ( vol* ` ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ) = 0 ) -> ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) e. dom vol )
14 11 12 13 syl2anc 
 |-  ( ph -> ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) e. dom vol )
15 unmbl 
 |-  ( ( U. ran ( (,) o. F ) e. dom vol /\ ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) e. dom vol ) -> ( U. ran ( (,) o. F ) u. ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ) e. dom vol )
16 8 14 15 syl2anc 
 |-  ( ph -> ( U. ran ( (,) o. F ) u. ( U. ran ( [,] o. F ) \ U. ran ( (,) o. F ) ) ) e. dom vol )
17 7 16 eqeltrrd 
 |-  ( ph -> U. ran ( [,] o. F ) e. dom vol )