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 ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
caratheodorylem2.x ⊢ 𝑋 = ∪ dom 𝑂
caratheodorylem2.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
caratheodorylem2.e ⊢ ( 𝜑 → 𝐸 : ℕ ⟶ 𝑆 )
caratheodorylem2.5 ⊢ ( 𝜑 → Disj 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) )
caratheodorylem2.g ⊢ 𝐺 = ( 𝑘 ∈ ℕ ↦ ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) )
Assertion caratheodorylem2 ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 caratheodorylem2.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2 caratheodorylem2.x ⊢ 𝑋 = ∪ dom 𝑂
3 caratheodorylem2.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
4 caratheodorylem2.e ⊢ ( 𝜑 → 𝐸 : ℕ ⟶ 𝑆 )
5 caratheodorylem2.5 ⊢ ( 𝜑 → Disj 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) )
6 caratheodorylem2.g ⊢ 𝐺 = ( 𝑘 ∈ ℕ ↦ ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) )
7 3 caragenss ⊢ ( 𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂 )
8 1 7 syl ⊢ ( 𝜑 → 𝑆 ⊆ dom 𝑂 )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑆 ⊆ dom 𝑂 )
10 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ‘ 𝑛 ) ∈ 𝑆 )
11 9 10 sseldd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ‘ 𝑛 ) ∈ dom 𝑂 )
12 elssuni ⊢ ( ( 𝐸 ‘ 𝑛 ) ∈ dom 𝑂 → ( 𝐸 ‘ 𝑛 ) ⊆ ∪ dom 𝑂 )
13 11 12 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ‘ 𝑛 ) ⊆ ∪ dom 𝑂 )
14 13 2 sseqtrrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
15 14 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
16 iunss ⊢ ( ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 ↔ ∀ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
17 15 16 sylibr ⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
18 1 2 17 omexrcl ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ* )
19 nnex ⊢ ℕ ∈ V
20 19 a1i ⊢ ( 𝜑 → ℕ ∈ V )
21 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑂 ∈ OutMeas )
22 21 2 14 omecl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
23 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
24 22 23 fmptd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
25 20 24 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ* )
26 nfv ⊢ Ⅎ 𝑛 𝜑
27 nfcv ⊢ Ⅎ 𝑛 𝐸
28 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
29 1 2 3 caragensspw ⊢ ( 𝜑 → 𝑆 ⊆ 𝒫 𝑋 )
30 4 29 fssd ⊢ ( 𝜑 → 𝐸 : ℕ ⟶ 𝒫 𝑋 )
31 26 27 1 2 28 30 omeiunle ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
32 elpwinss ⊢ ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) → 𝑥 ⊆ ℕ )
33 32 resmptd ⊢ ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑥 ) = ( 𝑛 ∈ 𝑥 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
34 33 fveq2d ⊢ ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) → ( Σ^ ‘ ( ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝑥 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
35 34 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( Σ^ ‘ ( ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝑥 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
36 1zzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → 1 ∈ ℤ )
37 32 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → 𝑥 ⊆ ℕ )
38 elinel2 ⊢ ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) → 𝑥 ∈ Fin )
39 38 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → 𝑥 ∈ Fin )
40 36 28 37 39 uzfissfz ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ∃ 𝑘 ∈ ℕ 𝑥 ⊆ ( 1 ... 𝑘 ) )
41 vex ⊢ 𝑥 ∈ V
42 41 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) → 𝑥 ∈ V )
43 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) ∧ 𝑛 ∈ 𝑥 ) → 𝑂 ∈ OutMeas )
44 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) ∧ 𝑛 ∈ 𝑥 ) → 𝐸 : ℕ ⟶ 𝒫 𝑋 )
45 fz1ssnn ⊢ ( 1 ... 𝑘 ) ⊆ ℕ
46 ssel2 ⊢ ( ( 𝑥 ⊆ ( 1 ... 𝑘 ) ∧ 𝑛 ∈ 𝑥 ) → 𝑛 ∈ ( 1 ... 𝑘 ) )
47 45 46 sselid ⊢ ( ( 𝑥 ⊆ ( 1 ... 𝑘 ) ∧ 𝑛 ∈ 𝑥 ) → 𝑛 ∈ ℕ )
48 47 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) ∧ 𝑛 ∈ 𝑥 ) → 𝑛 ∈ ℕ )
49 44 48 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) ∧ 𝑛 ∈ 𝑥 ) → ( 𝐸 ‘ 𝑛 ) ∈ 𝒫 𝑋 )
50 elpwi ⊢ ( ( 𝐸 ‘ 𝑛 ) ∈ 𝒫 𝑋 → ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
51 49 50 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) ∧ 𝑛 ∈ 𝑥 ) → ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
52 43 2 51 omecl ⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) ∧ 𝑛 ∈ 𝑥 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
53 eqid ⊢ ( 𝑛 ∈ 𝑥 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ 𝑥 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
54 52 53 fmptd ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) → ( 𝑛 ∈ 𝑥 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) : 𝑥 ⟶ ( 0 [,] +∞ ) )
55 42 54 sge0xrcl ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) → ( Σ^ ‘ ( 𝑛 ∈ 𝑥 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ* )
56 55 3adant2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) → ( Σ^ ‘ ( 𝑛 ∈ 𝑥 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ* )
57 ovex ⊢ ( 1 ... 𝑘 ) ∈ V
58 57 a1i ⊢ ( 𝜑 → ( 1 ... 𝑘 ) ∈ V )
59 elfznn ⊢ ( 𝑛 ∈ ( 1 ... 𝑘 ) → 𝑛 ∈ ℕ )
60 59 22 sylan2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
61 eqid ⊢ ( 𝑛 ∈ ( 1 ... 𝑘 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ( 1 ... 𝑘 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
62 60 61 fmptd ⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑘 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) : ( 1 ... 𝑘 ) ⟶ ( 0 [,] +∞ ) )
63 58 62 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ( 1 ... 𝑘 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ* )
64 63 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) → ( Σ^ ‘ ( 𝑛 ∈ ( 1 ... 𝑘 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ* )
65 18 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ* )
66 57 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) → ( 1 ... 𝑘 ) ∈ V )
67 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → 𝜑 )
68 59 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → 𝑛 ∈ ℕ )
69 67 68 22 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
70 simp3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) → 𝑥 ⊆ ( 1 ... 𝑘 ) )
71 66 69 70 sge0lessmpt ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) → ( Σ^ ‘ ( 𝑛 ∈ 𝑥 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ( 1 ... 𝑘 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
72 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑂 ∈ OutMeas )
73 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐸 : ℕ ⟶ 𝑆 )
74 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Disj 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) )
75 nfiu1 ⊢ Ⅎ 𝑛 ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐸 ‘ 𝑛 )
76 nfcv ⊢ Ⅎ 𝑘 ∪ 𝑚 ∈ ( 1 ... 𝑛 ) ( 𝐸 ‘ 𝑚 )
77 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑚 ) )
78 77 cbviunv ⊢ ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) = ∪ 𝑚 ∈ ( 1 ... 𝑘 ) ( 𝐸 ‘ 𝑚 )
79 78 a1i ⊢ ( 𝑘 = 𝑛 → ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) = ∪ 𝑚 ∈ ( 1 ... 𝑘 ) ( 𝐸 ‘ 𝑚 ) )
80 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 1 ... 𝑘 ) = ( 1 ... 𝑛 ) )
81 80 iuneq1d ⊢ ( 𝑘 = 𝑛 → ∪ 𝑚 ∈ ( 1 ... 𝑘 ) ( 𝐸 ‘ 𝑚 ) = ∪ 𝑚 ∈ ( 1 ... 𝑛 ) ( 𝐸 ‘ 𝑚 ) )
82 79 81 eqtrd ⊢ ( 𝑘 = 𝑛 → ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) = ∪ 𝑚 ∈ ( 1 ... 𝑛 ) ( 𝐸 ‘ 𝑚 ) )
83 75 76 82 cbvmpt ⊢ ( 𝑘 ∈ ℕ ↦ ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ∪ 𝑚 ∈ ( 1 ... 𝑛 ) ( 𝐸 ‘ 𝑚 ) )
84 6 83 eqtri ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ∪ 𝑚 ∈ ( 1 ... 𝑛 ) ( 𝐸 ‘ 𝑚 ) )
85 id ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ )
86 85 28 eleqtrdi ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
87 86 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
88 72 3 28 73 74 84 87 caratheodorylem1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑂 ‘ ( 𝐺 ‘ 𝑘 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 1 ... 𝑘 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
89 88 eqcomd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( Σ^ ‘ ( 𝑛 ∈ ( 1 ... 𝑘 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = ( 𝑂 ‘ ( 𝐺 ‘ 𝑘 ) ) )
90 17 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
91 fvex ⊢ ( 𝐸 ‘ 𝑛 ) ∈ V
92 57 91 iunex ⊢ ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) ∈ V
93 6 fvmpt2 ⊢ ( ( 𝑘 ∈ ℕ ∧ ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) ∈ V ) → ( 𝐺 ‘ 𝑘 ) = ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) )
94 85 92 93 sylancl ⊢ ( 𝑘 ∈ ℕ → ( 𝐺 ‘ 𝑘 ) = ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) )
95 45 a1i ⊢ ( 𝑘 ∈ ℕ → ( 1 ... 𝑘 ) ⊆ ℕ )
96 iunss1 ⊢ ( ( 1 ... 𝑘 ) ⊆ ℕ → ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) ⊆ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) )
97 95 96 syl ⊢ ( 𝑘 ∈ ℕ → ∪ 𝑛 ∈ ( 1 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) ⊆ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) )
98 94 97 eqsstrd ⊢ ( 𝑘 ∈ ℕ → ( 𝐺 ‘ 𝑘 ) ⊆ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) )
99 98 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ⊆ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) )
100 72 2 90 99 omessle ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑂 ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) )
101 89 100 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( Σ^ ‘ ( 𝑛 ∈ ( 1 ... 𝑘 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) )
102 101 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) → ( Σ^ ‘ ( 𝑛 ∈ ( 1 ... 𝑘 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) )
103 56 64 65 71 102 xrletrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑥 ⊆ ( 1 ... 𝑘 ) ) → ( Σ^ ‘ ( 𝑛 ∈ 𝑥 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) )
104 103 3exp ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ → ( 𝑥 ⊆ ( 1 ... 𝑘 ) → ( Σ^ ‘ ( 𝑛 ∈ 𝑥 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) ) ) )
105 104 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( 𝑘 ∈ ℕ → ( 𝑥 ⊆ ( 1 ... 𝑘 ) → ( Σ^ ‘ ( 𝑛 ∈ 𝑥 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) ) ) )
106 105 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( ∃ 𝑘 ∈ ℕ 𝑥 ⊆ ( 1 ... 𝑘 ) → ( Σ^ ‘ ( 𝑛 ∈ 𝑥 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) ) )
107 40 106 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( Σ^ ‘ ( 𝑛 ∈ 𝑥 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) )
108 35 107 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( Σ^ ‘ ( ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑥 ) ) ≤ ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) )
109 108 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ( Σ^ ‘ ( ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑥 ) ) ≤ ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) )
110 20 24 18 sge0lefi ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) ↔ ∀ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ( Σ^ ‘ ( ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ↾ 𝑥 ) ) ≤ ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) ) )
111 109 110 mpbird ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) )
112 18 25 31 111 xrletrid ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )