Metamath Proof Explorer


Theorem smfpreimale

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of a closed interval unbounded below is in the subspace sigma-algebra induced by its domain. See Proposition 121B (ii) of Fremlin1 p. 35 (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfpreimale.s φ S SAlg
smfpreimale.f φ F SMblFn S
smfpreimale.d D = dom F
smfpreimale.a φ A
Assertion smfpreimale φ x D | F x A S 𝑡 D

Proof

Step Hyp Ref Expression
1 smfpreimale.s φ S SAlg
2 smfpreimale.f φ F SMblFn S
3 smfpreimale.d D = dom F
4 smfpreimale.a φ A
5 1 3 issmfle φ F SMblFn S D S F : D a x D | F x a S 𝑡 D
6 2 5 mpbid φ D S F : D a x D | F x a S 𝑡 D
7 6 simp3d φ a x D | F x a S 𝑡 D
8 breq2 a = A F x a F x A
9 8 rabbidv a = A x D | F x a = x D | F x A
10 9 eleq1d a = A x D | F x a S 𝑡 D x D | F x A S 𝑡 D
11 10 rspcva A a x D | F x a S 𝑡 D x D | F x A S 𝑡 D
12 4 7 11 syl2anc φ x D | F x A S 𝑡 D