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. 𝑀 )