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		ffvelcdm	\|- ( ( 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* , < ) )

Metamath Proof Explorer

Theorem uniiccvol

Proof