Metamath Proof Explorer


Theorem smfpimbor1

Description: Given a sigma-measurable function, the preimage of a Borel set belongs to the subspace sigma-algebra induced by the domain of the function. Proposition 121E (f) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfpimbor1.s
|- ( ph -> S e. SAlg )
smfpimbor1.f
|- ( ph -> F e. ( SMblFn ` S ) )
smfpimbor1.a
|- D = dom F
smfpimbor1.j
|- J = ( topGen ` ran (,) )
smfpimbor1.b
|- B = ( SalGen ` J )
smfpimbor1.e
|- ( ph -> E e. B )
smfpimbor1.p
|- P = ( `' F " E )
Assertion smfpimbor1
|- ( ph -> P e. ( S |`t D ) )

Proof

Step Hyp Ref Expression
1 smfpimbor1.s
 |-  ( ph -> S e. SAlg )
2 smfpimbor1.f
 |-  ( ph -> F e. ( SMblFn ` S ) )
3 smfpimbor1.a
 |-  D = dom F
4 smfpimbor1.j
 |-  J = ( topGen ` ran (,) )
5 smfpimbor1.b
 |-  B = ( SalGen ` J )
6 smfpimbor1.e
 |-  ( ph -> E e. B )
7 smfpimbor1.p
 |-  P = ( `' F " E )
8 eqid
 |-  { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) } = { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) }
9 1 2 3 4 5 6 7 8 smfpimbor1lem2
 |-  ( ph -> P e. ( S |`t D ) )