Theorem isanmbfmOLD

Description: Obsolete version of isanmbfm as of 13-Jan-2025. (Contributed by Thierry Arnoux, 30-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mbfmf.1	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
	mbfmf.2	$$⊢\phi \to T\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
	mbfmf.3	$$⊢\phi \to F\in \left(S{\mathrm{MblFn}}_{\mu }T\right)$$
Assertion	isanmbfmOLD	$$⊢\phi \to F\in \bigcup \mathrm{ran}{\mathrm{MblFn}}_{\mu }$$

Proof

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