Theorem ovoliun

Description: The Lebesgue outer measure function is countably sub-additive. (Many books allow +oo as a value for one of the sets in the sum, but in our setup we can't do arithmetic on infinity, and in any case the volume of a union containing an infinitely large set is already infinitely large by monotonicity ovolss , so we need not consider this case here, although we do allow the sum itself to be infinite.) (Contributed by Mario Carneiro, 12-Jun-2014)

	Ref	Expression
Hypotheses	ovoliun.t	|- T = seq 1 ( + , G )
	ovoliun.g	|- G = ( n e. NN |-> ( vol* ` A ) )
	ovoliun.a	|- ( ( ph /\ n e. NN ) -> A C_ RR )
	ovoliun.v	|- ( ( ph /\ n e. NN ) -> ( vol* ` A ) e. RR )
Assertion	ovoliun	|- ( ph -> ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) )

Proof

Step	Hyp	Ref	Expression
1		ovoliun.t	|- T = seq 1 ( + , G )
2		ovoliun.g	|- G = ( n e. NN |-> ( vol* ` A ) )
3		ovoliun.a	|- ( ( ph /\ n e. NN ) -> A C_ RR )
4		ovoliun.v	|- ( ( ph /\ n e. NN ) -> ( vol* ` A ) e. RR )
5		mnfxr	|- -oo e. RR*
6	5	a1i	|- ( ph -> -oo e. RR* )
7		nnuz	|- NN = ( ZZ>= ` 1 )
8		1zzd	|- ( ph -> 1 e. ZZ )
9	4 2	fmptd	|- ( ph -> G : NN --> RR )
10	9	ffvelrnda	|- ( ( ph /\ k e. NN ) -> ( G ` k ) e. RR )
11	7 8 10	serfre	|- ( ph -> seq 1 ( + , G ) : NN --> RR )
12	1	feq1i	|- ( T : NN --> RR <-> seq 1 ( + , G ) : NN --> RR )
13	11 12	sylibr	|- ( ph -> T : NN --> RR )
14		1nn	|- 1 e. NN
15		ffvelrn	|- ( ( T : NN --> RR /\ 1 e. NN ) -> ( T ` 1 ) e. RR )
16	13 14 15	sylancl	|- ( ph -> ( T ` 1 ) e. RR )
17	16	rexrd	|- ( ph -> ( T ` 1 ) e. RR* )
18	13	frnd	|- ( ph -> ran T C_ RR )
19		ressxr	|- RR C_ RR*
20	18 19	sstrdi	|- ( ph -> ran T C_ RR* )
21		supxrcl	|- ( ran T C_ RR* -> sup ( ran T , RR* , < ) e. RR* )
22	20 21	syl	|- ( ph -> sup ( ran T , RR* , < ) e. RR* )
23	16	mnfltd	|- ( ph -> -oo < ( T ` 1 ) )
24	13	ffnd	|- ( ph -> T Fn NN )
25		fnfvelrn	|- ( ( T Fn NN /\ 1 e. NN ) -> ( T ` 1 ) e. ran T )
26	24 14 25	sylancl	|- ( ph -> ( T ` 1 ) e. ran T )
27		supxrub	|- ( ( ran T C_ RR* /\ ( T ` 1 ) e. ran T ) -> ( T ` 1 ) <_ sup ( ran T , RR* , < ) )
28	20 26 27	syl2anc	|- ( ph -> ( T ` 1 ) <_ sup ( ran T , RR* , < ) )
29	6 17 22 23 28	xrltletrd	|- ( ph -> -oo < sup ( ran T , RR* , < ) )
30		xrrebnd	|- ( sup ( ran T , RR* , < ) e. RR* -> ( sup ( ran T , RR* , < ) e. RR <-> ( -oo < sup ( ran T , RR* , < ) /\ sup ( ran T , RR* , < ) < +oo ) ) )
31	22 30	syl	|- ( ph -> ( sup ( ran T , RR* , < ) e. RR <-> ( -oo < sup ( ran T , RR* , < ) /\ sup ( ran T , RR* , < ) < +oo ) ) )
32	29 31	mpbirand	|- ( ph -> ( sup ( ran T , RR* , < ) e. RR <-> sup ( ran T , RR* , < ) < +oo ) )
33		nfcv	|- F/_ m A
34		nfcsb1v	|- F/_ n [_ m / n ]_ A
35		csbeq1a	|- ( n = m -> A = [_ m / n ]_ A )
36	33 34 35	cbviun	|- U_ n e. NN A = U_ m e. NN [_ m / n ]_ A
37	36	fveq2i	|- ( vol* ` U_ n e. NN A ) = ( vol* ` U_ m e. NN [_ m / n ]_ A )
38		nfcv	|- F/_ m ( vol* ` A )
39		nfcv	|- F/_ n vol*
40	39 34	nffv	|- F/_ n ( vol* ` [_ m / n ]_ A )
41	35	fveq2d	|- ( n = m -> ( vol* ` A ) = ( vol* ` [_ m / n ]_ A ) )
42	38 40 41	cbvmpt	|- ( n e. NN |-> ( vol* ` A ) ) = ( m e. NN |-> ( vol* ` [_ m / n ]_ A ) )
43	2 42	eqtri	|- G = ( m e. NN |-> ( vol* ` [_ m / n ]_ A ) )
44	3	ralrimiva	|- ( ph -> A. n e. NN A C_ RR )
45		nfv	|- F/ m A C_ RR
46		nfcv	|- F/_ n RR
47	34 46	nfss	|- F/ n [_ m / n ]_ A C_ RR
48	35	sseq1d	|- ( n = m -> ( A C_ RR <-> [_ m / n ]_ A C_ RR ) )
49	45 47 48	cbvralw	|- ( A. n e. NN A C_ RR <-> A. m e. NN [_ m / n ]_ A C_ RR )
50	44 49	sylib	|- ( ph -> A. m e. NN [_ m / n ]_ A C_ RR )
51	50	ad2antrr	|- ( ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) /\ x e. RR+ ) -> A. m e. NN [_ m / n ]_ A C_ RR )
52	51	r19.21bi	|- ( ( ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) /\ x e. RR+ ) /\ m e. NN ) -> [_ m / n ]_ A C_ RR )
53	4	ralrimiva	|- ( ph -> A. n e. NN ( vol* ` A ) e. RR )
54	38	nfel1	|- F/ m ( vol* ` A ) e. RR
55	40	nfel1	|- F/ n ( vol* ` [_ m / n ]_ A ) e. RR
56	41	eleq1d	|- ( n = m -> ( ( vol* ` A ) e. RR <-> ( vol* ` [_ m / n ]_ A ) e. RR ) )
57	54 55 56	cbvralw	|- ( A. n e. NN ( vol* ` A ) e. RR <-> A. m e. NN ( vol* ` [_ m / n ]_ A ) e. RR )
58	53 57	sylib	|- ( ph -> A. m e. NN ( vol* ` [_ m / n ]_ A ) e. RR )
59	58	ad2antrr	|- ( ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) /\ x e. RR+ ) -> A. m e. NN ( vol* ` [_ m / n ]_ A ) e. RR )
60	59	r19.21bi	|- ( ( ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) /\ x e. RR+ ) /\ m e. NN ) -> ( vol* ` [_ m / n ]_ A ) e. RR )
61		simplr	|- ( ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) /\ x e. RR+ ) -> sup ( ran T , RR* , < ) e. RR )
62		simpr	|- ( ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) /\ x e. RR+ ) -> x e. RR+ )
63	1 43 52 60 61 62	ovoliunlem3	|- ( ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) /\ x e. RR+ ) -> ( vol* ` U_ m e. NN [_ m / n ]_ A ) <_ ( sup ( ran T , RR* , < ) + x ) )
64	37 63	eqbrtrid	|- ( ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) /\ x e. RR+ ) -> ( vol* ` U_ n e. NN A ) <_ ( sup ( ran T , RR* , < ) + x ) )
65	64	ralrimiva	|- ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) -> A. x e. RR+ ( vol* ` U_ n e. NN A ) <_ ( sup ( ran T , RR* , < ) + x ) )
66		iunss	|- ( U_ n e. NN A C_ RR <-> A. n e. NN A C_ RR )
67	44 66	sylibr	|- ( ph -> U_ n e. NN A C_ RR )
68		ovolcl	|- ( U_ n e. NN A C_ RR -> ( vol* ` U_ n e. NN A ) e. RR* )
69	67 68	syl	|- ( ph -> ( vol* ` U_ n e. NN A ) e. RR* )
70		xralrple	|- ( ( ( vol* ` U_ n e. NN A ) e. RR* /\ sup ( ran T , RR* , < ) e. RR ) -> ( ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) <-> A. x e. RR+ ( vol* ` U_ n e. NN A ) <_ ( sup ( ran T , RR* , < ) + x ) ) )
71	69 70	sylan	|- ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) -> ( ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) <-> A. x e. RR+ ( vol* ` U_ n e. NN A ) <_ ( sup ( ran T , RR* , < ) + x ) ) )
72	65 71	mpbird	|- ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) -> ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) )
73	72	ex	|- ( ph -> ( sup ( ran T , RR* , < ) e. RR -> ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) ) )
74	32 73	sylbird	|- ( ph -> ( sup ( ran T , RR* , < ) < +oo -> ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) ) )
75		nltpnft	|- ( sup ( ran T , RR* , < ) e. RR* -> ( sup ( ran T , RR* , < ) = +oo <-> -. sup ( ran T , RR* , < ) < +oo ) )
76	22 75	syl	|- ( ph -> ( sup ( ran T , RR* , < ) = +oo <-> -. sup ( ran T , RR* , < ) < +oo ) )
77		pnfge	|- ( ( vol* ` U_ n e. NN A ) e. RR* -> ( vol* ` U_ n e. NN A ) <_ +oo )
78	69 77	syl	|- ( ph -> ( vol* ` U_ n e. NN A ) <_ +oo )
79		breq2	|- ( sup ( ran T , RR* , < ) = +oo -> ( ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) <-> ( vol* ` U_ n e. NN A ) <_ +oo ) )
80	78 79	syl5ibrcom	|- ( ph -> ( sup ( ran T , RR* , < ) = +oo -> ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) ) )
81	76 80	sylbird	|- ( ph -> ( -. sup ( ran T , RR* , < ) < +oo -> ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) ) )
82	74 81	pm2.61d	|- ( ph -> ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) )