Theorem smfdmmblpimne

Description: If a measurable function w.r.t. to a sigma-algebra has domain in the sigma-algebra, the set of elements that are not mapped to a given real, is in the sigma-algebra (Contributed by Glauco Siliprandi, 5-Jan-2025)

	Ref	Expression
Hypotheses	smfdmmblpimne.1	|- F/ x ph
	smfdmmblpimne.2	|- F/_ x A
	smfdmmblpimne.3	|- ( ph -> S e. SAlg )
	smfdmmblpimne.4	|- ( ph -> A e. S )
	smfdmmblpimne.5	|- ( ( ph /\ x e. A ) -> B e. RR )
	smfdmmblpimne.6	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
	smfdmmblpimne.7	|- ( ph -> C e. RR )
	smfdmmblpimne.8	|- D = { x e. A | B =/= C }
Assertion	smfdmmblpimne	|- ( ph -> D e. S )

Proof

Step	Hyp	Ref	Expression
1		smfdmmblpimne.1	|- F/ x ph
2		smfdmmblpimne.2	|- F/_ x A
3		smfdmmblpimne.3	|- ( ph -> S e. SAlg )
4		smfdmmblpimne.4	|- ( ph -> A e. S )
5		smfdmmblpimne.5	|- ( ( ph /\ x e. A ) -> B e. RR )
6		smfdmmblpimne.6	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
7		smfdmmblpimne.7	|- ( ph -> C e. RR )
8		smfdmmblpimne.8	|- D = { x e. A | B =/= C }
9	5	rexrd	|- ( ( ph /\ x e. A ) -> B e. RR* )
10	7	rexrd	|- ( ph -> C e. RR* )
11	10	adantr	|- ( ( ph /\ x e. A ) -> C e. RR* )
12	1 9 11	pimxrneun	|- ( ph -> { x e. A | B =/= C } = ( { x e. A | B < C } u. { x e. A | C < B } ) )
13	8 12	eqtrid	|- ( ph -> D = ( { x e. A | B < C } u. { x e. A | C < B } ) )
14	3 4	salrestss	|- ( ph -> ( S |`t A ) C_ S )
15	1 2 3 5 6 10	smfpimltxrmptf	|- ( ph -> { x e. A | B < C } e. ( S |`t A ) )
16	14 15	sseldd	|- ( ph -> { x e. A | B < C } e. S )
17	1 2 3 5 6 10	smfpimgtxrmptf	|- ( ph -> { x e. A | C < B } e. ( S |`t A ) )
18	14 17	sseldd	|- ( ph -> { x e. A | C < B } e. S )
19	3 16 18	saluncld	|- ( ph -> ( { x e. A | B < C } u. { x e. A | C < B } ) e. S )
20	13 19	eqeltrd	|- ( ph -> D e. S )