Theorem truae

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

	Ref	Expression
Hypotheses	truae.1	|- U. dom M = O
	truae.2	|- ( ph -> M e. U. ran measures )
	truae.3	|- ( ph -> ps )
Assertion	truae	|- ( ph -> { x e. O | ps } ae M )

Proof

Step	Hyp	Ref	Expression
1		truae.1	|- U. dom M = O
2		truae.2	|- ( ph -> M e. U. ran measures )
3		truae.3	|- ( ph -> ps )
4	3	pm2.24d	|- ( ph -> ( -. ps -> x e. (/) ) )
5	4	ralrimivw	|- ( ph -> A. x e. O ( -. ps -> x e. (/) ) )
6		rabss	|- ( { x e. O | -. ps } C_ (/) <-> A. x e. O ( -. ps -> x e. (/) ) )
7	5 6	sylibr	|- ( ph -> { x e. O | -. ps } C_ (/) )
8		ss0	|- ( { x e. O | -. ps } C_ (/) -> { x e. O | -. ps } = (/) )
9	7 8	syl	|- ( ph -> { x e. O | -. ps } = (/) )
10	9	fveq2d	|- ( ph -> ( M ` { x e. O | -. ps } ) = ( M ` (/) ) )
11		measbasedom	|- ( M e. U. ran measures <-> M e. ( measures ` dom M ) )
12		measvnul	|- ( M e. ( measures ` dom M ) -> ( M ` (/) ) = 0 )
13	11 12	sylbi	|- ( M e. U. ran measures -> ( M ` (/) ) = 0 )
14	2 13	syl	|- ( ph -> ( M ` (/) ) = 0 )
15	10 14	eqtrd	|- ( ph -> ( M ` { x e. O | -. ps } ) = 0 )
16	1	braew	|- ( M e. U. ran measures -> ( { x e. O | ps } ae M <-> ( M ` { x e. O | -. ps } ) = 0 ) )
17	2 16	syl	|- ( ph -> ( { x e. O | ps } ae M <-> ( M ` { x e. O | -. ps } ) = 0 ) )
18	15 17	mpbird	|- ( ph -> { x e. O | ps } ae M )