Theorem smfdmss

Description: The domain of a function measurable w.r.t. to a sigma-algebra, is a subset of the set underlying the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfdmss.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
	smfdmss.f	$$⊢\phi \to F\in \mathrm{SMblFn}\left(S\right)$$
	smfdmss.d	$$⊢D=\mathrm{dom}F$$
Assertion	smfdmss	$$⊢\phi \to D\subseteq \bigcup S$$

Proof

Step	Hyp	Ref	Expression
1		smfdmss.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
2		smfdmss.f	$$⊢\phi \to F\in \mathrm{SMblFn}\left(S\right)$$
3		smfdmss.d	$$⊢D=\mathrm{dom}F$$
4	1 3	issmf	$$⊢\phi \to \left(F\in \mathrm{SMblFn}\left(S\right)\leftrightarrow \left(D\subseteq \bigcup S\wedge F:D⟶ℝ\wedge \forall a\in ℝ\left\{x\in D|F\left(x\right)<a\right\}\in \left(S{\upharpoonright }_{𝑡}D\right)\right)\right)$$
5	2 4	mpbid	$$⊢\phi \to \left(D\subseteq \bigcup S\wedge F:D⟶ℝ\wedge \forall a\in ℝ\left\{x\in D|F\left(x\right)<a\right\}\in \left(S{\upharpoonright }_{𝑡}D\right)\right)$$
6	5	simp1d	$$⊢\phi \to D\subseteq \bigcup S$$