Theorem smfpimioo

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfpimioo.s	|- ( ph -> S e. SAlg )
	smfpimioo.f	|- ( ph -> F e. ( SMblFn ` S ) )
	smfpimioo.d	|- D = dom F
	smfpimioo.a	|- ( ph -> A e. RR* )
	smfpimioo.b	|- ( ph -> B e. RR* )
Assertion	smfpimioo	|- ( ph -> ( `' F " ( A (,) B ) ) e. ( S |`t D ) )

Proof

Step	Hyp	Ref	Expression
1		smfpimioo.s	|- ( ph -> S e. SAlg )
2		smfpimioo.f	|- ( ph -> F e. ( SMblFn ` S ) )
3		smfpimioo.d	|- D = dom F
4		smfpimioo.a	|- ( ph -> A e. RR* )
5		smfpimioo.b	|- ( ph -> B e. RR* )
6	1 2 3	smff	|- ( ph -> F : D --> RR )
7	6	feqmptd	|- ( ph -> F = ( x e. D |-> ( F ` x ) ) )
8	7	cnveqd	|- ( ph -> `' F = `' ( x e. D |-> ( F ` x ) ) )
9	8	imaeq1d	|- ( ph -> ( `' F " ( A (,) B ) ) = ( `' ( x e. D |-> ( F ` x ) ) " ( A (,) B ) ) )
10		eqid	|- ( x e. D |-> ( F ` x ) ) = ( x e. D |-> ( F ` x ) )
11	10	mptpreima	|- ( `' ( x e. D |-> ( F ` x ) ) " ( A (,) B ) ) = { x e. D | ( F ` x ) e. ( A (,) B ) }
12	11	a1i	|- ( ph -> ( `' ( x e. D |-> ( F ` x ) ) " ( A (,) B ) ) = { x e. D | ( F ` x ) e. ( A (,) B ) } )
13	9 12	eqtrd	|- ( ph -> ( `' F " ( A (,) B ) ) = { x e. D | ( F ` x ) e. ( A (,) B ) } )
14		nfv	|- F/ x ph
15	1	uniexd	|- ( ph -> U. S e. _V )
16	1 2 3	smfdmss	|- ( ph -> D C_ U. S )
17	15 16	ssexd	|- ( ph -> D e. _V )
18	6	ffvelrnda	|- ( ( ph /\ x e. D ) -> ( F ` x ) e. RR )
19	7 2	eqeltrrd	|- ( ph -> ( x e. D |-> ( F ` x ) ) e. ( SMblFn ` S ) )
20	14 1 17 18 19 4 5	smfpimioompt	|- ( ph -> { x e. D | ( F ` x ) e. ( A (,) B ) } e. ( S |`t D ) )
21	13 20	eqeltrd	|- ( ph -> ( `' F " ( A (,) B ) ) e. ( S |`t D ) )