Metamath Proof Explorer

Theorem braew

Description: 'almost everywhere' relation for a measure M and a property ph (Contributed by Thierry Arnoux, 20-Oct-2017)

Ref Expression
Hypothesis braew.1 ⊢ ⋃ dom ⁡ M = O
Assertion braew ⊢ M ∈ ⋃ ran ⁡ measures → x ∈ O | φ M-ae. ↔ M ⁡ x ∈ O | ¬ φ = 0

Proof

Step Hyp Ref Expression
1 braew.1 ⊢ ⋃ dom ⁡ M = O
2 dmexg ⊢ M ∈ ⋃ ran ⁡ measures → dom ⁡ M ∈ V
3 2 uniexd ⊢ M ∈ ⋃ ran ⁡ measures → ⋃ dom ⁡ M ∈ V
4 1 3 eqeltrrid ⊢ M ∈ ⋃ ran ⁡ measures → O ∈ V
5 rabexg ⊢ O ∈ V → x ∈ O | φ ∈ V
6 4 5 syl ⊢ M ∈ ⋃ ran ⁡ measures → x ∈ O | φ ∈ V
7 simpr ⊢ a = x ∈ O | φ ∧ m = M → m = M
8 7 dmeqd ⊢ a = x ∈ O | φ ∧ m = M → dom ⁡ m = dom ⁡ M
9 8 unieqd ⊢ a = x ∈ O | φ ∧ m = M → ⋃ dom ⁡ m = ⋃ dom ⁡ M
10 simpl ⊢ a = x ∈ O | φ ∧ m = M → a = x ∈ O | φ
11 9 10 difeq12d ⊢ a = x ∈ O | φ ∧ m = M → ⋃ dom ⁡ m ∖ a = ⋃ dom ⁡ M ∖ x ∈ O | φ
12 7 11 fveq12d ⊢ a = x ∈ O | φ ∧ m = M → m ⁡ ⋃ dom ⁡ m ∖ a = M ⁡ ⋃ dom ⁡ M ∖ x ∈ O | φ
13 12 eqeq1d ⊢ a = x ∈ O | φ ∧ m = M → m ⁡ ⋃ dom ⁡ m ∖ a = 0 ↔ M ⁡ ⋃ dom ⁡ M ∖ x ∈ O | φ = 0
14 df-ae ⊢ ae = a m | m ⁡ ⋃ dom ⁡ m ∖ a = 0
15 13 14 brabga ⊢ x ∈ O | φ ∈ V ∧ M ∈ ⋃ ran ⁡ measures → x ∈ O | φ M-ae. ↔ M ⁡ ⋃ dom ⁡ M ∖ x ∈ O | φ = 0
16 6 15 mpancom ⊢ M ∈ ⋃ ran ⁡ measures → x ∈ O | φ M-ae. ↔ M ⁡ ⋃ dom ⁡ M ∖ x ∈ O | φ = 0
17 1 difeq1i ⊢ ⋃ dom ⁡ M ∖ x ∈ O | φ = O ∖ x ∈ O | φ
18 notrab ⊢ O ∖ x ∈ O | φ = x ∈ O | ¬ φ
19 17 18 eqtri ⊢ ⋃ dom ⁡ M ∖ x ∈ O | φ = x ∈ O | ¬ φ
20 19 fveq2i ⊢ M ⁡ ⋃ dom ⁡ M ∖ x ∈ O | φ = M ⁡ x ∈ O | ¬ φ
21 20 eqeq1i ⊢ M ⁡ ⋃ dom ⁡ M ∖ x ∈ O | φ = 0 ↔ M ⁡ x ∈ O | ¬ φ = 0
22 16 21 syl6bb ⊢ M ∈ ⋃ ran ⁡ measures → x ∈ O | φ M-ae. ↔ M ⁡ x ∈ O | ¬ φ = 0