Theorem sibff

Description: A simple function is a function. (Contributed by Thierry Arnoux, 19-Feb-2018)

	Ref	Expression
Hypotheses	sitgval.b	$$⊢B={\mathrm{Base}}_W$$
	sitgval.j	$$⊢J=\mathrm{TopOpen}\left(W\right)$$
	sitgval.s	$$⊢S=𝛔\left(J\right)$$
	sitgval.0	$$⊢\underset{\dot{}}{0}=0_W$$
	sitgval.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	sitgval.h	$$⊢H=\mathrm{ℝHom}\left(\mathrm{Scalar}\left(W\right)\right)$$
	sitgval.1	$$⊢\phi \to W\in V$$
	sitgval.2	$$⊢\phi \to M\in \bigcup \mathrm{ran}\mathrm{measures}$$
	sibfmbl.1	$$⊢\phi \to F\in {\Im }_M^W$$
Assertion	sibff	$$⊢\phi \to F:\bigcup \mathrm{dom}M⟶\bigcup J$$

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	$$⊢B={\mathrm{Base}}_W$$
2		sitgval.j	$$⊢J=\mathrm{TopOpen}\left(W\right)$$
3		sitgval.s	$$⊢S=𝛔\left(J\right)$$
4		sitgval.0	$$⊢\underset{\dot{}}{0}=0_W$$
5		sitgval.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		sitgval.h	$$⊢H=\mathrm{ℝHom}\left(\mathrm{Scalar}\left(W\right)\right)$$
7		sitgval.1	$$⊢\phi \to W\in V$$
8		sitgval.2	$$⊢\phi \to M\in \bigcup \mathrm{ran}\mathrm{measures}$$
9		sibfmbl.1	$$⊢\phi \to F\in {\Im }_M^W$$
10		dmmeas	$$⊢M\in \bigcup \mathrm{ran}\mathrm{measures}\to \mathrm{dom}M\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
11	8 10	syl	$$⊢\phi \to \mathrm{dom}M\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
12		fvexd	$$⊢\phi \to \mathrm{TopOpen}\left(W\right)\in \mathrm{V}$$
13	2 12	eqeltrid	$$⊢\phi \to J\in \mathrm{V}$$
14	13	sgsiga	$$⊢\phi \to 𝛔\left(J\right)\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
15	3 14	eqeltrid	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
16	1 2 3 4 5 6 7 8 9	sibfmbl	$$⊢\phi \to F\in \left(\mathrm{dom}M{\mathrm{MblFn}}_{\mu }S\right)$$
17	11 15 16	mbfmf	$$⊢\phi \to F:\bigcup \mathrm{dom}M⟶\bigcup S$$
18	3	unieqi	$$⊢\bigcup S=\bigcup 𝛔\left(J\right)$$
19		unisg	$$⊢J\in \mathrm{V}\to \bigcup 𝛔\left(J\right)=\bigcup J$$
20	13 19	syl	$$⊢\phi \to \bigcup 𝛔\left(J\right)=\bigcup J$$
21	18 20	syl5eq	$$⊢\phi \to \bigcup S=\bigcup J$$
22	21	feq3d	$$⊢\phi \to \left(F:\bigcup \mathrm{dom}M⟶\bigcup S\leftrightarrow F:\bigcup \mathrm{dom}M⟶\bigcup J\right)$$
23	17 22	mpbid	$$⊢\phi \to F:\bigcup \mathrm{dom}M⟶\bigcup J$$