Theorem carageniuncl

Description: The Caratheodory's construction is closed under indexed countable union. Step (d) in the proof of Theorem 113C of Fremlin1 p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	carageniuncl.o	|- ( ph -> O e. OutMeas )
	carageniuncl.s	|- S = ( CaraGen ` O )
	carageniuncl.3	|- ( ph -> M e. ZZ )
	carageniuncl.z	|- Z = ( ZZ>= ` M )
	carageniuncl.e	|- ( ph -> E : Z --> S )
Assertion	carageniuncl	|- ( ph -> U_ n e. Z ( E ` n ) e. S )

Proof

Step	Hyp	Ref	Expression
1		carageniuncl.o	|- ( ph -> O e. OutMeas )
2		carageniuncl.s	|- S = ( CaraGen ` O )
3		carageniuncl.3	|- ( ph -> M e. ZZ )
4		carageniuncl.z	|- Z = ( ZZ>= ` M )
5		carageniuncl.e	|- ( ph -> E : Z --> S )
6		eqid	|- U. dom O = U. dom O
7	5	ffvelcdmda	|- ( ( ph /\ n e. Z ) -> ( E ` n ) e. S )
8		elssuni	|- ( ( E ` n ) e. S -> ( E ` n ) C_ U. S )
9	7 8	syl	|- ( ( ph /\ n e. Z ) -> ( E ` n ) C_ U. S )
10	1 2	caragenuni	|- ( ph -> U. S = U. dom O )
11	10	adantr	|- ( ( ph /\ n e. Z ) -> U. S = U. dom O )
12	9 11	sseqtrd	|- ( ( ph /\ n e. Z ) -> ( E ` n ) C_ U. dom O )
13	12	ralrimiva	|- ( ph -> A. n e. Z ( E ` n ) C_ U. dom O )
14		iunss	|- ( U_ n e. Z ( E ` n ) C_ U. dom O <-> A. n e. Z ( E ` n ) C_ U. dom O )
15	13 14	sylibr	|- ( ph -> U_ n e. Z ( E ` n ) C_ U. dom O )
16	4	fvexi	|- Z e. _V
17		fvex	|- ( E ` n ) e. _V
18	16 17	iunex	|- U_ n e. Z ( E ` n ) e. _V
19	18	a1i	|- ( ph -> U_ n e. Z ( E ` n ) e. _V )
20		elpwg	|- ( U_ n e. Z ( E ` n ) e. _V -> ( U_ n e. Z ( E ` n ) e. ~P U. dom O <-> U_ n e. Z ( E ` n ) C_ U. dom O ) )
21	19 20	syl	|- ( ph -> ( U_ n e. Z ( E ` n ) e. ~P U. dom O <-> U_ n e. Z ( E ` n ) C_ U. dom O ) )
22	15 21	mpbird	|- ( ph -> U_ n e. Z ( E ` n ) e. ~P U. dom O )
23		iccssxr	|- ( 0 [,] +oo ) C_ RR*
24	1	adantr	|- ( ( ph /\ a e. ~P U. dom O ) -> O e. OutMeas )
25		elpwi	|- ( a e. ~P U. dom O -> a C_ U. dom O )
26		ssinss1	|- ( a C_ U. dom O -> ( a i^i U_ n e. Z ( E ` n ) ) C_ U. dom O )
27	25 26	syl	|- ( a e. ~P U. dom O -> ( a i^i U_ n e. Z ( E ` n ) ) C_ U. dom O )
28	27	adantl	|- ( ( ph /\ a e. ~P U. dom O ) -> ( a i^i U_ n e. Z ( E ` n ) ) C_ U. dom O )
29	24 6 28	omecl	|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) e. ( 0 [,] +oo ) )
30	23 29	sselid	|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) e. RR* )
31	25	adantl	|- ( ( ph /\ a e. ~P U. dom O ) -> a C_ U. dom O )
32	31	ssdifssd	|- ( ( ph /\ a e. ~P U. dom O ) -> ( a \ U_ n e. Z ( E ` n ) ) C_ U. dom O )
33	24 6 32	omecl	|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) e. ( 0 [,] +oo ) )
34	23 33	sselid	|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) e. RR* )
35	30 34	xaddcld	|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) e. RR* )
36	24 6 31	omecl	|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` a ) e. ( 0 [,] +oo ) )
37	23 36	sselid	|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` a ) e. RR* )
38		pnfge	|- ( ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) e. RR* -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ +oo )
39	35 38	syl	|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ +oo )
40	39	adantr	|- ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) = +oo ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ +oo )
41		id	|- ( ( O ` a ) = +oo -> ( O ` a ) = +oo )
42	41	eqcomd	|- ( ( O ` a ) = +oo -> +oo = ( O ` a ) )
43	42	adantl	|- ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) = +oo ) -> +oo = ( O ` a ) )
44	40 43	breqtrd	|- ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) = +oo ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( O ` a ) )
45		simpl	|- ( ( ( ph /\ a e. ~P U. dom O ) /\ -. ( O ` a ) = +oo ) -> ( ph /\ a e. ~P U. dom O ) )
46		rge0ssre	|- ( 0 [,) +oo ) C_ RR
47		0xr	|- 0 e. RR*
48	47	a1i	|- ( ( ( ph /\ a e. ~P U. dom O ) /\ -. ( O ` a ) = +oo ) -> 0 e. RR* )
49		pnfxr	|- +oo e. RR*
50	49	a1i	|- ( ( ( ph /\ a e. ~P U. dom O ) /\ -. ( O ` a ) = +oo ) -> +oo e. RR* )
51	45 36	syl	|- ( ( ( ph /\ a e. ~P U. dom O ) /\ -. ( O ` a ) = +oo ) -> ( O ` a ) e. ( 0 [,] +oo ) )
52	41	necon3bi	|- ( -. ( O ` a ) = +oo -> ( O ` a ) =/= +oo )
53	52	adantl	|- ( ( ( ph /\ a e. ~P U. dom O ) /\ -. ( O ` a ) = +oo ) -> ( O ` a ) =/= +oo )
54	48 50 51 53	eliccelicod	|- ( ( ( ph /\ a e. ~P U. dom O ) /\ -. ( O ` a ) = +oo ) -> ( O ` a ) e. ( 0 [,) +oo ) )
55	46 54	sselid	|- ( ( ( ph /\ a e. ~P U. dom O ) /\ -. ( O ` a ) = +oo ) -> ( O ` a ) e. RR )
56	24	ad2antrr	|- ( ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) /\ x e. RR+ ) -> O e. OutMeas )
57	31	ad2antrr	|- ( ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) /\ x e. RR+ ) -> a C_ U. dom O )
58		simpr	|- ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) -> ( O ` a ) e. RR )
59	58	adantr	|- ( ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) /\ x e. RR+ ) -> ( O ` a ) e. RR )
60	3	ad3antrrr	|- ( ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) /\ x e. RR+ ) -> M e. ZZ )
61	5	ad3antrrr	|- ( ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) /\ x e. RR+ ) -> E : Z --> S )
62		simpr	|- ( ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) /\ x e. RR+ ) -> x e. RR+ )
63		eqid	|- ( n e. Z |-> U_ i e. ( M ... n ) ( E ` i ) ) = ( n e. Z |-> U_ i e. ( M ... n ) ( E ` i ) )
64		fveq2	|- ( m = n -> ( E ` m ) = ( E ` n ) )
65		oveq2	|- ( m = n -> ( M ..^ m ) = ( M ..^ n ) )
66	65	iuneq1d	|- ( m = n -> U_ i e. ( M ..^ m ) ( E ` i ) = U_ i e. ( M ..^ n ) ( E ` i ) )
67	64 66	difeq12d	|- ( m = n -> ( ( E ` m ) \ U_ i e. ( M ..^ m ) ( E ` i ) ) = ( ( E ` n ) \ U_ i e. ( M ..^ n ) ( E ` i ) ) )
68	67	cbvmptv	|- ( m e. Z |-> ( ( E ` m ) \ U_ i e. ( M ..^ m ) ( E ` i ) ) ) = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( M ..^ n ) ( E ` i ) ) )
69	56 2 6 57 59 60 4 61 62 63 68	carageniuncllem2	|- ( ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) /\ x e. RR+ ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( ( O ` a ) + x ) )
70	69	ralrimiva	|- ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) -> A. x e. RR+ ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( ( O ` a ) + x ) )
71	35	adantr	|- ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) e. RR* )
72		xralrple	|- ( ( ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) e. RR* /\ ( O ` a ) e. RR ) -> ( ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( O ` a ) <-> A. x e. RR+ ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( ( O ` a ) + x ) ) )
73	71 58 72	syl2anc	|- ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) -> ( ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( O ` a ) <-> A. x e. RR+ ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( ( O ` a ) + x ) ) )
74	70 73	mpbird	|- ( ( ( ph /\ a e. ~P U. dom O ) /\ ( O ` a ) e. RR ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( O ` a ) )
75	45 55 74	syl2anc	|- ( ( ( ph /\ a e. ~P U. dom O ) /\ -. ( O ` a ) = +oo ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( O ` a ) )
76	44 75	pm2.61dan	|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) <_ ( O ` a ) )
77	24 6 31	omelesplit	|- ( ( ph /\ a e. ~P U. dom O ) -> ( O ` a ) <_ ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) )
78	35 37 76 77	xrletrid	|- ( ( ph /\ a e. ~P U. dom O ) -> ( ( O ` ( a i^i U_ n e. Z ( E ` n ) ) ) +e ( O ` ( a \ U_ n e. Z ( E ` n ) ) ) ) = ( O ` a ) )
79	1 6 2 22 78	carageneld	|- ( ph -> U_ n e. Z ( E ` n ) e. S )