Metamath Proof Explorer


Theorem truae

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

Ref Expression
Hypotheses truae.1 domM=O
truae.2 φMranmeasures
truae.3 φψ
Assertion truae φxO|ψM-ae.

Proof

Step Hyp Ref Expression
1 truae.1 domM=O
2 truae.2 φMranmeasures
3 truae.3 φψ
4 3 pm2.24d φ¬ψx
5 4 ralrimivw φxO¬ψx
6 rabss xO|¬ψxO¬ψx
7 5 6 sylibr φxO|¬ψ
8 ss0 xO|¬ψxO|¬ψ=
9 7 8 syl φxO|¬ψ=
10 9 fveq2d φMxO|¬ψ=M
11 measbasedom MranmeasuresMmeasuresdomM
12 measvnul MmeasuresdomMM=0
13 11 12 sylbi MranmeasuresM=0
14 2 13 syl φM=0
15 10 14 eqtrd φMxO|¬ψ=0
16 1 braew MranmeasuresxO|ψM-ae.MxO|¬ψ=0
17 2 16 syl φxO|ψM-ae.MxO|¬ψ=0
18 15 17 mpbird φxO|ψM-ae.