Metamath Proof Explorer

Theorem caratheodorylem2

Description: Caratheodory's construction is sigma-additive. Main part of Step (e) in the proof of Theorem 113C of Fremlin1 p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses caratheodorylem2.o 
|- ( ph -> O e. OutMeas )
caratheodorylem2.x 
|- X = U. dom O
caratheodorylem2.s 
|- S = ( CaraGen ` O )
caratheodorylem2.e 
|- ( ph -> E : NN --> S )
caratheodorylem2.5 
|- ( ph -> Disj_ n e. NN ( E ` n ) )
caratheodorylem2.g 
|- G = ( k e. NN |-> U_ n e. ( 1 ... k ) ( E ` n ) )
Assertion caratheodorylem2 
|- ( ph -> ( O ` U_ n e. NN ( E ` n ) ) = ( sum^ ` ( n e. NN |-> ( O ` ( E ` n ) ) ) ) )

Proof

Step Hyp Ref Expression
1 caratheodorylem2.o 
 |-  ( ph -> O e. OutMeas )
2 caratheodorylem2.x 
 |-  X = U. dom O
3 caratheodorylem2.s 
 |-  S = ( CaraGen ` O )
4 caratheodorylem2.e 
 |-  ( ph -> E : NN --> S )
5 caratheodorylem2.5 
 |-  ( ph -> Disj_ n e. NN ( E ` n ) )
6 caratheodorylem2.g 
 |-  G = ( k e. NN |-> U_ n e. ( 1 ... k ) ( E ` n ) )
7 3 caragenss 
 |-  ( O e. OutMeas -> S C_ dom O )
8 1 7 syl 
 |-  ( ph -> S C_ dom O )
9 8 adantr 
 |-  ( ( ph /\ n e. NN ) -> S C_ dom O )
10 4 ffvelrnda 
 |-  ( ( ph /\ n e. NN ) -> ( E ` n ) e. S )
11 9 10 sseldd 
 |-  ( ( ph /\ n e. NN ) -> ( E ` n ) e. dom O )
12 elssuni 
 |-  ( ( E ` n ) e. dom O -> ( E ` n ) C_ U. dom O )
13 11 12 syl 
 |-  ( ( ph /\ n e. NN ) -> ( E ` n ) C_ U. dom O )
14 13 2 sseqtrrdi 
 |-  ( ( ph /\ n e. NN ) -> ( E ` n ) C_ X )
15 14 ralrimiva 
 |-  ( ph -> A. n e. NN ( E ` n ) C_ X )
16 iunss 
 |-  ( U_ n e. NN ( E ` n ) C_ X <-> A. n e. NN ( E ` n ) C_ X )
