Step | Hyp | Ref
| Expression |
1 | | braew.1 |
. . . . 5
⊢ ∪ dom 𝑀 = 𝑂 |
2 | | dmexg 6989 |
. . . . . 6
⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ V) |
3 | | uniexg 6853 |
. . . . . 6
⊢ (dom
𝑀 ∈ V → ∪ dom 𝑀 ∈ V) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝑀 ∈ ∪ ran measures → ∪ dom
𝑀 ∈
V) |
5 | 1, 4 | syl5eqelr 2693 |
. . . 4
⊢ (𝑀 ∈ ∪ ran measures → 𝑂 ∈ V) |
6 | | rabexg 4739 |
. . . 4
⊢ (𝑂 ∈ V → {𝑥 ∈ 𝑂 ∣ 𝜑} ∈ V) |
7 | 5, 6 | syl 17 |
. . 3
⊢ (𝑀 ∈ ∪ ran measures → {𝑥 ∈ 𝑂 ∣ 𝜑} ∈ V) |
8 | | simpr 476 |
. . . . . 6
⊢ ((𝑎 = {𝑥 ∈ 𝑂 ∣ 𝜑} ∧ 𝑚 = 𝑀) → 𝑚 = 𝑀) |
9 | 8 | dmeqd 5248 |
. . . . . . . 8
⊢ ((𝑎 = {𝑥 ∈ 𝑂 ∣ 𝜑} ∧ 𝑚 = 𝑀) → dom 𝑚 = dom 𝑀) |
10 | 9 | unieqd 4382 |
. . . . . . 7
⊢ ((𝑎 = {𝑥 ∈ 𝑂 ∣ 𝜑} ∧ 𝑚 = 𝑀) → ∪ dom
𝑚 = ∪ dom 𝑀) |
11 | | simpl 472 |
. . . . . . 7
⊢ ((𝑎 = {𝑥 ∈ 𝑂 ∣ 𝜑} ∧ 𝑚 = 𝑀) → 𝑎 = {𝑥 ∈ 𝑂 ∣ 𝜑}) |
12 | 10, 11 | difeq12d 3691 |
. . . . . 6
⊢ ((𝑎 = {𝑥 ∈ 𝑂 ∣ 𝜑} ∧ 𝑚 = 𝑀) → (∪ dom
𝑚 ∖ 𝑎) = (∪ dom 𝑀 ∖ {𝑥 ∈ 𝑂 ∣ 𝜑})) |
13 | 8, 12 | fveq12d 6109 |
. . . . 5
⊢ ((𝑎 = {𝑥 ∈ 𝑂 ∣ 𝜑} ∧ 𝑚 = 𝑀) → (𝑚‘(∪ dom
𝑚 ∖ 𝑎)) = (𝑀‘(∪ dom
𝑀 ∖ {𝑥 ∈ 𝑂 ∣ 𝜑}))) |
14 | 13 | eqeq1d 2612 |
. . . 4
⊢ ((𝑎 = {𝑥 ∈ 𝑂 ∣ 𝜑} ∧ 𝑚 = 𝑀) → ((𝑚‘(∪ dom
𝑚 ∖ 𝑎)) = 0 ↔ (𝑀‘(∪ dom
𝑀 ∖ {𝑥 ∈ 𝑂 ∣ 𝜑})) = 0)) |
15 | | df-ae 29629 |
. . . 4
⊢ a.e. =
{〈𝑎, 𝑚〉 ∣ (𝑚‘(∪ dom 𝑚 ∖ 𝑎)) = 0} |
16 | 14, 15 | brabga 4914 |
. . 3
⊢ (({𝑥 ∈ 𝑂 ∣ 𝜑} ∈ V ∧ 𝑀 ∈ ∪ ran
measures) → ({𝑥 ∈
𝑂 ∣ 𝜑}a.e.𝑀 ↔ (𝑀‘(∪ dom
𝑀 ∖ {𝑥 ∈ 𝑂 ∣ 𝜑})) = 0)) |
17 | 7, 16 | mpancom 700 |
. 2
⊢ (𝑀 ∈ ∪ ran measures → ({𝑥 ∈ 𝑂 ∣ 𝜑}a.e.𝑀 ↔ (𝑀‘(∪ dom
𝑀 ∖ {𝑥 ∈ 𝑂 ∣ 𝜑})) = 0)) |
18 | 1 | difeq1i 3686 |
. . . . 5
⊢ (∪ dom 𝑀 ∖ {𝑥 ∈ 𝑂 ∣ 𝜑}) = (𝑂 ∖ {𝑥 ∈ 𝑂 ∣ 𝜑}) |
19 | | notrab 3863 |
. . . . 5
⊢ (𝑂 ∖ {𝑥 ∈ 𝑂 ∣ 𝜑}) = {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} |
20 | 18, 19 | eqtri 2632 |
. . . 4
⊢ (∪ dom 𝑀 ∖ {𝑥 ∈ 𝑂 ∣ 𝜑}) = {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} |
21 | 20 | fveq2i 6106 |
. . 3
⊢ (𝑀‘(∪ dom 𝑀 ∖ {𝑥 ∈ 𝑂 ∣ 𝜑})) = (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) |
22 | 21 | eqeq1i 2615 |
. 2
⊢ ((𝑀‘(∪ dom 𝑀 ∖ {𝑥 ∈ 𝑂 ∣ 𝜑})) = 0 ↔ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0) |
23 | 17, 22 | syl6bb 275 |
1
⊢ (𝑀 ∈ ∪ ran measures → ({𝑥 ∈ 𝑂 ∣ 𝜑}a.e.𝑀 ↔ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0)) |