Theorem omeiunle

Description: The outer measure of the indexed union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	omeiunle.nph	|- F/ n ph
	omeiunle.ne	|- F/_ n E
	omeiunle.o	|- ( ph -> O e. OutMeas )
	omeiunle.x	|- X = U. dom O
	omeiunle.z	|- Z = ( ZZ>= ` N )
	omeiunle.e	|- ( ph -> E : Z --> ~P X )
Assertion	omeiunle	|- ( ph -> ( O ` U_ n e. Z ( E ` n ) ) <_ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		omeiunle.nph	|- F/ n ph
2		omeiunle.ne	|- F/_ n E
3		omeiunle.o	|- ( ph -> O e. OutMeas )
4		omeiunle.x	|- X = U. dom O
5		omeiunle.z	|- Z = ( ZZ>= ` N )
6		omeiunle.e	|- ( ph -> E : Z --> ~P X )
7		iccssxr	|- ( 0 [,] +oo ) C_ RR*
8	6	ffvelrnda	|- ( ( ph /\ n e. Z ) -> ( E ` n ) e. ~P X )
9		elpwi	|- ( ( E ` n ) e. ~P X -> ( E ` n ) C_ X )
10	8 9	syl	|- ( ( ph /\ n e. Z ) -> ( E ` n ) C_ X )
11	10	ex	|- ( ph -> ( n e. Z -> ( E ` n ) C_ X ) )
12	1 11	ralrimi	|- ( ph -> A. n e. Z ( E ` n ) C_ X )
13		iunss	|- ( U_ n e. Z ( E ` n ) C_ X <-> A. n e. Z ( E ` n ) C_ X )
14	12 13	sylibr	|- ( ph -> U_ n e. Z ( E ` n ) C_ X )
15	3 4 14	omecl	|- ( ph -> ( O ` U_ n e. Z ( E ` n ) ) e. ( 0 [,] +oo ) )
16	7 15	sseldi	|- ( ph -> ( O ` U_ n e. Z ( E ` n ) ) e. RR* )
17	6	ffnd	|- ( ph -> E Fn Z )
18	5	fvexi	|- Z e. _V
19	18	a1i	|- ( ph -> Z e. _V )
20		fnex	|- ( ( E Fn Z /\ Z e. _V ) -> E e. _V )
21	17 19 20	syl2anc	|- ( ph -> E e. _V )
22		rnexg	|- ( E e. _V -> ran E e. _V )
23	21 22	syl	|- ( ph -> ran E e. _V )
24	3 4	omef	|- ( ph -> O : ~P X --> ( 0 [,] +oo ) )
25	6	frnd	|- ( ph -> ran E C_ ~P X )
26	24 25	fssresd	|- ( ph -> ( O |` ran E ) : ran E --> ( 0 [,] +oo ) )
27	23 26	sge0xrcl	|- ( ph -> ( sum^ ` ( O |` ran E ) ) e. RR* )
28	3	adantr	|- ( ( ph /\ n e. Z ) -> O e. OutMeas )
29	28 4 10	omecl	|- ( ( ph /\ n e. Z ) -> ( O ` ( E ` n ) ) e. ( 0 [,] +oo ) )
30		eqid	|- ( n e. Z |-> ( O ` ( E ` n ) ) ) = ( n e. Z |-> ( O ` ( E ` n ) ) )
31	1 29 30	fmptdf	|- ( ph -> ( n e. Z |-> ( O ` ( E ` n ) ) ) : Z --> ( 0 [,] +oo ) )
32	19 31	sge0xrcl	|- ( ph -> ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) e. RR* )
33		fvex	|- ( E ` n ) e. _V
34	33	rgenw	|- A. n e. Z ( E ` n ) e. _V
35		dfiun3g	|- ( A. n e. Z ( E ` n ) e. _V -> U_ n e. Z ( E ` n ) = U. ran ( n e. Z |-> ( E ` n ) ) )
36	34 35	ax-mp	|- U_ n e. Z ( E ` n ) = U. ran ( n e. Z |-> ( E ` n ) )
37	36	a1i	|- ( ph -> U_ n e. Z ( E ` n ) = U. ran ( n e. Z |-> ( E ` n ) ) )
38	6	feqmptd	|- ( ph -> E = ( m e. Z |-> ( E ` m ) ) )
39		nfcv	|- F/_ n m
40	2 39	nffv	|- F/_ n ( E ` m )
41		nfcv	|- F/_ m ( E ` n )
42		fveq2	|- ( m = n -> ( E ` m ) = ( E ` n ) )
43	40 41 42	cbvmpt	|- ( m e. Z |-> ( E ` m ) ) = ( n e. Z |-> ( E ` n ) )
44	43	a1i	|- ( ph -> ( m e. Z |-> ( E ` m ) ) = ( n e. Z |-> ( E ` n ) ) )
45	38 44	eqtrd	|- ( ph -> E = ( n e. Z |-> ( E ` n ) ) )
46	45	rneqd	|- ( ph -> ran E = ran ( n e. Z |-> ( E ` n ) ) )
47	46	unieqd	|- ( ph -> U. ran E = U. ran ( n e. Z |-> ( E ` n ) ) )
48	37 47	eqtr4d	|- ( ph -> U_ n e. Z ( E ` n ) = U. ran E )
49	48	fveq2d	|- ( ph -> ( O ` U_ n e. Z ( E ` n ) ) = ( O ` U. ran E ) )
50		fnrndomg	|- ( Z e. _V -> ( E Fn Z -> ran E ~<_ Z ) )
51	19 17 50	sylc	|- ( ph -> ran E ~<_ Z )
52	5	uzct	|- Z ~<_ _om
53	52	a1i	|- ( ph -> Z ~<_ _om )
54		domtr	|- ( ( ran E ~<_ Z /\ Z ~<_ _om ) -> ran E ~<_ _om )
55	51 53 54	syl2anc	|- ( ph -> ran E ~<_ _om )
56	3 4 25 55	omeunile	|- ( ph -> ( O ` U. ran E ) <_ ( sum^ ` ( O |` ran E ) ) )
57	49 56	eqbrtrd	|- ( ph -> ( O ` U_ n e. Z ( E ` n ) ) <_ ( sum^ ` ( O |` ran E ) ) )
58		ltweuz	|- < We ( ZZ>= ` N )
59		weeq2	|- ( Z = ( ZZ>= ` N ) -> ( < We Z <-> < We ( ZZ>= ` N ) ) )
60	5 59	ax-mp	|- ( < We Z <-> < We ( ZZ>= ` N ) )
61	58 60	mpbir	|- < We Z
62	61	a1i	|- ( ph -> < We Z )
63	19 24 6 62	sge0resrn	|- ( ph -> ( sum^ ` ( O |` ran E ) ) <_ ( sum^ ` ( O o. E ) ) )
64		fcompt	|- ( ( O : ~P X --> ( 0 [,] +oo ) /\ E : Z --> ~P X ) -> ( O o. E ) = ( m e. Z |-> ( O ` ( E ` m ) ) ) )
65		nfcv	|- F/_ n O
66	65 40	nffv	|- F/_ n ( O ` ( E ` m ) )
67		nfcv	|- F/_ m ( O ` ( E ` n ) )
68		2fveq3	|- ( m = n -> ( O ` ( E ` m ) ) = ( O ` ( E ` n ) ) )
69	66 67 68	cbvmpt	|- ( m e. Z |-> ( O ` ( E ` m ) ) ) = ( n e. Z |-> ( O ` ( E ` n ) ) )
70	69	a1i	|- ( ( O : ~P X --> ( 0 [,] +oo ) /\ E : Z --> ~P X ) -> ( m e. Z |-> ( O ` ( E ` m ) ) ) = ( n e. Z |-> ( O ` ( E ` n ) ) ) )
71	64 70	eqtrd	|- ( ( O : ~P X --> ( 0 [,] +oo ) /\ E : Z --> ~P X ) -> ( O o. E ) = ( n e. Z |-> ( O ` ( E ` n ) ) ) )
72	24 6 71	syl2anc	|- ( ph -> ( O o. E ) = ( n e. Z |-> ( O ` ( E ` n ) ) ) )
73	72	fveq2d	|- ( ph -> ( sum^ ` ( O o. E ) ) = ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) )
74	63 73	breqtrd	|- ( ph -> ( sum^ ` ( O |` ran E ) ) <_ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) )
75	16 27 32 57 74	xrletrd	|- ( ph -> ( O ` U_ n e. Z ( E ` n ) ) <_ ( sum^ ` ( n e. Z |-> ( O ` ( E ` n ) ) ) ) )