Theorem isanmbfm

Description: The predicate to be a measurable function. (Contributed by Thierry Arnoux, 30-Jan-2017) Remove hypotheses. (Revised by SN, 13-Jan-2025)

	Ref	Expression
Hypothesis	isanmbfm.1	$$⊢\phi \to F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)$$
Assertion	isanmbfm	$$⊢\phi \to F\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }$$

Proof

Step	Hyp	Ref	Expression
1		isanmbfm.1	$$⊢\phi \to F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)$$
2		ovssunirn	$$⊢S{\mathrm{MblFn}}_{\mu }T\subseteq \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }$$
3	2 1	sselid	$$⊢\phi \to F\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }$$