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	⊢ Ⅎ 𝑥 𝜑
	smfpimne.x	⊢ Ⅎ 𝑥 𝐹
	smfpimne.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfpimne.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
	smfpimne.d	⊢ 𝐷 = dom 𝐹
	smfpimne.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
Assertion	smfpimne	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		smfpimne.p	⊢ Ⅎ 𝑥 𝜑
2		smfpimne.x	⊢ Ⅎ 𝑥 𝐹
3		smfpimne.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		smfpimne.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
5		smfpimne.d	⊢ 𝐷 = dom 𝐹
6		smfpimne.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
7	3 4 5	smff	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
8	7	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
9	8	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
10	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ ℝ* )
11	1 9 10	pimxrneun	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝐴 } = ( { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∪ { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ) )
12	3 4 5	smfdmss	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
13	3 12	subsaluni	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑆 ↾t 𝐷 ) )
14		eqid	⊢ ( 𝑆 ↾t 𝐷 ) = ( 𝑆 ↾t 𝐷 )
15	3 13 14	subsalsal	⊢ ( 𝜑 → ( 𝑆 ↾t 𝐷 ) ∈ SAlg )
16	2 3 4 5 6	smfpimltxr	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
17	2 3 4 5 6	smfpimgtxr	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
18	15 16 17	saluncld	⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∪ { 𝑥 ∈ 𝐷 ∣ 𝐴 < ( 𝐹 ‘ 𝑥 ) } ) ∈ ( 𝑆 ↾t 𝐷 ) )
19	11 18	eqeltrd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )