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 ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
carageniuncl.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
carageniuncl.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
carageniuncl.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
carageniuncl.e ⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝑆 )
Assertion carageniuncl ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 carageniuncl.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2 carageniuncl.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
3 carageniuncl.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 carageniuncl.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5 carageniuncl.e ⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝑆 )
6 eqid ⊢ ∪ dom 𝑂 = ∪ dom 𝑂
7 5 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ∈ 𝑆 )
8 elssuni ⊢ ( ( 𝐸 ‘ 𝑛 ) ∈ 𝑆 → ( 𝐸 ‘ 𝑛 ) ⊆ ∪ 𝑆 )
9 7 8 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ∪ 𝑆 )
10 1 2 caragenuni ⊢ ( 𝜑 → ∪ 𝑆 = ∪ dom 𝑂 )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∪ 𝑆 = ∪ dom 𝑂 )
12 9 11 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ∪ dom 𝑂 )
13 12 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ ∪ dom 𝑂 )
14 iunss ⊢ ( ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ ∪ dom 𝑂 ↔ ∀ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ ∪ dom 𝑂 )
15 13 14 sylibr ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ ∪ dom 𝑂 )
16 4 fvexi ⊢ 𝑍 ∈ V
17 fvex ⊢ ( 𝐸 ‘ 𝑛 ) ∈ V
18 16 17 iunex ⊢ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ∈ V
19 18 a1i ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ∈ V )
20 elpwg ⊢ ( ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ∈ V → ( ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ∈ 𝒫 ∪ dom 𝑂 ↔ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ ∪ dom 𝑂 ) )
21 19 20 syl ⊢ ( 𝜑 → ( ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ∈ 𝒫 ∪ dom 𝑂 ↔ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ ∪ dom 𝑂 ) )
22 15 21 mpbird ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ∈ 𝒫 ∪ dom 𝑂 )
23 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
24 1 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → 𝑂 ∈ OutMeas )
25 elpwi ⊢ ( 𝑎 ∈ 𝒫 ∪ dom 𝑂 → 𝑎 ⊆ ∪ dom 𝑂 )
26 ssinss1 ⊢ ( 𝑎 ⊆ ∪ dom 𝑂 → ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ⊆ ∪ dom 𝑂 )
27 25 26 syl ⊢ ( 𝑎 ∈ 𝒫 ∪ dom 𝑂 → ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ⊆ ∪ dom 𝑂 )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ⊆ ∪ dom 𝑂 )
29 24 6 28 omecl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ∈ ( 0 [,] +∞ ) )
30 23 29 sselid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ∈ ℝ* )
31 25 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → 𝑎 ⊆ ∪ dom 𝑂 )
32 31 ssdifssd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ⊆ ∪ dom 𝑂 )
33 24 6 32 omecl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ∈ ( 0 [,] +∞ ) )
34 23 33 sselid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ∈ ℝ* )
35 30 34 xaddcld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ* )
36 24 6 31 omecl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑂 ‘ 𝑎 ) ∈ ( 0 [,] +∞ ) )
37 23 36 sselid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑂 ‘ 𝑎 ) ∈ ℝ* )
38 pnfge ⊢ ( ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ* → ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ +∞ )
39 35 38 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ +∞ )
40 39 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ 𝑎 ) = +∞ ) → ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ +∞ )
41 id ⊢ ( ( 𝑂 ‘ 𝑎 ) = +∞ → ( 𝑂 ‘ 𝑎 ) = +∞ )
42 41 eqcomd ⊢ ( ( 𝑂 ‘ 𝑎 ) = +∞ → +∞ = ( 𝑂 ‘ 𝑎 ) )
43 42 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ 𝑎 ) = +∞ ) → +∞ = ( 𝑂 ‘ 𝑎 ) )
44 40 43 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ 𝑎 ) = +∞ ) → ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( 𝑂 ‘ 𝑎 ) )
45 simpl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ¬ ( 𝑂 ‘ 𝑎 ) = +∞ ) → ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) )
46 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
47 0xr ⊢ 0 ∈ ℝ*
48 47 a1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ¬ ( 𝑂 ‘ 𝑎 ) = +∞ ) → 0 ∈ ℝ* )
49 pnfxr ⊢ +∞ ∈ ℝ*
50 49 a1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ¬ ( 𝑂 ‘ 𝑎 ) = +∞ ) → +∞ ∈ ℝ* )
51 45 36 syl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ¬ ( 𝑂 ‘ 𝑎 ) = +∞ ) → ( 𝑂 ‘ 𝑎 ) ∈ ( 0 [,] +∞ ) )
52 41 necon3bi ⊢ ( ¬ ( 𝑂 ‘ 𝑎 ) = +∞ → ( 𝑂 ‘ 𝑎 ) ≠ +∞ )
53 52 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ¬ ( 𝑂 ‘ 𝑎 ) = +∞ ) → ( 𝑂 ‘ 𝑎 ) ≠ +∞ )
54 48 50 51 53 eliccelicod ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ¬ ( 𝑂 ‘ 𝑎 ) = +∞ ) → ( 𝑂 ‘ 𝑎 ) ∈ ( 0 [,) +∞ ) )
55 46 54 sselid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ¬ ( 𝑂 ‘ 𝑎 ) = +∞ ) → ( 𝑂 ‘ 𝑎 ) ∈ ℝ )
56 24 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝑂 ∈ OutMeas )
57 31 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝑎 ⊆ ∪ dom 𝑂 )
58 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℝ ) → ( 𝑂 ‘ 𝑎 ) ∈ ℝ )
59 58 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑂 ‘ 𝑎 ) ∈ ℝ )
60 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
61 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝐸 : 𝑍 ⟶ 𝑆 )
62 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
63 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) = ( 𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) )
64 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐸 ‘ 𝑚 ) = ( 𝐸 ‘ 𝑛 ) )
65 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝑀 ..^ 𝑚 ) = ( 𝑀 ..^ 𝑛 ) )
66 65 iuneq1d ⊢ ( 𝑚 = 𝑛 → ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑚 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) )
67 64 66 difeq12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝐸 ‘ 𝑚 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑚 ) ( 𝐸 ‘ 𝑖 ) ) = ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
68 67 cbvmptv ⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑚 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑚 ) ( 𝐸 ‘ 𝑖 ) ) ) = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
69 56 2 6 57 59 60 4 61 62 63 68 carageniuncllem2 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( ( 𝑂 ‘ 𝑎 ) + 𝑥 ) )
70 69 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℝ ) → ∀ 𝑥 ∈ ℝ+ ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( ( 𝑂 ‘ 𝑎 ) + 𝑥 ) )
71 35 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℝ ) → ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ* )
72 xralrple ⊢ ( ( ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ* ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℝ ) → ( ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( 𝑂 ‘ 𝑎 ) ↔ ∀ 𝑥 ∈ ℝ+ ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( ( 𝑂 ‘ 𝑎 ) + 𝑥 ) ) )
73 71 58 72 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℝ ) → ( ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( 𝑂 ‘ 𝑎 ) ↔ ∀ 𝑥 ∈ ℝ+ ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( ( 𝑂 ‘ 𝑎 ) + 𝑥 ) ) )
74 70 73 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ 𝑎 ) ∈ ℝ ) → ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( 𝑂 ‘ 𝑎 ) )
75 45 55 74 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) ∧ ¬ ( 𝑂 ‘ 𝑎 ) = +∞ ) → ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( 𝑂 ‘ 𝑎 ) )
76 44 75 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( 𝑂 ‘ 𝑎 ) )
77 24 6 31 omelesplit ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( 𝑂 ‘ 𝑎 ) ≤ ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) )
78 35 37 76 77 xrletrid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂 ) → ( ( 𝑂 ‘ ( 𝑎 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝑎 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) = ( 𝑂 ‘ 𝑎 ) )
79 1 6 2 22 78 carageneld ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ∈ 𝑆 )