Theorem mbfmcnvima

Description: The preimage by a measurable function is a measurable set. (Contributed by Thierry Arnoux, 23-Jan-2017)

	Ref	Expression
Hypotheses	mbfmf.1	|- ( ph -> S e. U. ran sigAlgebra )
	mbfmf.2	|- ( ph -> T e. U. ran sigAlgebra )
	mbfmf.3	|- ( ph -> F e. ( S MblFnM T ) )
	mbfmcnvima.4	|- ( ph -> A e. T )
Assertion	mbfmcnvima	|- ( ph -> ( `' F " A ) e. S )

Proof

Step	Hyp	Ref	Expression
1		mbfmf.1	|- ( ph -> S e. U. ran sigAlgebra )
2		mbfmf.2	|- ( ph -> T e. U. ran sigAlgebra )
3		mbfmf.3	|- ( ph -> F e. ( S MblFnM T ) )
4		mbfmcnvima.4	|- ( ph -> A e. T )
5		imaeq2	|- ( x = A -> ( `' F " x ) = ( `' F " A ) )
6	5	eleq1d	|- ( x = A -> ( ( `' F " x ) e. S <-> ( `' F " A ) e. S ) )
7	1 2	ismbfm	|- ( ph -> ( F e. ( S MblFnM T ) <-> ( F e. ( U. T ^m U. S ) /\ A. x e. T ( `' F " x ) e. S ) ) )
8	3 7	mpbid	|- ( ph -> ( F e. ( U. T ^m U. S ) /\ A. x e. T ( `' F " x ) e. S ) )
9	8	simprd	|- ( ph -> A. x e. T ( `' F " x ) e. S )
10	6 9 4	rspcdva	|- ( ph -> ( `' F " A ) e. S )