Theorem smfpreimagtf

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

	Ref	Expression
Hypotheses	smfpreimagtf.x	|- F/_ x F
	smfpreimagtf.s	|- ( ph -> S e. SAlg )
	smfpreimagtf.f	|- ( ph -> F e. ( SMblFn ` S ) )
	smfpreimagtf.d	|- D = dom F
	smfpreimagtf.a	|- ( ph -> A e. RR )
Assertion	smfpreimagtf	|- ( ph -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )

Proof

Step	Hyp	Ref	Expression
1		smfpreimagtf.x	|- F/_ x F
2		smfpreimagtf.s	|- ( ph -> S e. SAlg )
3		smfpreimagtf.f	|- ( ph -> F e. ( SMblFn ` S ) )
4		smfpreimagtf.d	|- D = dom F
5		smfpreimagtf.a	|- ( ph -> A e. RR )
6	1	nfdm	|- F/_ x dom F
7	4 6	nfcxfr	|- F/_ x D
8		nfcv	|- F/_ y D
9		nfv	|- F/ y A < ( F ` x )
10		nfcv	|- F/_ x A
11		nfcv	|- F/_ x <
12		nfcv	|- F/_ x y
13	1 12	nffv	|- F/_ x ( F ` y )
14	10 11 13	nfbr	|- F/ x A < ( F ` y )
15		fveq2	|- ( x = y -> ( F ` x ) = ( F ` y ) )
16	15	breq2d	|- ( x = y -> ( A < ( F ` x ) <-> A < ( F ` y ) ) )
17	7 8 9 14 16	cbvrabw	|- { x e. D | A < ( F ` x ) } = { y e. D | A < ( F ` y ) }
18	17	a1i	|- ( ph -> { x e. D | A < ( F ` x ) } = { y e. D | A < ( F ` y ) } )
19	2 3 4 5	smfpreimagt	|- ( ph -> { y e. D | A < ( F ` y ) } e. ( S |`t D ) )
20	18 19	eqeltrd	|- ( ph -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )