Theorem issmfle2d

Description: A sufficient condition for " F being a measurable function w.r.t. to the sigma-algebra S ". (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	issmfle2d.a	$$⊢Ⅎa\phi$$
	issmfle2d.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
	issmfle2d.d	$$⊢\phi \to D\subseteq \bigcup S$$
	issmfle2d.f	$$⊢\phi \to F:D⟶ℝ$$
	issmfle2d.l	$$⊢\left(\phi \wedge a\in ℝ\right)\to F^{-1}\left[\left(\mathrm{-\infty },a\right]\right]\in \left(S{\upharpoonright }_{𝑡}D\right)$$
Assertion	issmfle2d	$$⊢\phi \to F\in \mathrm{SMblFn}\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		issmfle2d.a	$$⊢Ⅎa\phi$$
2		issmfle2d.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
3		issmfle2d.d	$$⊢\phi \to D\subseteq \bigcup S$$
4		issmfle2d.f	$$⊢\phi \to F:D⟶ℝ$$
5		issmfle2d.l	$$⊢\left(\phi \wedge a\in ℝ\right)\to F^{-1}\left[\left(\mathrm{-\infty },a\right]\right]\in \left(S{\upharpoonright }_{𝑡}D\right)$$
6	4	adantr	$$⊢\left(\phi \wedge a\in ℝ\right)\to F:D⟶ℝ$$
7		rexr	$$⊢a\in ℝ\to a\in {ℝ}^{*}$$
8	7	adantl	$$⊢\left(\phi \wedge a\in ℝ\right)\to a\in {ℝ}^{*}$$
9	6 8	preimaiocmnf	$$⊢\left(\phi \wedge a\in ℝ\right)\to F^{-1}\left[\left(\mathrm{-\infty },a\right]\right]=\left\{x\in D|F\left(x\right)\le a\right\}$$
10	9 5	eqeltrrd	$$⊢\left(\phi \wedge a\in ℝ\right)\to \left\{x\in D|F\left(x\right)\le a\right\}\in \left(S{\upharpoonright }_{𝑡}D\right)$$
11	1 2 3 4 10	issmfled	$$⊢\phi \to F\in \mathrm{SMblFn}\left(S\right)$$