Theorem smfpimgtxrmpt

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

	Ref	Expression
Hypotheses	smfpimgtxrmpt.x	$$⊢Ⅎx\phi$$
	smfpimgtxrmpt.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
	smfpimgtxrmpt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
	smfpimgtxrmpt.f	$$⊢\phi \to \left(x\in A⟼B\right)\in \mathrm{SMblFn}\left(S\right)$$
	smfpimgtxrmpt.l	$$⊢\phi \to L\in {ℝ}^{*}$$
Assertion	smfpimgtxrmpt	$$⊢\phi \to \left\{x\in A|L<B\right\}\in \left(S{\upharpoonright }_{𝑡}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		smfpimgtxrmpt.x	$$⊢Ⅎx\phi$$
2		smfpimgtxrmpt.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
3		smfpimgtxrmpt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
4		smfpimgtxrmpt.f	$$⊢\phi \to \left(x\in A⟼B\right)\in \mathrm{SMblFn}\left(S\right)$$
5		smfpimgtxrmpt.l	$$⊢\phi \to L\in {ℝ}^{*}$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
7	1 6 2 3 4 5	smfpimgtxrmptf	$$⊢\phi \to \left\{x\in A|L<B\right\}\in \left(S{\upharpoonright }_{𝑡}A\right)$$