| Step | Hyp | Ref
| Expression |
| 1 | | caragendifcl.o |
. 2
⊢ (𝜑 → 𝑂 ∈ OutMeas) |
| 2 | | eqid 2737 |
. 2
⊢ ∪ dom 𝑂 = ∪ dom 𝑂 |
| 3 | | caragendifcl.s |
. 2
⊢ 𝑆 = (CaraGen‘𝑂) |
| 4 | 3 | caragenss 46519 |
. . . . . 6
⊢ (𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂) |
| 5 | 1, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ dom 𝑂) |
| 6 | 5 | unissd 4917 |
. . . 4
⊢ (𝜑 → ∪ 𝑆
⊆ ∪ dom 𝑂) |
| 7 | 6 | ssdifssd 4147 |
. . 3
⊢ (𝜑 → (∪ 𝑆
∖ 𝐸) ⊆ ∪ dom 𝑂) |
| 8 | 3 | fvexi 6920 |
. . . . . . 7
⊢ 𝑆 ∈ V |
| 9 | 8 | uniex 7761 |
. . . . . 6
⊢ ∪ 𝑆
∈ V |
| 10 | | difexg 5329 |
. . . . . 6
⊢ (∪ 𝑆
∈ V → (∪ 𝑆 ∖ 𝐸) ∈ V) |
| 11 | 9, 10 | ax-mp 5 |
. . . . 5
⊢ (∪ 𝑆
∖ 𝐸) ∈
V |
| 12 | 11 | a1i 11 |
. . . 4
⊢ (𝜑 → (∪ 𝑆
∖ 𝐸) ∈
V) |
| 13 | | elpwg 4603 |
. . . 4
⊢ ((∪ 𝑆
∖ 𝐸) ∈ V →
((∪ 𝑆 ∖ 𝐸) ∈ 𝒫 ∪ dom 𝑂 ↔ (∪ 𝑆 ∖ 𝐸) ⊆ ∪ dom
𝑂)) |
| 14 | 12, 13 | syl 17 |
. . 3
⊢ (𝜑 → ((∪ 𝑆
∖ 𝐸) ∈ 𝒫
∪ dom 𝑂 ↔ (∪ 𝑆 ∖ 𝐸) ⊆ ∪ dom
𝑂)) |
| 15 | 7, 14 | mpbird 257 |
. 2
⊢ (𝜑 → (∪ 𝑆
∖ 𝐸) ∈ 𝒫
∪ dom 𝑂) |
| 16 | | elpwi 4607 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝒫 ∪ dom 𝑂 → 𝑎 ⊆ ∪ dom
𝑂) |
| 17 | 16 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → 𝑎 ⊆ ∪ dom
𝑂) |
| 18 | 1, 3 | caragenuni 46526 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑆 =
∪ dom 𝑂) |
| 19 | 18 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝜑 → ∪ dom 𝑂 = ∪ 𝑆) |
| 20 | 19 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ∪ dom
𝑂 = ∪ 𝑆) |
| 21 | 17, 20 | sseqtrd 4020 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → 𝑎 ⊆ ∪ 𝑆) |
| 22 | | difin2 4301 |
. . . . . . 7
⊢ (𝑎 ⊆ ∪ 𝑆
→ (𝑎 ∖ 𝐸) = ((∪ 𝑆
∖ 𝐸) ∩ 𝑎)) |
| 23 | 21, 22 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ 𝐸) = ((∪ 𝑆 ∖ 𝐸) ∩ 𝑎)) |
| 24 | | incom 4209 |
. . . . . . 7
⊢ ((∪ 𝑆
∖ 𝐸) ∩ 𝑎) = (𝑎 ∩ (∪ 𝑆 ∖ 𝐸)) |
| 25 | 24 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((∪
𝑆 ∖ 𝐸) ∩ 𝑎) = (𝑎 ∩ (∪ 𝑆 ∖ 𝐸))) |
| 26 | 23, 25 | eqtr2d 2778 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∩ (∪ 𝑆 ∖ 𝐸)) = (𝑎 ∖ 𝐸)) |
| 27 | 26 | fveq2d 6910 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∩ (∪ 𝑆 ∖ 𝐸))) = (𝑂‘(𝑎 ∖ 𝐸))) |
| 28 | 21 | ssdifd 4145 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ 𝐸) ⊆ (∪
𝑆 ∖ 𝐸)) |
| 29 | | sscon 4143 |
. . . . . . . 8
⊢ ((𝑎 ∖ 𝐸) ⊆ (∪
𝑆 ∖ 𝐸) → (𝑎 ∖ (∪ 𝑆 ∖ 𝐸)) ⊆ (𝑎 ∖ (𝑎 ∖ 𝐸))) |
| 30 | 28, 29 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ (∪ 𝑆 ∖ 𝐸)) ⊆ (𝑎 ∖ (𝑎 ∖ 𝐸))) |
| 31 | | dfin4 4278 |
. . . . . . . . 9
⊢ (𝑎 ∩ 𝐸) = (𝑎 ∖ (𝑎 ∖ 𝐸)) |
| 32 | 31 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∩ 𝐸) = (𝑎 ∖ (𝑎 ∖ 𝐸))) |
| 33 | | eqimss2 4043 |
. . . . . . . 8
⊢ ((𝑎 ∩ 𝐸) = (𝑎 ∖ (𝑎 ∖ 𝐸)) → (𝑎 ∖ (𝑎 ∖ 𝐸)) ⊆ (𝑎 ∩ 𝐸)) |
| 34 | 32, 33 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ (𝑎 ∖ 𝐸)) ⊆ (𝑎 ∩ 𝐸)) |
| 35 | 30, 34 | sstrd 3994 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ (∪ 𝑆 ∖ 𝐸)) ⊆ (𝑎 ∩ 𝐸)) |
| 36 | | elinel1 4201 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑎 ∩ 𝐸) → 𝑥 ∈ 𝑎) |
| 37 | | elinel2 4202 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑎 ∩ 𝐸) → 𝑥 ∈ 𝐸) |
| 38 | | elndif 4133 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐸 → ¬ 𝑥 ∈ (∪ 𝑆 ∖ 𝐸)) |
| 39 | 37, 38 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑎 ∩ 𝐸) → ¬ 𝑥 ∈ (∪ 𝑆 ∖ 𝐸)) |
| 40 | 36, 39 | eldifd 3962 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑎 ∩ 𝐸) → 𝑥 ∈ (𝑎 ∖ (∪ 𝑆 ∖ 𝐸))) |
| 41 | 40 | ssriv 3987 |
. . . . . . 7
⊢ (𝑎 ∩ 𝐸) ⊆ (𝑎 ∖ (∪ 𝑆 ∖ 𝐸)) |
| 42 | 41 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∩ 𝐸) ⊆ (𝑎 ∖ (∪ 𝑆 ∖ 𝐸))) |
| 43 | 35, 42 | eqssd 4001 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ (∪ 𝑆 ∖ 𝐸)) = (𝑎 ∩ 𝐸)) |
| 44 | 43 | fveq2d 6910 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∖ (∪ 𝑆 ∖ 𝐸))) = (𝑂‘(𝑎 ∩ 𝐸))) |
| 45 | 27, 44 | oveq12d 7449 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ (∪ 𝑆 ∖ 𝐸))) +𝑒 (𝑂‘(𝑎 ∖ (∪ 𝑆 ∖ 𝐸)))) = ((𝑂‘(𝑎 ∖ 𝐸)) +𝑒 (𝑂‘(𝑎 ∩ 𝐸)))) |
| 46 | | iccssxr 13470 |
. . . . 5
⊢
(0[,]+∞) ⊆ ℝ* |
| 47 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → 𝑂 ∈ OutMeas) |
| 48 | 17 | ssdifssd 4147 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ 𝐸) ⊆ ∪ dom
𝑂) |
| 49 | 47, 2, 48 | omecl 46518 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∖ 𝐸)) ∈ (0[,]+∞)) |
| 50 | 46, 49 | sselid 3981 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∖ 𝐸)) ∈
ℝ*) |
| 51 | | ssinss1 4246 |
. . . . . . . 8
⊢ (𝑎 ⊆ ∪ dom 𝑂 → (𝑎 ∩ 𝐸) ⊆ ∪ dom
𝑂) |
| 52 | 16, 51 | syl 17 |
. . . . . . 7
⊢ (𝑎 ∈ 𝒫 ∪ dom 𝑂 → (𝑎 ∩ 𝐸) ⊆ ∪ dom
𝑂) |
| 53 | 52 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∩ 𝐸) ⊆ ∪ dom
𝑂) |
| 54 | 47, 2, 53 | omecl 46518 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∩ 𝐸)) ∈ (0[,]+∞)) |
| 55 | 46, 54 | sselid 3981 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∩ 𝐸)) ∈
ℝ*) |
| 56 | 50, 55 | xaddcomd 45335 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∖ 𝐸)) +𝑒 (𝑂‘(𝑎 ∩ 𝐸))) = ((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸)))) |
| 57 | | caragendifcl.e |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ 𝑆) |
| 58 | 1, 3 | caragenel 46510 |
. . . . . 6
⊢ (𝜑 → (𝐸 ∈ 𝑆 ↔ (𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎)))) |
| 59 | 57, 58 | mpbid 232 |
. . . . 5
⊢ (𝜑 → (𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎))) |
| 60 | 59 | simprd 495 |
. . . 4
⊢ (𝜑 → ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎)) |
| 61 | 60 | r19.21bi 3251 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎)) |
| 62 | 45, 56, 61 | 3eqtrd 2781 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ (∪ 𝑆 ∖ 𝐸))) +𝑒 (𝑂‘(𝑎 ∖ (∪ 𝑆 ∖ 𝐸)))) = (𝑂‘𝑎)) |
| 63 | 1, 2, 3, 15, 62 | carageneld 46517 |
1
⊢ (𝜑 → (∪ 𝑆
∖ 𝐸) ∈ 𝑆) |