Metamath Proof Explorer


Theorem smfpreimalt

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfpreimalt.s
|- ( ph -> S e. SAlg )
smfpreimalt.f
|- ( ph -> F e. ( SMblFn ` S ) )
smfpreimalt.d
|- D = dom F
smfpreimalt.a
|- ( ph -> A e. RR )
Assertion smfpreimalt
|- ( ph -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )

Proof

Step Hyp Ref Expression
1 smfpreimalt.s
 |-  ( ph -> S e. SAlg )
2 smfpreimalt.f
 |-  ( ph -> F e. ( SMblFn ` S ) )
3 smfpreimalt.d
 |-  D = dom F
4 smfpreimalt.a
 |-  ( ph -> A e. RR )
5 1 3 issmf
 |-  ( ph -> ( F e. ( SMblFn ` S ) <-> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) ) )
6 2 5 mpbid
 |-  ( ph -> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) )
7 6 simp3d
 |-  ( ph -> A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) )
8 breq2
 |-  ( a = A -> ( ( F ` x ) < a <-> ( F ` x ) < A ) )
9 8 rabbidv
 |-  ( a = A -> { x e. D | ( F ` x ) < a } = { x e. D | ( F ` x ) < A } )
10 9 eleq1d
 |-  ( a = A -> ( { x e. D | ( F ` x ) < a } e. ( S |`t D ) <-> { x e. D | ( F ` x ) < A } e. ( S |`t D ) ) )
11 10 rspcva
 |-  ( ( A e. RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )
12 4 7 11 syl2anc
 |-  ( ph -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )