Theorem smfpreimagtf

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)

	Ref	Expression
Hypotheses	smfpreimagtf.x	$$⊢\underset{\_}{Ⅎ}xF$$
	smfpreimagtf.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
	smfpreimagtf.f	$$⊢\phi \to F\in \mathrm{SMblFn}\left(S\right)$$
	smfpreimagtf.d	$$⊢D=\mathrm{dom}F$$
	smfpreimagtf.a	$$⊢\phi \to A\in ℝ$$
Assertion	smfpreimagtf	$$⊢\phi \to \left\{x\in D|A<F\left(x\right)\right\}\in \left(S{\upharpoonright }_{𝑡}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		smfpreimagtf.x	$$⊢\underset{\_}{Ⅎ}xF$$
2		smfpreimagtf.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
3		smfpreimagtf.f	$$⊢\phi \to F\in \mathrm{SMblFn}\left(S\right)$$
4		smfpreimagtf.d	$$⊢D=\mathrm{dom}F$$
5		smfpreimagtf.a	$$⊢\phi \to A\in ℝ$$
6	1	nfdm	$$⊢\underset{\_}{Ⅎ}x\mathrm{dom}F$$
7	4 6	nfcxfr	$$⊢\underset{\_}{Ⅎ}xD$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}yD$$
9		nfv	$$⊢ℲyA<F\left(x\right)$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}x<$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
13	1 12	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(y\right)$$
14	10 11 13	nfbr	$$⊢ℲxA<F\left(y\right)$$
15		fveq2	$$⊢x=y\to F\left(x\right)=F\left(y\right)$$
16	15	breq2d	$$⊢x=y\to \left(A<F\left(x\right)\leftrightarrow A<F\left(y\right)\right)$$
17	7 8 9 14 16	cbvrabw	$$⊢\left\{x\in D|A<F\left(x\right)\right\}=\left\{y\in D|A<F\left(y\right)\right\}$$
18	17	a1i	$$⊢\phi \to \left\{x\in D|A<F\left(x\right)\right\}=\left\{y\in D|A<F\left(y\right)\right\}$$
19	2 3 4 5	smfpreimagt	$$⊢\phi \to \left\{y\in D|A<F\left(y\right)\right\}\in \left(S{\upharpoonright }_{𝑡}D\right)$$
20	18 19	eqeltrd	$$⊢\phi \to \left\{x\in D|A<F\left(x\right)\right\}\in \left(S{\upharpoonright }_{𝑡}D\right)$$