Proof of Theorem aean
Step | Hyp | Ref
| Expression |
1 | | unrab 3857 |
. . . . . 6
⊢ ({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = {𝑥 ∈ 𝑂 ∣ (¬ 𝜑 ∨ ¬ 𝜓)} |
2 | | ianor 508 |
. . . . . . . 8
⊢ (¬
(𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓)) |
3 | 2 | a1i 11 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑂 → (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))) |
4 | 3 | rabbiia 3161 |
. . . . . 6
⊢ {𝑥 ∈ 𝑂 ∣ ¬ (𝜑 ∧ 𝜓)} = {𝑥 ∈ 𝑂 ∣ (¬ 𝜑 ∨ ¬ 𝜓)} |
5 | 1, 4 | eqtr4i 2635 |
. . . . 5
⊢ ({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = {𝑥 ∈ 𝑂 ∣ ¬ (𝜑 ∧ 𝜓)} |
6 | 5 | fveq2i 6106 |
. . . 4
⊢ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ (𝜑 ∧ 𝜓)}) |
7 | 6 | eqeq1i 2615 |
. . 3
⊢ ((𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0 ↔ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ (𝜑 ∧ 𝜓)}) = 0) |
8 | | measbasedom 29592 |
. . . . . . . . 9
⊢ (𝑀 ∈ ∪ ran measures ↔ 𝑀 ∈ (measures‘dom 𝑀)) |
9 | 8 | biimpi 205 |
. . . . . . . 8
⊢ (𝑀 ∈ ∪ ran measures → 𝑀 ∈ (measures‘dom 𝑀)) |
10 | 9 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) → 𝑀 ∈ (measures‘dom 𝑀)) |
11 | 10 | adantr 480 |
. . . . . 6
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0) → 𝑀 ∈ (measures‘dom 𝑀)) |
12 | | simp2 1055 |
. . . . . . 7
⊢ ((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) → {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀) |
13 | 12 | adantr 480 |
. . . . . 6
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0) → {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀) |
14 | | dmmeas 29591 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran
sigAlgebra) |
15 | | unelsiga 29524 |
. . . . . . . . . 10
⊢ ((dom
𝑀 ∈ ∪ ran sigAlgebra ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) → ({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) ∈ dom 𝑀) |
16 | 14, 15 | syl3an1 1351 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) → ({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) ∈ dom 𝑀) |
17 | | ssun1 3738 |
. . . . . . . . . 10
⊢ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ⊆ ({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) |
18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) → {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ⊆ ({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) |
19 | 10, 12, 16, 18 | measssd 29605 |
. . . . . . . 8
⊢ ((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) → (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) ≤ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓}))) |
20 | 19 | adantr 480 |
. . . . . . 7
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0) → (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) ≤ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓}))) |
21 | | simpr 476 |
. . . . . . 7
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0) → (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0) |
22 | 20, 21 | breqtrd 4609 |
. . . . . 6
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0) → (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) ≤ 0) |
23 | | measle0 29598 |
. . . . . 6
⊢ ((𝑀 ∈ (measures‘dom
𝑀) ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) ≤ 0) → (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0) |
24 | 11, 13, 22, 23 | syl3anc 1318 |
. . . . 5
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0) → (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0) |
25 | | simp3 1056 |
. . . . . . 7
⊢ ((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) → {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) |
26 | 25 | adantr 480 |
. . . . . 6
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0) → {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) |
27 | | ssun2 3739 |
. . . . . . . . . 10
⊢ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ⊆ ({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) |
28 | 27 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) → {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ⊆ ({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) |
29 | 10, 25, 16, 28 | measssd 29605 |
. . . . . . . 8
⊢ ((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) → (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) ≤ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓}))) |
30 | 29 | adantr 480 |
. . . . . . 7
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0) → (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) ≤ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓}))) |
31 | 30, 21 | breqtrd 4609 |
. . . . . 6
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0) → (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) ≤ 0) |
32 | | measle0 29598 |
. . . . . 6
⊢ ((𝑀 ∈ (measures‘dom
𝑀) ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) ≤ 0) → (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0) |
33 | 11, 26, 31, 32 | syl3anc 1318 |
. . . . 5
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0) → (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0) |
34 | 24, 33 | jca 553 |
. . . 4
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0) → ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0)) |
35 | 10 | adantr 480 |
. . . . 5
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0)) → 𝑀 ∈ (measures‘dom 𝑀)) |
36 | | measbase 29587 |
. . . . . . 7
⊢ (𝑀 ∈ (measures‘dom
𝑀) → dom 𝑀 ∈ ∪ ran sigAlgebra) |
37 | 35, 36 | syl 17 |
. . . . . 6
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0)) → dom 𝑀 ∈ ∪ ran
sigAlgebra) |
38 | 12 | adantr 480 |
. . . . . 6
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0)) → {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀) |
39 | 25 | adantr 480 |
. . . . . 6
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0)) → {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) |
40 | 37, 38, 39, 15 | syl3anc 1318 |
. . . . 5
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0)) → ({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) ∈ dom 𝑀) |
41 | 35, 38, 39 | measunl 29606 |
. . . . . 6
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0)) → (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) ≤ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) +𝑒 (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}))) |
42 | | simprl 790 |
. . . . . . . 8
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0)) → (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0) |
43 | | simprr 792 |
. . . . . . . 8
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0)) → (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0) |
44 | 42, 43 | oveq12d 6567 |
. . . . . . 7
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0)) → ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) +𝑒 (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = (0 +𝑒
0)) |
45 | | 0xr 9965 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
46 | | xaddid1 11946 |
. . . . . . . 8
⊢ (0 ∈
ℝ* → (0 +𝑒 0) = 0) |
47 | 45, 46 | ax-mp 5 |
. . . . . . 7
⊢ (0
+𝑒 0) = 0 |
48 | 44, 47 | syl6eq 2660 |
. . . . . 6
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0)) → ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) +𝑒 (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0) |
49 | 41, 48 | breqtrd 4609 |
. . . . 5
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0)) → (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) ≤ 0) |
50 | | measle0 29598 |
. . . . 5
⊢ ((𝑀 ∈ (measures‘dom
𝑀) ∧ ({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) ∈ dom 𝑀 ∧ (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) ≤ 0) → (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0) |
51 | 35, 40, 49, 50 | syl3anc 1318 |
. . . 4
⊢ (((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) ∧ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0)) → (𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0) |
52 | 34, 51 | impbida 873 |
. . 3
⊢ ((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) → ((𝑀‘({𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∪ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓})) = 0 ↔ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0))) |
53 | 7, 52 | syl5bbr 273 |
. 2
⊢ ((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) → ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ (𝜑 ∧ 𝜓)}) = 0 ↔ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0))) |
54 | | aean.1 |
. . . 4
⊢ ∪ dom 𝑀 = 𝑂 |
55 | 54 | braew 29632 |
. . 3
⊢ (𝑀 ∈ ∪ ran measures → ({𝑥 ∈ 𝑂 ∣ (𝜑 ∧ 𝜓)}a.e.𝑀 ↔ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ (𝜑 ∧ 𝜓)}) = 0)) |
56 | 55 | 3ad2ant1 1075 |
. 2
⊢ ((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) → ({𝑥 ∈ 𝑂 ∣ (𝜑 ∧ 𝜓)}a.e.𝑀 ↔ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ (𝜑 ∧ 𝜓)}) = 0)) |
57 | 54 | braew 29632 |
. . . 4
⊢ (𝑀 ∈ ∪ ran measures → ({𝑥 ∈ 𝑂 ∣ 𝜑}a.e.𝑀 ↔ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0)) |
58 | 54 | braew 29632 |
. . . 4
⊢ (𝑀 ∈ ∪ ran measures → ({𝑥 ∈ 𝑂 ∣ 𝜓}a.e.𝑀 ↔ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0)) |
59 | 57, 58 | anbi12d 743 |
. . 3
⊢ (𝑀 ∈ ∪ ran measures → (({𝑥 ∈ 𝑂 ∣ 𝜑}a.e.𝑀 ∧ {𝑥 ∈ 𝑂 ∣ 𝜓}a.e.𝑀) ↔ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0))) |
60 | 59 | 3ad2ant1 1075 |
. 2
⊢ ((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) → (({𝑥 ∈ 𝑂 ∣ 𝜑}a.e.𝑀 ∧ {𝑥 ∈ 𝑂 ∣ 𝜓}a.e.𝑀) ↔ ((𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0 ∧ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜓}) = 0))) |
61 | 53, 56, 60 | 3bitr4d 299 |
1
⊢ ((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) → ({𝑥 ∈ 𝑂 ∣ (𝜑 ∧ 𝜓)}a.e.𝑀 ↔ ({𝑥 ∈ 𝑂 ∣ 𝜑}a.e.𝑀 ∧ {𝑥 ∈ 𝑂 ∣ 𝜓}a.e.𝑀))) |