17 15 16 sylibr 
 |-  ( ph -> U_ n e. NN ( E ` n ) C_ X )
18 1 2 17 omexrcl 
 |-  ( ph -> ( O ` U_ n e. NN ( E ` n ) ) e. RR* )
19 nnex 
 |-  NN e. _V
20 19 a1i 
 |-  ( ph -> NN e. _V )
21 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> O e. OutMeas )
22 21 2 14 omecl 
 |-  ( ( ph /\ n e. NN ) -> ( O ` ( E ` n ) ) e. ( 0 [,] +oo ) )
23 eqid 
 |-  ( n e. NN |-> ( O ` ( E ` n ) ) ) = ( n e. NN |-> ( O ` ( E ` n ) ) )
24 22 23 fmptd 
 |-  ( ph -> ( n e. NN |-> ( O ` ( E ` n ) ) ) : NN --> ( 0 [,] +oo ) )
25 20 24 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( n e. NN |-> ( O ` ( E ` n ) ) ) ) e. RR* )
26 nfv 
 |-  F/ n ph
27 nfcv 
 |-  F/_ n E
28 nnuz 
 |-  NN = ( ZZ>= ` 1 )
29 1 2 3 caragensspw 
 |-  ( ph -> S C_ ~P X )
30 4 29 fssd 
 |-  ( ph -> E : NN --> ~P X )
31 26 27 1 2 28 30 omeiunle 
 |-  ( ph -> ( O ` U_ n e. NN ( E ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( O ` ( E ` n ) ) ) ) )
32 elpwinss 
 |-  ( x e. ( ~P NN i^i Fin ) -> x C_ NN )
33 32 resmptd 
 |-  ( x e. ( ~P NN i^i Fin ) -> ( ( n e. NN |-> ( O ` ( E ` n ) ) ) |` x ) = ( n e. x |-> ( O ` ( E ` n ) ) ) )
34 33 fveq2d 
 |-  ( x e. ( ~P NN i^i Fin ) -> ( sum^ ` ( ( n e. NN |-> ( O ` ( E ` n ) ) ) |` x ) ) = ( sum^ ` ( n e. x |-> ( O ` ( E ` n ) ) ) ) )
35 34 adantl 
 |-  ( ( ph /\ x e. ( ~P NN i^i Fin ) ) -> ( sum^ ` ( ( n e. NN |-> ( O ` ( E ` n ) ) ) |` x ) ) = ( sum^ ` ( n e. x |-> ( O ` ( E ` n ) ) ) ) )
36 1zzd 
 |-  ( ( ph /\ x e. ( ~P NN i^i Fin ) ) -> 1 e. ZZ )
37 32 adantl 
 |-  ( ( ph /\ x e. ( ~P NN i^i Fin ) ) -> x C_ NN )
38 elinel2 
 |-  ( x e. ( ~P NN i^i Fin ) -> x e. Fin )
39 38 adantl 
 |-  ( ( ph /\ x e. ( ~P NN i^i Fin ) ) -> x e. Fin )
40 36 28 37 39 uzfissfz 
 |-  ( ( ph /\ x e. ( ~P NN i^i Fin ) ) -> E. k e. NN x C_ ( 1 ... k ) )
41 vex 
 |-  x e. _V
42 41 a1i 
 |-  ( ( ph /\ x C_ ( 1 ... k ) ) -> x e. _V )
43 1 ad2antrr 
 |-  ( ( ( ph /\ x C_ ( 1 ... k ) ) /\ n e. x ) -> O e. OutMeas )
44 30 ad2antrr 
 |-  ( ( ( ph /\ x C_ ( 1 ... k ) ) /\ n e. x ) -> E : NN --> ~P X )
45 fz1ssnn 
 |-  ( 1 ... k ) C_ NN
46 ssel2 
 |-  ( ( x C_ ( 1 ... k ) /\ n e. x ) -> n e. ( 1 ... k ) )
47 45 46 sselid 
 |-  ( ( x C_ ( 1 ... k ) /\ n e. x ) -> n e. NN )
48 47 adantll 
 |-  ( ( ( ph /\ x C_ ( 1 ... k ) ) /\ n e. x ) -> n e. NN )
49 44 48 ffvelrnd 
 |-  ( ( ( ph /\ x C_ ( 1 ... k ) ) /\ n e. x ) -> ( E ` n ) e. ~P X )
50 elpwi 
 |-  ( ( E ` n ) e. ~P X -> ( E ` n ) C_ X )
51 49 50 syl 
 |-  ( ( ( ph /\ x C_ ( 1 ... k ) ) /\ n e. x ) -> ( E ` n ) C_ X )
52 43 2 51 omecl 
 |-  ( ( ( ph /\ x C_ ( 1 ... k ) ) /\ n e. x ) -> ( O ` ( E ` n ) ) e. ( 0 [,] +oo ) )
53 eqid 
 |-  ( n e. x |-> ( O ` ( E ` n ) ) ) = ( n e. x |-> ( O ` ( E ` n ) ) )
54 52 53 fmptd 
 |-  ( ( ph /\ x C_ ( 1 ... k ) ) -> ( n e. x |-> ( O ` ( E ` n ) ) ) : x --> ( 0 [,] +oo ) )
55 42 54 sge0xrcl 
 |-  ( ( ph /\ x C_ ( 1 ... k ) ) -> ( sum^ ` ( n e. x |-> ( O ` ( E ` n ) ) ) ) e. RR* )
56 55 3adant2 
 |-  ( ( ph /\ k e. NN /\ x C_ ( 1 ... k ) ) -> ( sum^ ` ( n e. x |-> ( O ` ( E ` n ) ) ) ) e. RR* )
57 ovex 
 |-  ( 1 ... k ) e. _V
58 57 a1i 
 |-  ( ph -> ( 1 ... k ) e. _V )
59 elfznn 
 |-  ( n e. ( 1 ... k ) -> n e. NN )
60 59 22 sylan2 
 |-  ( ( ph /\ n e. ( 1 ... k ) ) -> ( O ` ( E ` n ) ) e. ( 0 [,] +oo ) )
61 eqid 
 |-  ( n e. ( 1 ... k ) |-> ( O ` ( E ` n ) ) ) = ( n e. ( 1 ... k ) |-> ( O ` ( E ` n ) ) )
62 60 61 fmptd 
 |-  ( ph -> ( n e. ( 1 ... k ) |-> ( O ` ( E ` n ) ) ) : ( 1 ... k ) --> ( 0 [,] +oo ) )
