Metamath Proof Explorer


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 ffvelrnda
 |-  ( ( 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 sseldi
 |-  ( ( 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 sseldi
 |-  ( ( 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 sseldi
 |-  ( ( 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 sseldi
 |-  ( ( ( 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 )