# Metamath Proof Explorer

## Theorem truae

Description: A truth holds almost everywhere. (Contributed by Thierry Arnoux, 20-Oct-2017)

Ref Expression
Hypotheses truae.1 dom 𝑀 = 𝑂
truae.2 ( 𝜑𝑀 ran measures )
truae.3 ( 𝜑𝜓 )
Assertion truae ( 𝜑 → { 𝑥𝑂𝜓 } a.e. 𝑀 )

### Proof

Step Hyp Ref Expression
1 truae.1 dom 𝑀 = 𝑂
2 truae.2 ( 𝜑𝑀 ran measures )
3 truae.3 ( 𝜑𝜓 )
4 3 pm2.24d ( 𝜑 → ( ¬ 𝜓𝑥 ∈ ∅ ) )
5 4 ralrimivw ( 𝜑 → ∀ 𝑥𝑂 ( ¬ 𝜓𝑥 ∈ ∅ ) )
6 rabss ( { 𝑥𝑂 ∣ ¬ 𝜓 } ⊆ ∅ ↔ ∀ 𝑥𝑂 ( ¬ 𝜓𝑥 ∈ ∅ ) )
7 5 6 sylibr ( 𝜑 → { 𝑥𝑂 ∣ ¬ 𝜓 } ⊆ ∅ )
8 ss0 ( { 𝑥𝑂 ∣ ¬ 𝜓 } ⊆ ∅ → { 𝑥𝑂 ∣ ¬ 𝜓 } = ∅ )
9 7 8 syl ( 𝜑 → { 𝑥𝑂 ∣ ¬ 𝜓 } = ∅ )
10 9 fveq2d ( 𝜑 → ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = ( 𝑀 ‘ ∅ ) )
11 measbasedom ( 𝑀 ran measures ↔ 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
12 measvnul ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) → ( 𝑀 ‘ ∅ ) = 0 )
13 11 12 sylbi ( 𝑀 ran measures → ( 𝑀 ‘ ∅ ) = 0 )
14 2 13 syl ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
15 10 14 eqtrd ( 𝜑 → ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 )
16 1 braew ( 𝑀 ran measures → ( { 𝑥𝑂𝜓 } a.e. 𝑀 ↔ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) )
17 2 16 syl ( 𝜑 → ( { 𝑥𝑂𝜓 } a.e. 𝑀 ↔ ( 𝑀 ‘ { 𝑥𝑂 ∣ ¬ 𝜓 } ) = 0 ) )
18 15 17 mpbird ( 𝜑 → { 𝑥𝑂𝜓 } a.e. 𝑀 )