63 58 62 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( n e. ( 1 ... k ) |-> ( O ` ( E ` n ) ) ) ) e. RR* )
64 63 3ad2ant1 
 |-  ( ( ph /\ k e. NN /\ x C_ ( 1 ... k ) ) -> ( sum^ ` ( n e. ( 1 ... k ) |-> ( O ` ( E ` n ) ) ) ) e. RR* )
65 18 3ad2ant1 
 |-  ( ( ph /\ k e. NN /\ x C_ ( 1 ... k ) ) -> ( O ` U_ n e. NN ( E ` n ) ) e. RR* )
66 57 a1i 
 |-  ( ( ph /\ k e. NN /\ x C_ ( 1 ... k ) ) -> ( 1 ... k ) e. _V )
67 simpl1 
 |-  ( ( ( ph /\ k e. NN /\ x C_ ( 1 ... k ) ) /\ n e. ( 1 ... k ) ) -> ph )
68 59 adantl 
 |-  ( ( ( ph /\ k e. NN /\ x C_ ( 1 ... k ) ) /\ n e. ( 1 ... k ) ) -> n e. NN )
69 67 68 22 syl2anc 
 |-  ( ( ( ph /\ k e. NN /\ x C_ ( 1 ... k ) ) /\ n e. ( 1 ... k ) ) -> ( O ` ( E ` n ) ) e. ( 0 [,] +oo ) )
70 simp3 
 |-  ( ( ph /\ k e. NN /\ x C_ ( 1 ... k ) ) -> x C_ ( 1 ... k ) )
71 66 69 70 sge0lessmpt 
 |-  ( ( ph /\ k e. NN /\ x C_ ( 1 ... k ) ) -> ( sum^ ` ( n e. x |-> ( O ` ( E ` n ) ) ) ) <_ ( sum^ ` ( n e. ( 1 ... k ) |-> ( O ` ( E ` n ) ) ) ) )
72 1 adantr 
 |-  ( ( ph /\ k e. NN ) -> O e. OutMeas )
73 4 adantr 
 |-  ( ( ph /\ k e. NN ) -> E : NN --> S )
74 5 adantr 
 |-  ( ( ph /\ k e. NN ) -> Disj_ n e. NN ( E ` n ) )
75 nfiu1 
 |-  F/_ n U_ n e. ( 1 ... k ) ( E ` n )
76 nfcv 
 |-  F/_ k U_ m e. ( 1 ... n ) ( E ` m )
77 fveq2 
 |-  ( n = m -> ( E ` n ) = ( E ` m ) )
78 77 cbviunv 
 |-  U_ n e. ( 1 ... k ) ( E ` n ) = U_ m e. ( 1 ... k ) ( E ` m )
79 78 a1i 
 |-  ( k = n -> U_ n e. ( 1 ... k ) ( E ` n ) = U_ m e. ( 1 ... k ) ( E ` m ) )
80 oveq2 
 |-  ( k = n -> ( 1 ... k ) = ( 1 ... n ) )
81 80 iuneq1d 
 |-  ( k = n -> U_ m e. ( 1 ... k ) ( E ` m ) = U_ m e. ( 1 ... n ) ( E ` m ) )
82 79 81 eqtrd 
 |-  ( k = n -> U_ n e. ( 1 ... k ) ( E ` n ) = U_ m e. ( 1 ... n ) ( E ` m ) )
83 75 76 82 cbvmpt 
 |-  ( k e. NN |-> U_ n e. ( 1 ... k ) ( E ` n ) ) = ( n e. NN |-> U_ m e. ( 1 ... n ) ( E ` m ) )
84 6 83 eqtri 
 |-  G = ( n e. NN |-> U_ m e. ( 1 ... n ) ( E ` m ) )
85 id 
 |-  ( k e. NN -> k e. NN )
86 85 28 eleqtrdi 
 |-  ( k e. NN -> k e. ( ZZ>= ` 1 ) )
87 86 adantl 
 |-  ( ( ph /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
88 72 3 28 73 74 84 87 caratheodorylem1 
 |-  ( ( ph /\ k e. NN ) -> ( O ` ( G ` k ) ) = ( sum^ ` ( n e. ( 1 ... k ) |-> ( O ` ( E ` n ) ) ) ) )
89 88 eqcomd 
 |-  ( ( ph /\ k e. NN ) -> ( sum^ ` ( n e. ( 1 ... k ) |-> ( O ` ( E ` n ) ) ) ) = ( O ` ( G ` k ) ) )
90 17 adantr 
 |-  ( ( ph /\ k e. NN ) -> U_ n e. NN ( E ` n ) C_ X )
91 fvex 
 |-  ( E ` n ) e. _V
92 57 91 iunex 
 |-  U_ n e. ( 1 ... k ) ( E ` n ) e. _V
93 6 fvmpt2 
 |-  ( ( k e. NN /\ U_ n e. ( 1 ... k ) ( E ` n ) e. _V ) -> ( G ` k ) = U_ n e. ( 1 ... k ) ( E ` n ) )
94 85 92 93 sylancl 
 |-  ( k e. NN -> ( G ` k ) = U_ n e. ( 1 ... k ) ( E ` n ) )
95 45 a1i 
 |-  ( k e. NN -> ( 1 ... k ) C_ NN )
96 iunss1 
 |-  ( ( 1 ... k ) C_ NN -> U_ n e. ( 1 ... k ) ( E ` n ) C_ U_ n e. NN ( E ` n ) )
97 95 96 syl 
 |-  ( k e. NN -> U_ n e. ( 1 ... k ) ( E ` n ) C_ U_ n e. NN ( E ` n ) )
98 94 97 eqsstrd 
 |-  ( k e. NN -> ( G ` k ) C_ U_ n e. NN ( E ` n ) )
99 98 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( G ` k ) C_ U_ n e. NN ( E ` n ) )
100 72 2 90 99 omessle 
 |-  ( ( ph /\ k e. NN ) -> ( O ` ( G ` k ) ) <_ ( O ` U_ n e. NN ( E ` n ) ) )
