Metamath Proof Explorer

Theorem smfpreimage

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

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

Proof

Step	Hyp	Ref	Expression
1		smfpreimage.s	\|- ( ph -> S e. SAlg )
2		smfpreimage.f	\|- ( ph -> F e. ( SMblFn ` S ) )
3		smfpreimage.d	\|- D = dom F
4		smfpreimage.a	\|- ( ph -> A e. RR )
5	1 3	issmfge	\|- ( ph -> ( F e. ( SMblFn ` S ) <-> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D \| a <_ ( F ` x ) } e. ( S \|`t D ) ) ) )
6	2 5	mpbid	\|- ( ph -> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D \| a <_ ( F ` x ) } e. ( S \|`t D ) ) )
7	6	simp3d	\|- ( ph -> A. a e. RR { x e. D \| a <_ ( F ` x ) } e. ( S \|`t D ) )
8		breq1	\|- ( a = A -> ( a <_ ( F ` x ) <-> A <_ ( F ` x ) ) )
9	8	rabbidv	\|- ( a = A -> { x e. D \| a <_ ( F ` x ) } = { x e. D \| A <_ ( F ` x ) } )
10	9	eleq1d	\|- ( a = A -> ( { x e. D \| a <_ ( F ` x ) } e. ( S \|`t D ) <-> { x e. D \| A <_ ( F ` x ) } e. ( S \|`t D ) ) )
11	10	rspcva	\|- ( ( A e. RR /\ A. a e. RR { x e. D \| a <_ ( F ` x ) } e. ( S \|`t D ) ) -> { x e. D \| A <_ ( F ` x ) } e. ( S \|`t D ) )
12	4 7 11	syl2anc	\|- ( ph -> { x e. D \| A <_ ( F ` x ) } e. ( S \|`t D ) )