Step | Hyp | Ref
| Expression |
1 | | caragendifcl.o |
. 2
⊢ (𝜑 → 𝑂 ∈ OutMeas) |
2 | | eqid 2622 |
. 2
⊢ ∪ dom 𝑂 = ∪ dom 𝑂 |
3 | | caragendifcl.s |
. 2
⊢ 𝑆 = (CaraGen‘𝑂) |
4 | 3 | caragenss 40718 |
. . . . . 6
⊢ (𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂) |
5 | 1, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ dom 𝑂) |
6 | 5 | unissd 4462 |
. . . 4
⊢ (𝜑 → ∪ 𝑆
⊆ ∪ dom 𝑂) |
7 | 6 | ssdifssd 3748 |
. . 3
⊢ (𝜑 → (∪ 𝑆
∖ 𝐸) ⊆ ∪ dom 𝑂) |
8 | | fvex 6201 |
. . . . . . . 8
⊢
(CaraGen‘𝑂)
∈ V |
9 | 3, 8 | eqeltri 2697 |
. . . . . . 7
⊢ 𝑆 ∈ V |
10 | 9 | uniex 6953 |
. . . . . 6
⊢ ∪ 𝑆
∈ V |
11 | | difexg 4808 |
. . . . . 6
⊢ (∪ 𝑆
∈ V → (∪ 𝑆 ∖ 𝐸) ∈ V) |
12 | 10, 11 | ax-mp 5 |
. . . . 5
⊢ (∪ 𝑆
∖ 𝐸) ∈
V |
13 | 12 | a1i 11 |
. . . 4
⊢ (𝜑 → (∪ 𝑆
∖ 𝐸) ∈
V) |
14 | | elpwg 4166 |
. . . 4
⊢ ((∪ 𝑆
∖ 𝐸) ∈ V →
((∪ 𝑆 ∖ 𝐸) ∈ 𝒫 ∪ dom 𝑂 ↔ (∪ 𝑆 ∖ 𝐸) ⊆ ∪ dom
𝑂)) |
15 | 13, 14 | syl 17 |
. . 3
⊢ (𝜑 → ((∪ 𝑆
∖ 𝐸) ∈ 𝒫
∪ dom 𝑂 ↔ (∪ 𝑆 ∖ 𝐸) ⊆ ∪ dom
𝑂)) |
16 | 7, 15 | mpbird 247 |
. 2
⊢ (𝜑 → (∪ 𝑆
∖ 𝐸) ∈ 𝒫
∪ dom 𝑂) |
17 | | elpwi 4168 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝒫 ∪ dom 𝑂 → 𝑎 ⊆ ∪ dom
𝑂) |
18 | 17 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → 𝑎 ⊆ ∪ dom
𝑂) |
19 | 1, 3 | caragenuni 40725 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑆 =
∪ dom 𝑂) |
20 | 19 | eqcomd 2628 |
. . . . . . . . 9
⊢ (𝜑 → ∪ dom 𝑂 = ∪ 𝑆) |
21 | 20 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ∪ dom
𝑂 = ∪ 𝑆) |
22 | 18, 21 | sseqtrd 3641 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → 𝑎 ⊆ ∪ 𝑆) |
23 | | difin2 3890 |
. . . . . . 7
⊢ (𝑎 ⊆ ∪ 𝑆
→ (𝑎 ∖ 𝐸) = ((∪ 𝑆
∖ 𝐸) ∩ 𝑎)) |
24 | 22, 23 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ 𝐸) = ((∪ 𝑆 ∖ 𝐸) ∩ 𝑎)) |
25 | | incom 3805 |
. . . . . . 7
⊢ ((∪ 𝑆
∖ 𝐸) ∩ 𝑎) = (𝑎 ∩ (∪ 𝑆 ∖ 𝐸)) |
26 | 25 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((∪
𝑆 ∖ 𝐸) ∩ 𝑎) = (𝑎 ∩ (∪ 𝑆 ∖ 𝐸))) |
27 | 24, 26 | eqtr2d 2657 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∩ (∪ 𝑆 ∖ 𝐸)) = (𝑎 ∖ 𝐸)) |
28 | 27 | fveq2d 6195 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∩ (∪ 𝑆 ∖ 𝐸))) = (𝑂‘(𝑎 ∖ 𝐸))) |
29 | 22 | ssdifd 3746 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ 𝐸) ⊆ (∪
𝑆 ∖ 𝐸)) |
30 | | sscon 3744 |
. . . . . . . 8
⊢ ((𝑎 ∖ 𝐸) ⊆ (∪
𝑆 ∖ 𝐸) → (𝑎 ∖ (∪ 𝑆 ∖ 𝐸)) ⊆ (𝑎 ∖ (𝑎 ∖ 𝐸))) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ (∪ 𝑆 ∖ 𝐸)) ⊆ (𝑎 ∖ (𝑎 ∖ 𝐸))) |
32 | | dfin4 3867 |
. . . . . . . . 9
⊢ (𝑎 ∩ 𝐸) = (𝑎 ∖ (𝑎 ∖ 𝐸)) |
33 | 32 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∩ 𝐸) = (𝑎 ∖ (𝑎 ∖ 𝐸))) |
34 | | eqimss2 3658 |
. . . . . . . 8
⊢ ((𝑎 ∩ 𝐸) = (𝑎 ∖ (𝑎 ∖ 𝐸)) → (𝑎 ∖ (𝑎 ∖ 𝐸)) ⊆ (𝑎 ∩ 𝐸)) |
35 | 33, 34 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ (𝑎 ∖ 𝐸)) ⊆ (𝑎 ∩ 𝐸)) |
36 | 31, 35 | sstrd 3613 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ (∪ 𝑆 ∖ 𝐸)) ⊆ (𝑎 ∩ 𝐸)) |
37 | | elinel1 3799 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑎 ∩ 𝐸) → 𝑥 ∈ 𝑎) |
38 | | elinel2 3800 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑎 ∩ 𝐸) → 𝑥 ∈ 𝐸) |
39 | | elndif 3734 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐸 → ¬ 𝑥 ∈ (∪ 𝑆 ∖ 𝐸)) |
40 | 38, 39 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑎 ∩ 𝐸) → ¬ 𝑥 ∈ (∪ 𝑆 ∖ 𝐸)) |
41 | 37, 40 | eldifd 3585 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑎 ∩ 𝐸) → 𝑥 ∈ (𝑎 ∖ (∪ 𝑆 ∖ 𝐸))) |
42 | 41 | ssriv 3607 |
. . . . . . 7
⊢ (𝑎 ∩ 𝐸) ⊆ (𝑎 ∖ (∪ 𝑆 ∖ 𝐸)) |
43 | 42 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∩ 𝐸) ⊆ (𝑎 ∖ (∪ 𝑆 ∖ 𝐸))) |
44 | 36, 43 | eqssd 3620 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ (∪ 𝑆 ∖ 𝐸)) = (𝑎 ∩ 𝐸)) |
45 | 44 | fveq2d 6195 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∖ (∪ 𝑆 ∖ 𝐸))) = (𝑂‘(𝑎 ∩ 𝐸))) |
46 | 28, 45 | oveq12d 6668 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ (∪ 𝑆 ∖ 𝐸))) +𝑒 (𝑂‘(𝑎 ∖ (∪ 𝑆 ∖ 𝐸)))) = ((𝑂‘(𝑎 ∖ 𝐸)) +𝑒 (𝑂‘(𝑎 ∩ 𝐸)))) |
47 | | iccssxr 12256 |
. . . . 5
⊢
(0[,]+∞) ⊆ ℝ* |
48 | 1 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → 𝑂 ∈ OutMeas) |
49 | 18 | ssdifssd 3748 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∖ 𝐸) ⊆ ∪ dom
𝑂) |
50 | 48, 2, 49 | omecl 40717 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∖ 𝐸)) ∈ (0[,]+∞)) |
51 | 47, 50 | sseldi 3601 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∖ 𝐸)) ∈
ℝ*) |
52 | | ssinss1 3841 |
. . . . . . . 8
⊢ (𝑎 ⊆ ∪ dom 𝑂 → (𝑎 ∩ 𝐸) ⊆ ∪ dom
𝑂) |
53 | 17, 52 | syl 17 |
. . . . . . 7
⊢ (𝑎 ∈ 𝒫 ∪ dom 𝑂 → (𝑎 ∩ 𝐸) ⊆ ∪ dom
𝑂) |
54 | 53 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑎 ∩ 𝐸) ⊆ ∪ dom
𝑂) |
55 | 48, 2, 54 | omecl 40717 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∩ 𝐸)) ∈ (0[,]+∞)) |
56 | 47, 55 | sseldi 3601 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → (𝑂‘(𝑎 ∩ 𝐸)) ∈
ℝ*) |
57 | 51, 56 | xaddcomd 39540 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∖ 𝐸)) +𝑒 (𝑂‘(𝑎 ∩ 𝐸))) = ((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸)))) |
58 | | caragendifcl.e |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ 𝑆) |
59 | 1, 3 | caragenel 40709 |
. . . . . 6
⊢ (𝜑 → (𝐸 ∈ 𝑆 ↔ (𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎)))) |
60 | 58, 59 | mpbid 222 |
. . . . 5
⊢ (𝜑 → (𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎))) |
61 | 60 | simprd 479 |
. . . 4
⊢ (𝜑 → ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎)) |
62 | 61 | r19.21bi 2932 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎)) |
63 | 46, 57, 62 | 3eqtrd 2660 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 ∪ dom 𝑂) → ((𝑂‘(𝑎 ∩ (∪ 𝑆 ∖ 𝐸))) +𝑒 (𝑂‘(𝑎 ∖ (∪ 𝑆 ∖ 𝐸)))) = (𝑂‘𝑎)) |
64 | 1, 2, 3, 16, 63 | carageneld 40716 |
1
⊢ (𝜑 → (∪ 𝑆
∖ 𝐸) ∈ 𝑆) |