101 89 100 eqbrtrd 
 |-  ( ( ph /\ k e. NN ) -> ( sum^ ` ( n e. ( 1 ... k ) |-> ( O ` ( E ` n ) ) ) ) <_ ( O ` U_ n e. NN ( E ` n ) ) )
102 101 3adant3 
 |-  ( ( ph /\ k e. NN /\ x C_ ( 1 ... k ) ) -> ( sum^ ` ( n e. ( 1 ... k ) |-> ( O ` ( E ` n ) ) ) ) <_ ( O ` U_ n e. NN ( E ` n ) ) )
103 56 64 65 71 102 xrletrd 
 |-  ( ( ph /\ k e. NN /\ x C_ ( 1 ... k ) ) -> ( sum^ ` ( n e. x |-> ( O ` ( E ` n ) ) ) ) <_ ( O ` U_ n e. NN ( E ` n ) ) )
104 103 3exp 
 |-  ( ph -> ( k e. NN -> ( x C_ ( 1 ... k ) -> ( sum^ ` ( n e. x |-> ( O ` ( E ` n ) ) ) ) <_ ( O ` U_ n e. NN ( E ` n ) ) ) ) )
105 104 adantr 
 |-  ( ( ph /\ x e. ( ~P NN i^i Fin ) ) -> ( k e. NN -> ( x C_ ( 1 ... k ) -> ( sum^ ` ( n e. x |-> ( O ` ( E ` n ) ) ) ) <_ ( O ` U_ n e. NN ( E ` n ) ) ) ) )
106 105 rexlimdv 
 |-  ( ( ph /\ x e. ( ~P NN i^i Fin ) ) -> ( E. k e. NN x C_ ( 1 ... k ) -> ( sum^ ` ( n e. x |-> ( O ` ( E ` n ) ) ) ) <_ ( O ` U_ n e. NN ( E ` n ) ) ) )
107 40 106 mpd 
 |-  ( ( ph /\ x e. ( ~P NN i^i Fin ) ) -> ( sum^ ` ( n e. x |-> ( O ` ( E ` n ) ) ) ) <_ ( O ` U_ n e. NN ( E ` n ) ) )
108 35 107 eqbrtrd 
 |-  ( ( ph /\ x e. ( ~P NN i^i Fin ) ) -> ( sum^ ` ( ( n e. NN |-> ( O ` ( E ` n ) ) ) |` x ) ) <_ ( O ` U_ n e. NN ( E ` n ) ) )
109 108 ralrimiva 
 |-  ( ph -> A. x e. ( ~P NN i^i Fin ) ( sum^ ` ( ( n e. NN |-> ( O ` ( E ` n ) ) ) |` x ) ) <_ ( O ` U_ n e. NN ( E ` n ) ) )
110 20 24 18 sge0lefi 
 |-  ( ph -> ( ( sum^ ` ( n e. NN |-> ( O ` ( E ` n ) ) ) ) <_ ( O ` U_ n e. NN ( E ` n ) ) <-> A. x e. ( ~P NN i^i Fin ) ( sum^ ` ( ( n e. NN |-> ( O ` ( E ` n ) ) ) |` x ) ) <_ ( O ` U_ n e. NN ( E ` n ) ) ) )
111 109 110 mpbird 
 |-  ( ph -> ( sum^ ` ( n e. NN |-> ( O ` ( E ` n ) ) ) ) <_ ( O ` U_ n e. NN ( E ` n ) ) )
112 18 25 31 111 xrletrid 
 |-  ( ph -> ( O ` U_ n e. NN ( E ` n ) ) = ( sum^ ` ( n e. NN |-> ( O ` ( E ` n ) ) ) ) )