Step | Hyp | Ref
| Expression |
1 | | carageniuncl.o |
. 2
⊢ (𝜑 → 𝑂 ∈ OutMeas) |
2 | | eqid 2610 |
. 2
⊢ ∪ dom 𝑂 = ∪ dom 𝑂 |
3 | | carageniuncl.s |
. 2
⊢ 𝑆 = (CaraGen‘𝑂) |
4 | | carageniuncl.e |
. . . . . . . 8
⊢ (𝜑 → 𝐸:𝑍⟶𝑆) |
5 | 4 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ 𝑆) |
6 | | elssuni 4403 |
. . . . . . 7
⊢ ((𝐸‘𝑛) ∈ 𝑆 → (𝐸‘𝑛) ⊆ ∪ 𝑆) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∪ 𝑆) |
8 | 1, 3 | caragenuni 39401 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑆 =
∪ dom 𝑂) |
9 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑆 = ∪
dom 𝑂) |
10 | 7, 9 | sseqtrd 3604 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∪ dom
𝑂) |
11 | 10 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂) |
12 | | iunss 4497 |
. . . 4
⊢ (∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂 ↔ ∀𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂) |
13 | 11, 12 | sylibr 223 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂) |
14 | | carageniuncl.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
15 | | fvex 6113 |
. . . . . . 7
⊢
(ℤ≥‘𝑀) ∈ V |
16 | 14, 15 | eqeltri 2684 |
. . . . . 6
⊢ 𝑍 ∈ V |
17 | | fvex 6113 |
. . . . . 6
⊢ (𝐸‘𝑛) ∈ V |
18 | 16, 17 | iunex 7039 |
. . . . 5
⊢ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ V |
19 | 18 | a1i 11 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ V) |
20 | | elpwg 4116 |
. . . 4
⊢ (∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ V → (∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ 𝒫 ∪ dom 𝑂 ↔ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂)) |
21 | 19, 20 | syl 17 |
. . 3
⊢ (𝜑 → (∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ 𝒫 ∪ dom 𝑂 ↔ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ ∪ dom
𝑂)) |
22 | 13, 21 | mpbird 246 |
. 2
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ 𝒫 ∪ dom 𝑂) |
23 | | iccssxr 12127 |
. . . . 5
⊢
(0[,]+∞) ⊆ ℝ* |
24 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → 𝑂 ∈ OutMeas) |
25 | | elpwi 4117 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝒫 ∪ dom 𝑂 → 𝑎 ⊆ ∪ dom
𝑂) |
26 | | ssinss1 3803 |
. . . . . . . 8
⊢ (𝑎 ⊆ ∪ dom 𝑂 → (𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ⊆ ∪ dom
𝑂) |
27 | 25, 26 | syl 17 |
. . . . . . 7
⊢ (𝑎 ∈ 𝒫 ∪ dom 𝑂 → (𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ⊆ ∪ dom
𝑂) |
28 | 27 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ⊆ ∪ dom
𝑂) |
29 | 24, 2, 28 | omecl 39393 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈ (0[,]+∞)) |
30 | 23, 29 | sseldi 3566 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈
ℝ*) |
31 | 25 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → 𝑎 ⊆ ∪ dom
𝑂) |
32 | 31 | ssdifssd 3710 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ⊆ ∪ dom
𝑂) |
33 | 24, 2, 32 | omecl 39393 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈ (0[,]+∞)) |
34 | 23, 33 | sseldi 3566 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈
ℝ*) |
35 | 30, 34 | xaddcld 12003 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ∈
ℝ*) |
36 | 24, 2, 31 | omecl 39393 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘𝑎) ∈ (0[,]+∞)) |
37 | 23, 36 | sseldi 3566 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘𝑎) ∈
ℝ*) |
38 | | pnfge 11840 |
. . . . . . 7
⊢ (((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ∈ ℝ* →
((𝑂‘(𝑎 ∩ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ +∞) |
39 | 35, 38 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ +∞) |
40 | 39 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) = +∞) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ +∞) |
41 | | id 22 |
. . . . . . 7
⊢ ((𝑂‘𝑎) = +∞ → (𝑂‘𝑎) = +∞) |
42 | 41 | eqcomd 2616 |
. . . . . 6
⊢ ((𝑂‘𝑎) = +∞ → +∞ = (𝑂‘𝑎)) |
43 | 42 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) = +∞) → +∞ = (𝑂‘𝑎)) |
44 | 40, 43 | breqtrd 4609 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) = +∞) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎)) |
45 | | simpl 472 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → (𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂)) |
46 | | rge0ssre 12151 |
. . . . . 6
⊢
(0[,)+∞) ⊆ ℝ |
47 | | 0xr 9965 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
48 | 47 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → 0 ∈
ℝ*) |
49 | | pnfxr 9971 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
50 | 49 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → +∞ ∈
ℝ*) |
51 | 45, 36 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → (𝑂‘𝑎) ∈ (0[,]+∞)) |
52 | 41 | necon3bi 2808 |
. . . . . . . 8
⊢ (¬
(𝑂‘𝑎) = +∞ → (𝑂‘𝑎) ≠ +∞) |
53 | 52 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → (𝑂‘𝑎) ≠ +∞) |
54 | 48, 50, 51, 53 | eliccelicod 38604 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → (𝑂‘𝑎) ∈ (0[,)+∞)) |
55 | 46, 54 | sseldi 3566 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → (𝑂‘𝑎) ∈ ℝ) |
56 | 24 | ad2antrr 758 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑂 ∈
OutMeas) |
57 | 31 | ad2antrr 758 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑎 ⊆ ∪ dom 𝑂) |
58 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) → (𝑂‘𝑎) ∈ ℝ) |
59 | 58 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → (𝑂‘𝑎) ∈ ℝ) |
60 | | carageniuncl.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
61 | 60 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑀 ∈
ℤ) |
62 | 4 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝐸:𝑍⟶𝑆) |
63 | | simpr 476 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
64 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑍 ↦ ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) = (𝑛 ∈ 𝑍 ↦ ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) |
65 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝐸‘𝑚) = (𝐸‘𝑛)) |
66 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (𝑀..^𝑚) = (𝑀..^𝑛)) |
67 | 66 | iuneq1d 4481 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ∪
𝑖 ∈ (𝑀..^𝑚)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖)) |
68 | 65, 67 | difeq12d 3691 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((𝐸‘𝑚) ∖ ∪
𝑖 ∈ (𝑀..^𝑚)(𝐸‘𝑖)) = ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖))) |
69 | 68 | cbvmptv 4678 |
. . . . . . . 8
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝑚) ∖ ∪
𝑖 ∈ (𝑀..^𝑚)(𝐸‘𝑖))) = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖))) |
70 | 56, 3, 2, 57, 59, 61, 14, 62, 63, 64, 69 | carageniuncllem2 39412 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝑎) + 𝑥)) |
71 | 70 | ralrimiva 2949 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) → ∀𝑥 ∈ ℝ+
((𝑂‘(𝑎 ∩ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝑎) + 𝑥)) |
72 | 35 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ∈
ℝ*) |
73 | | xralrple 11910 |
. . . . . . 7
⊢ ((((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ∈ ℝ* ∧ (𝑂‘𝑎) ∈ ℝ) → (((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎) ↔ ∀𝑥 ∈ ℝ+ ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝑎) + 𝑥))) |
74 | 72, 58, 73 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) → (((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎) ↔ ∀𝑥 ∈ ℝ+ ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝑎) + 𝑥))) |
75 | 71, 74 | mpbird 246 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ (𝑂‘𝑎) ∈ ℝ) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎)) |
76 | 45, 55, 75 | syl2anc 691 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) ∧ ¬ (𝑂‘𝑎) = +∞) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎)) |
77 | 44, 76 | pm2.61dan 828 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (𝑂‘𝑎)) |
78 | 24, 2, 31 | omelesplit 39408 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘𝑎) ≤ ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))))) |
79 | 35, 37, 77, 78 | xrletrid 11862 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝑎 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) = (𝑂‘𝑎)) |
80 | 1, 2, 3, 22, 79 | carageneld 39392 |
1
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ 𝑆) |