| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | carageniuncl.o | . 2
⊢ (𝜑 → 𝑂 ∈ OutMeas) | 
| 2 |  | eqid 2736 | . 2
⊢ ∪ dom 𝑂 = ∪ dom 𝑂 | 
| 3 |  | carageniuncl.s | . 2
⊢ 𝑆 = (CaraGen‘𝑂) | 
| 4 |  | carageniuncl.e | . . . . . . . 8
⊢ (𝜑 → 𝐸:𝑍⟶𝑆) | 
| 5 | 4 | ffvelcdmda 7103 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ 𝑆) | 
| 6 |  | elssuni 4936 | . . . . . . 7
⊢ ((𝐸‘𝑛) ∈ 𝑆 → (𝐸‘𝑛) ⊆ ∪ 𝑆) | 
| 7 | 5, 6 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∪ 𝑆) | 
| 8 | 1, 3 | caragenuni 46531 | . . . . . . 7
⊢ (𝜑 → ∪ 𝑆 =
∪ dom 𝑂) | 
| 9 | 8 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑆 = ∪
dom 𝑂) | 
| 10 | 7, 9 | sseqtrd 4019 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∪ dom
𝑂) | 
| 11 | 10 | ralrimiva 3145 | . . . 4
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂) | 
| 12 |  | iunss 5044 | . . . 4
⊢ (∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂 ↔ ∀𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂) | 
| 13 | 11, 12 | sylibr 234 | . . 3
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂) | 
| 14 |  | carageniuncl.z | . . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 15 | 14 | fvexi 6919 | . . . . . 6
⊢ 𝑍 ∈ V | 
| 16 |  | fvex 6918 | . . . . . 6
⊢ (𝐸‘𝑛) ∈ V | 
| 17 | 15, 16 | iunex 7994 | . . . . 5
⊢ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ V | 
| 18 | 17 | a1i 11 | . . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ V) | 
| 19 |  | elpwg 4602 | . . . 4
⊢ (∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ V → (∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ 𝒫 ∪ dom 𝑂 ↔ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂)) | 
| 20 | 18, 19 | syl 17 | . . 3
⊢ (𝜑 → (∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ 𝒫 ∪ dom 𝑂 ↔ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂)) | 
| 21 | 13, 20 | mpbird 257 | . 2
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ 𝒫 ∪ dom 𝑂) | 
| 22 |  | iccssxr 13471 | . . . . 5
⊢
(0[,]+∞) ⊆ ℝ* | 
| 23 | 1 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → 𝑂 ∈ OutMeas) | 
| 24 |  | elpwi 4606 | . . . . . . . 8
⊢ (𝑎 ∈ 𝒫 ∪ dom 𝑂 → 𝑎 ⊆ ∪ dom
𝑂) | 
| 25 |  | ssinss1 4245 | . . . . . . . 8
⊢ (𝑎 ⊆ ∪ dom 𝑂 → (𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ⊆ ∪ dom
𝑂) | 
| 26 | 24, 25 | syl 17 | . . . . . . 7
⊢ (𝑎 ∈ 𝒫 ∪ dom 𝑂 → (𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ⊆ ∪ dom
𝑂) | 
| 27 | 26 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ⊆ ∪ dom
𝑂) | 
| 28 | 23, 2, 27 | omecl 46523 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈ (0[,]+∞)) | 
| 29 | 22, 28 | sselid 3980 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈
ℝ*) | 
| 30 | 24 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → 𝑎 ⊆ ∪ dom
𝑂) | 
| 31 | 30 | ssdifssd 4146 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ⊆ ∪ dom
𝑂) | 
| 32 | 23, 2, 31 | omecl 46523 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈ (0[,]+∞)) | 
| 33 | 22, 32 | sselid 3980 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈
ℝ*) | 
| 34 | 29, 33 | xaddcld 13344 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ∈
ℝ*) | 
| 35 | 23, 2, 30 | omecl 46523 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘𝑎) ∈ (0[,]+∞)) | 
| 36 | 22, 35 | sselid 3980 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘𝑎) ∈
ℝ*) | 
| 37 |  | pnfge 13173 | . . . . . . 7
⊢ (((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ∈ ℝ* →
((𝑂‘(𝑎 ∩ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ +∞) | 
| 38 | 34, 37 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ +∞) | 
| 39 | 38 | adantr 480 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) = +∞) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ +∞) | 
| 40 |  | id 22 | . . . . . . 7
⊢ ((𝑂‘𝑎) = +∞ → (𝑂‘𝑎) = +∞) | 
| 41 | 40 | eqcomd 2742 | . . . . . 6
⊢ ((𝑂‘𝑎) = +∞ → +∞ = (𝑂‘𝑎)) | 
| 42 | 41 | adantl 481 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) = +∞) → +∞ = (𝑂‘𝑎)) | 
| 43 | 39, 42 | breqtrd 5168 | . . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) = +∞) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎)) | 
| 44 |  | simpl 482 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → (𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂)) | 
| 45 |  | rge0ssre 13497 | . . . . . 6
⊢
(0[,)+∞) ⊆ ℝ | 
| 46 |  | 0xr 11309 | . . . . . . . 8
⊢ 0 ∈
ℝ* | 
| 47 | 46 | a1i 11 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → 0 ∈
ℝ*) | 
| 48 |  | pnfxr 11316 | . . . . . . . 8
⊢ +∞
∈ ℝ* | 
| 49 | 48 | a1i 11 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → +∞ ∈
ℝ*) | 
| 50 | 44, 35 | syl 17 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → (𝑂‘𝑎) ∈ (0[,]+∞)) | 
| 51 | 40 | necon3bi 2966 | . . . . . . . 8
⊢ (¬
(𝑂‘𝑎) = +∞ → (𝑂‘𝑎) ≠ +∞) | 
| 52 | 51 | adantl 481 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → (𝑂‘𝑎) ≠ +∞) | 
| 53 | 47, 49, 50, 52 | eliccelicod 45548 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → (𝑂‘𝑎) ∈ (0[,)+∞)) | 
| 54 | 45, 53 | sselid 3980 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → (𝑂‘𝑎) ∈ ℝ) | 
| 55 | 23 | ad2antrr 726 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑂 ∈
OutMeas) | 
| 56 | 30 | ad2antrr 726 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑎 ⊆ ∪ dom 𝑂) | 
| 57 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) → (𝑂‘𝑎) ∈ ℝ) | 
| 58 | 57 | adantr 480 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → (𝑂‘𝑎) ∈ ℝ) | 
| 59 |  | carageniuncl.3 | . . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 60 | 59 | ad3antrrr 730 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑀 ∈
ℤ) | 
| 61 | 4 | ad3antrrr 730 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝐸:𝑍⟶𝑆) | 
| 62 |  | simpr 484 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) | 
| 63 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑛 ∈ 𝑍 ↦ ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) = (𝑛 ∈ 𝑍 ↦ ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) | 
| 64 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝐸‘𝑚) = (𝐸‘𝑛)) | 
| 65 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (𝑀..^𝑚) = (𝑀..^𝑛)) | 
| 66 | 65 | iuneq1d 5018 | . . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ∪
𝑖 ∈ (𝑀..^𝑚)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖)) | 
| 67 | 64, 66 | difeq12d 4126 | . . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((𝐸‘𝑚) ∖ ∪
𝑖 ∈ (𝑀..^𝑚)(𝐸‘𝑖)) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖))) | 
| 68 | 67 | cbvmptv 5254 | . . . . . . . 8
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝑚) ∖ ∪
𝑖 ∈ (𝑀..^𝑚)(𝐸‘𝑖))) = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖))) | 
| 69 | 55, 3, 2, 56, 58, 60, 14, 61, 62, 63, 68 | carageniuncllem2 46542 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝑎) + 𝑥)) | 
| 70 | 69 | ralrimiva 3145 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) → ∀𝑥 ∈ ℝ+
((𝑂‘(𝑎 ∩ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝑎) + 𝑥)) | 
| 71 | 34 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ∈
ℝ*) | 
| 72 |  | xralrple 13248 | . . . . . . 7
⊢ ((((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ∈ ℝ* ∧ (𝑂‘𝑎) ∈ ℝ) → (((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎) ↔ ∀𝑥 ∈ ℝ+ ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝑎) + 𝑥))) | 
| 73 | 71, 57, 72 | syl2anc 584 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) → (((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎) ↔ ∀𝑥 ∈ ℝ+ ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝑎) + 𝑥))) | 
| 74 | 70, 73 | mpbird 257 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎)) | 
| 75 | 44, 54, 74 | syl2anc 584 | . . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎)) | 
| 76 | 43, 75 | pm2.61dan 812 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎)) | 
| 77 | 23, 2, 30 | omelesplit 46538 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘𝑎) ≤ ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))))) | 
| 78 | 34, 36, 76, 77 | xrletrid 13198 | . 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) = (𝑂‘𝑎)) | 
| 79 | 1, 2, 3, 21, 78 | carageneld 46522 | 1
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ 𝑆) |