Step | Hyp | Ref
| Expression |
1 | | caragendifcl.o |
. 2
⊢ (𝜑 → 𝑂 ∈ OutMeas) |
2 | | eqid 2760 |
. 2
⊢ ∪ dom 𝑂 = ∪ dom 𝑂 |
3 | | caragendifcl.s |
. 2
⊢ 𝑆 = (CaraGen‘𝑂) |
4 | 3 | caragenss 41242 |
. . . . . 6
⊢ (𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂) |
5 | 1, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ dom 𝑂) |
6 | 5 | unissd 4614 |
. . . 4
⊢ (𝜑 → ∪ 𝑆
⊆ ∪ dom 𝑂) |
7 | 6 | ssdifssd 3891 |
. . 3
⊢ (𝜑 → (∪ 𝑆
∖ 𝐸) ⊆ ∪ dom 𝑂) |
8 | | fvex 6363 |
. . . . . . . 8
⊢
(CaraGen‘𝑂)
∈ V |
9 | 3, 8 | eqeltri 2835 |
. . . . . . 7
⊢ 𝑆 ∈ V |
10 | 9 | uniex 7119 |
. . . . . 6
⊢ ∪ 𝑆
∈ V |
11 | | difexg 4960 |
. . . . . 6
⊢ (∪ 𝑆
∈ V → (∪ 𝑆 ∖ 𝐸) ∈ V) |
12 | 10, 11 | ax-mp 5 |
. . . . 5
⊢ (∪ 𝑆
∖ 𝐸) ∈
V |
13 | 12 | a1i 11 |
. . . 4
⊢ (𝜑 → (∪ 𝑆
∖ 𝐸) ∈
V) |
14 | | elpwg 4310 |
. . . 4
⊢ ((∪ 𝑆
∖ 𝐸) ∈ V →
((∪ 𝑆 ∖ 𝐸) ∈ 𝒫 ∪ dom 𝑂 ↔ (∪ 𝑆 ∖ 𝐸) ⊆ ∪ dom
𝑂)) |
15 | 13, 14 | syl 17 |
. . 3
⊢ (𝜑 → ((∪ 𝑆
∖ 𝐸) ∈ 𝒫
∪ dom 𝑂 ↔ (∪ 𝑆 ∖ 𝐸) ⊆ ∪ dom
𝑂)) |
16 | 7, 15 | mpbird 247 |
. 2
⊢ (𝜑 → (∪ 𝑆
∖ 𝐸) ∈ 𝒫
∪ dom 𝑂) |
17 | | elpwi 4312 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝒫 ∪ dom 𝑂 → 𝑎 ⊆ ∪ dom
𝑂) |
18 | 17 | adantl 473 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → 𝑎 ⊆ ∪ dom
𝑂) |
19 | 1, 3 | caragenuni 41249 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑆 =
∪ dom 𝑂) |
20 | 19 | eqcomd 2766 |
. . . . . . . . 9
⊢ (𝜑 → ∪ dom 𝑂 = ∪ 𝑆) |
21 | 20 | adantr 472 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ∪ dom
𝑂 = ∪ 𝑆) |
22 | 18, 21 | sseqtrd 3782 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → 𝑎 ⊆ ∪ 𝑆) |
23 | | difin2 4033 |
. . . . . . 7
⊢ (𝑎 ⊆ ∪ 𝑆
→ (𝑎 ∖ 𝐸) = ((∪ 𝑆
∖ 𝐸) ∩ 𝑎)) |
24 | 22, 23 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ 𝐸) = ((∪ 𝑆 ∖ 𝐸) ∩ 𝑎)) |
25 | | incom 3948 |
. . . . . . 7
⊢ ((∪ 𝑆
∖ 𝐸) ∩ 𝑎) = (𝑎 ∩ (∪ 𝑆 ∖ 𝐸)) |
26 | 25 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((∪
𝑆 ∖ 𝐸) ∩ 𝑎) = (𝑎 ∩ (∪ 𝑆 ∖ 𝐸))) |
27 | 24, 26 | eqtr2d 2795 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∩ (∪ 𝑆 ∖ 𝐸)) = (𝑎 ∖ 𝐸)) |
28 | 27 | fveq2d 6357 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∩ (∪ 𝑆 ∖ 𝐸))) = (𝑂‘(𝑎 ∖ 𝐸))) |
29 | 22 | ssdifd 3889 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ 𝐸) ⊆ (∪
𝑆 ∖ 𝐸)) |
30 | | sscon 3887 |
. . . . . . . 8
⊢ ((𝑎 ∖ 𝐸) ⊆ (∪
𝑆 ∖ 𝐸) → (𝑎 ∖ (∪ 𝑆 ∖ 𝐸)) ⊆ (𝑎 ∖ (𝑎 ∖ 𝐸))) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ (∪ 𝑆 ∖ 𝐸)) ⊆ (𝑎 ∖ (𝑎 ∖ 𝐸))) |
32 | | dfin4 4010 |
. . . . . . . . 9
⊢ (𝑎 ∩ 𝐸) = (𝑎 ∖ (𝑎 ∖ 𝐸)) |
33 | 32 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∩ 𝐸) = (𝑎 ∖ (𝑎 ∖ 𝐸))) |
34 | | eqimss2 3799 |
. . . . . . . 8
⊢ ((𝑎 ∩ 𝐸) = (𝑎 ∖ (𝑎 ∖ 𝐸)) → (𝑎 ∖ (𝑎 ∖ 𝐸)) ⊆ (𝑎 ∩ 𝐸)) |
35 | 33, 34 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ (𝑎 ∖ 𝐸)) ⊆ (𝑎 ∩ 𝐸)) |
36 | 31, 35 | sstrd 3754 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ (∪ 𝑆 ∖ 𝐸)) ⊆ (𝑎 ∩ 𝐸)) |
37 | | elinel1 3942 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑎 ∩ 𝐸) → 𝑥 ∈ 𝑎) |
38 | | elinel2 3943 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑎 ∩ 𝐸) → 𝑥 ∈ 𝐸) |
39 | | elndif 3877 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐸 → ¬ 𝑥 ∈ (∪ 𝑆 ∖ 𝐸)) |
40 | 38, 39 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑎 ∩ 𝐸) → ¬ 𝑥 ∈ (∪ 𝑆 ∖ 𝐸)) |
41 | 37, 40 | eldifd 3726 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑎 ∩ 𝐸) → 𝑥 ∈ (𝑎 ∖ (∪ 𝑆 ∖ 𝐸))) |
42 | 41 | ssriv 3748 |
. . . . . . 7
⊢ (𝑎 ∩ 𝐸) ⊆ (𝑎 ∖ (∪ 𝑆 ∖ 𝐸)) |
43 | 42 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∩ 𝐸) ⊆ (𝑎 ∖ (∪ 𝑆 ∖ 𝐸))) |
44 | 36, 43 | eqssd 3761 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ (∪ 𝑆 ∖ 𝐸)) = (𝑎 ∩ 𝐸)) |
45 | 44 | fveq2d 6357 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∖ (∪ 𝑆 ∖ 𝐸))) = (𝑂‘(𝑎 ∩ 𝐸))) |
46 | 28, 45 | oveq12d 6832 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ (∪ 𝑆 ∖ 𝐸))) +𝑒 (𝑂‘(𝑎 ∖ (∪ 𝑆 ∖ 𝐸)))) = ((𝑂‘(𝑎 ∖ 𝐸)) +𝑒 (𝑂‘(𝑎 ∩ 𝐸)))) |
47 | | iccssxr 12469 |
. . . . 5
⊢
(0[,]+∞) ⊆ ℝ* |
48 | 1 | adantr 472 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → 𝑂 ∈ OutMeas) |
49 | 18 | ssdifssd 3891 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ 𝐸) ⊆ ∪ dom
𝑂) |
50 | 48, 2, 49 | omecl 41241 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∖ 𝐸)) ∈ (0[,]+∞)) |
51 | 47, 50 | sseldi 3742 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∖ 𝐸)) ∈
ℝ*) |
52 | | ssinss1 3984 |
. . . . . . . 8
⊢ (𝑎 ⊆ ∪ dom 𝑂 → (𝑎 ∩ 𝐸) ⊆ ∪ dom
𝑂) |
53 | 17, 52 | syl 17 |
. . . . . . 7
⊢ (𝑎 ∈ 𝒫 ∪ dom 𝑂 → (𝑎 ∩ 𝐸) ⊆ ∪ dom
𝑂) |
54 | 53 | adantl 473 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∩ 𝐸) ⊆ ∪ dom
𝑂) |
55 | 48, 2, 54 | omecl 41241 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∩ 𝐸)) ∈ (0[,]+∞)) |
56 | 47, 55 | sseldi 3742 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∩ 𝐸)) ∈
ℝ*) |
57 | 51, 56 | xaddcomd 40056 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∖ 𝐸)) +𝑒 (𝑂‘(𝑎 ∩ 𝐸))) = ((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸)))) |
58 | | caragendifcl.e |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ 𝑆) |
59 | 1, 3 | caragenel 41233 |
. . . . . 6
⊢ (𝜑 → (𝐸 ∈ 𝑆 ↔ (𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎)))) |
60 | 58, 59 | mpbid 222 |
. . . . 5
⊢ (𝜑 → (𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎))) |
61 | 60 | simprd 482 |
. . . 4
⊢ (𝜑 → ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎)) |
62 | 61 | r19.21bi 3070 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎)) |
63 | 46, 57, 62 | 3eqtrd 2798 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ (∪ 𝑆 ∖ 𝐸))) +𝑒 (𝑂‘(𝑎 ∖ (∪ 𝑆 ∖ 𝐸)))) = (𝑂‘𝑎)) |
64 | 1, 2, 3, 16, 63 | carageneld 41240 |
1
⊢ (𝜑 → (∪ 𝑆
∖ 𝐸) ∈ 𝑆) |