Theorem uniiccvol

Description: An almost-disjoint union of closed intervals (disjoint interiors) has volume equal to the sum of the volume of the intervals. (This proof does not use countable choice, unlike voliun .) (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	uniiccvol	|- ( ph -> ( vol* ` U. ran ( [,] o. F ) ) = sup ( ran S , RR* , < ) )

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		ovolficcss	|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> U. ran ( [,] o. F ) C_ RR )
5	1 4	syl	|- ( ph -> U. ran ( [,] o. F ) C_ RR )
6		ovolcl	|- ( U. ran ( [,] o. F ) C_ RR -> ( vol* ` U. ran ( [,] o. F ) ) e. RR* )
7	5 6	syl	|- ( ph -> ( vol* ` U. ran ( [,] o. F ) ) e. RR* )
8		eqid	|- ( ( abs o. - ) o. F ) = ( ( abs o. - ) o. F )
9	8 3	ovolsf	|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> S : NN --> ( 0 [,) +oo ) )
10	1 9	syl	|- ( ph -> S : NN --> ( 0 [,) +oo ) )
11	10	frnd	|- ( ph -> ran S C_ ( 0 [,) +oo ) )
12		icossxr	|- ( 0 [,) +oo ) C_ RR*
13	11 12	sstrdi	|- ( ph -> ran S C_ RR* )
14		supxrcl	|- ( ran S C_ RR* -> sup ( ran S , RR* , < ) e. RR* )
15	13 14	syl	|- ( ph -> sup ( ran S , RR* , < ) e. RR* )
16		ssid	|- U. ran ( [,] o. F ) C_ U. ran ( [,] o. F )
17	3	ovollb2	|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ U. ran ( [,] o. F ) C_ U. ran ( [,] o. F ) ) -> ( vol* ` U. ran ( [,] o. F ) ) <_ sup ( ran S , RR* , < ) )
18	1 16 17	sylancl	|- ( ph -> ( vol* ` U. ran ( [,] o. F ) ) <_ sup ( ran S , RR* , < ) )
19	1 2 3	uniioovol	|- ( ph -> ( vol* ` U. ran ( (,) o. F ) ) = sup ( ran S , RR* , < ) )
20		ioossicc	|- ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) C_ ( ( 1st ` ( F ` x ) ) [,] ( 2nd ` ( F ` x ) ) )
21		df-ov	|- ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) = ( (,) ` <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. )
22		df-ov	|- ( ( 1st ` ( F ` x ) ) [,] ( 2nd ` ( F ` x ) ) ) = ( [,] ` <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. )
23	20 21 22	3sstr3i	|- ( (,) ` <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. ) C_ ( [,] ` <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. )
24	23	a1i	|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( (,) ` <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. ) C_ ( [,] ` <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. ) )
25		ffvelrn	|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( F ` x ) e. ( <_ i^i ( RR X. RR ) ) )
26	25	elin2d	|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( F ` x ) e. ( RR X. RR ) )
27		1st2nd2	|- ( ( F ` x ) e. ( RR X. RR ) -> ( F ` x ) = <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. )
28	26 27	syl	|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( F ` x ) = <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. )
29	28	fveq2d	|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( (,) ` ( F ` x ) ) = ( (,) ` <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. ) )
30	28	fveq2d	|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( [,] ` ( F ` x ) ) = ( [,] ` <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. ) )
31	24 29 30	3sstr4d	|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( (,) ` ( F ` x ) ) C_ ( [,] ` ( F ` x ) ) )
32		fvco3	|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( ( (,) o. F ) ` x ) = ( (,) ` ( F ` x ) ) )
33		fvco3	|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( ( [,] o. F ) ` x ) = ( [,] ` ( F ` x ) ) )
34	31 32 33	3sstr4d	|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( ( (,) o. F ) ` x ) C_ ( ( [,] o. F ) ` x ) )
35	1 34	sylan	|- ( ( ph /\ x e. NN ) -> ( ( (,) o. F ) ` x ) C_ ( ( [,] o. F ) ` x ) )
36	35	ralrimiva	|- ( ph -> A. x e. NN ( ( (,) o. F ) ` x ) C_ ( ( [,] o. F ) ` x ) )
37		ss2iun	|- ( A. x e. NN ( ( (,) o. F ) ` x ) C_ ( ( [,] o. F ) ` x ) -> U_ x e. NN ( ( (,) o. F ) ` x ) C_ U_ x e. NN ( ( [,] o. F ) ` x ) )
38	36 37	syl	|- ( ph -> U_ x e. NN ( ( (,) o. F ) ` x ) C_ U_ x e. NN ( ( [,] o. F ) ` x ) )
39		ioof	|- (,) : ( RR* X. RR* ) --> ~P RR
40		ffn	|- ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
41	39 40	ax-mp	|- (,) Fn ( RR* X. RR* )
42		inss2	|- ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
43		rexpssxrxp	|- ( RR X. RR ) C_ ( RR* X. RR* )
44	42 43	sstri	|- ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
45		fss	|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> F : NN --> ( RR* X. RR* ) )
46	1 44 45	sylancl	|- ( ph -> F : NN --> ( RR* X. RR* ) )
47		fnfco	|- ( ( (,) Fn ( RR* X. RR* ) /\ F : NN --> ( RR* X. RR* ) ) -> ( (,) o. F ) Fn NN )
48	41 46 47	sylancr	|- ( ph -> ( (,) o. F ) Fn NN )
49		fniunfv	|- ( ( (,) o. F ) Fn NN -> U_ x e. NN ( ( (,) o. F ) ` x ) = U. ran ( (,) o. F ) )
50	48 49	syl	|- ( ph -> U_ x e. NN ( ( (,) o. F ) ` x ) = U. ran ( (,) o. F ) )
51		iccf	|- [,] : ( RR* X. RR* ) --> ~P RR*
52		ffn	|- ( [,] : ( RR* X. RR* ) --> ~P RR* -> [,] Fn ( RR* X. RR* ) )
53	51 52	ax-mp	|- [,] Fn ( RR* X. RR* )
54		fnfco	|- ( ( [,] Fn ( RR* X. RR* ) /\ F : NN --> ( RR* X. RR* ) ) -> ( [,] o. F ) Fn NN )
55	53 46 54	sylancr	|- ( ph -> ( [,] o. F ) Fn NN )
56		fniunfv	|- ( ( [,] o. F ) Fn NN -> U_ x e. NN ( ( [,] o. F ) ` x ) = U. ran ( [,] o. F ) )
57	55 56	syl	|- ( ph -> U_ x e. NN ( ( [,] o. F ) ` x ) = U. ran ( [,] o. F ) )
58	38 50 57	3sstr3d	|- ( ph -> U. ran ( (,) o. F ) C_ U. ran ( [,] o. F ) )
59		ovolss	|- ( ( U. ran ( (,) o. F ) C_ U. ran ( [,] o. F ) /\ U. ran ( [,] o. F ) C_ RR ) -> ( vol* ` U. ran ( (,) o. F ) ) <_ ( vol* ` U. ran ( [,] o. F ) ) )
60	58 5 59	syl2anc	|- ( ph -> ( vol* ` U. ran ( (,) o. F ) ) <_ ( vol* ` U. ran ( [,] o. F ) ) )
61	19 60	eqbrtrrd	|- ( ph -> sup ( ran S , RR* , < ) <_ ( vol* ` U. ran ( [,] o. F ) ) )
62	7 15 18 61	xrletrid	|- ( ph -> ( vol* ` U. ran ( [,] o. F ) ) = sup ( ran S , RR* , < ) )