Theorem smfpimne

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of reals that are different from a value in the extended reals is in the subspace of sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 5-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		smfpimne.p	|- F/ x ph
2		smfpimne.x	|- F/_ x F
3		smfpimne.s	|- ( ph -> S e. SAlg )
4		smfpimne.f	|- ( ph -> F e. ( SMblFn ` S ) )
5		smfpimne.d	|- D = dom F
6		smfpimne.a	|- ( ph -> A e. RR* )
7	3 4 5	smff	|- ( ph -> F : D --> RR )
8	7	ffvelcdmda	|- ( ( ph /\ x e. D ) -> ( F ` x ) e. RR )
9	8	rexrd	|- ( ( ph /\ x e. D ) -> ( F ` x ) e. RR* )
10	6	adantr	|- ( ( ph /\ x e. D ) -> A e. RR* )
11	1 9 10	pimxrneun	|- ( ph -> { x e. D | ( F ` x ) =/= A } = ( { x e. D | ( F ` x ) < A } u. { x e. D | A < ( F ` x ) } ) )
12	3 4 5	smfdmss	|- ( ph -> D C_ U. S )
13	3 12	subsaluni	|- ( ph -> D e. ( S |`t D ) )
14		eqid	|- ( S |`t D ) = ( S |`t D )
15	3 13 14	subsalsal	|- ( ph -> ( S |`t D ) e. SAlg )
16	2 3 4 5 6	smfpimltxr	|- ( ph -> { x e. D | ( F ` x ) < A } e. ( S |`t D ) )
17	2 3 4 5 6	smfpimgtxr	|- ( ph -> { x e. D | A < ( F ` x ) } e. ( S |`t D ) )
18	15 16 17	saluncld	|- ( ph -> ( { x e. D | ( F ` x ) < A } u. { x e. D | A < ( F ` x ) } ) e. ( S |`t D ) )
19	11 18	eqeltrd	|- ( ph -> { x e. D | ( F ` x ) =/= A } e. ( S |`t D ) )