Theorem sibff

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

	Ref	Expression
Hypotheses	sitgval.b	|- B = ( Base ` W )
	sitgval.j	|- J = ( TopOpen ` W )
	sitgval.s	|- S = ( sigaGen ` J )
	sitgval.0	|- .0. = ( 0g ` W )
	sitgval.x	|- .x. = ( .s ` W )
	sitgval.h	|- H = ( RRHom ` ( Scalar ` W ) )
	sitgval.1	|- ( ph -> W e. V )
	sitgval.2	|- ( ph -> M e. U. ran measures )
	sibfmbl.1	|- ( ph -> F e. dom ( W sitg M ) )
Assertion	sibff	|- ( ph -> F : U. dom M --> U. J )

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	|- B = ( Base ` W )
2		sitgval.j	|- J = ( TopOpen ` W )
3		sitgval.s	|- S = ( sigaGen ` J )
4		sitgval.0	|- .0. = ( 0g ` W )
5		sitgval.x	|- .x. = ( .s ` W )
6		sitgval.h	|- H = ( RRHom ` ( Scalar ` W ) )
7		sitgval.1	|- ( ph -> W e. V )
8		sitgval.2	|- ( ph -> M e. U. ran measures )
9		sibfmbl.1	|- ( ph -> F e. dom ( W sitg M ) )
10		dmmeas	|- ( M e. U. ran measures -> dom M e. U. ran sigAlgebra )
11	8 10	syl	|- ( ph -> dom M e. U. ran sigAlgebra )
12		fvexd	|- ( ph -> ( TopOpen ` W ) e. _V )
13	2 12	eqeltrid	|- ( ph -> J e. _V )
14	13	sgsiga	|- ( ph -> ( sigaGen ` J ) e. U. ran sigAlgebra )
15	3 14	eqeltrid	|- ( ph -> S e. U. ran sigAlgebra )
16	1 2 3 4 5 6 7 8 9	sibfmbl	|- ( ph -> F e. ( dom M MblFnM S ) )
17	11 15 16	mbfmf	|- ( ph -> F : U. dom M --> U. S )
18	3	unieqi	|- U. S = U. ( sigaGen ` J )
19		unisg	|- ( J e. _V -> U. ( sigaGen ` J ) = U. J )
20	13 19	syl	|- ( ph -> U. ( sigaGen ` J ) = U. J )
21	18 20	syl5eq	|- ( ph -> U. S = U. J )
22	21	feq3d	|- ( ph -> ( F : U. dom M --> U. S <-> F : U. dom M --> U. J ) )
23	17 22	mpbid	|- ( ph -> F : U. dom M --> U. J )