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	⊢ Ⅎ 𝑥 𝜑
	smfdmmblpimne.2	⊢ Ⅎ 𝑥 𝐴
	smfdmmblpimne.3	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfdmmblpimne.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	smfdmmblpimne.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	smfdmmblpimne.6	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
	smfdmmblpimne.7	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	smfdmmblpimne.8	⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 }
Assertion	smfdmmblpimne	⊢ ( 𝜑 → 𝐷 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		smfdmmblpimne.1	⊢ Ⅎ 𝑥 𝜑
2		smfdmmblpimne.2	⊢ Ⅎ 𝑥 𝐴
3		smfdmmblpimne.3	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		smfdmmblpimne.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
5		smfdmmblpimne.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
6		smfdmmblpimne.6	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
7		smfdmmblpimne.7	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
8		smfdmmblpimne.8	⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 }
9	5	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ^* )
10	7	rexrd	⊢ ( 𝜑 → 𝐶 ∈ ℝ^* )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ^* )
12	1 9 11	pimxrneun	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } = ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
13	8 12	eqtrid	⊢ ( 𝜑 → 𝐷 = ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
14	3 4	salrestss	⊢ ( 𝜑 → ( 𝑆 ↾_t 𝐴 ) ⊆ 𝑆 )
15	1 2 3 5 6 10	smfpimltxrmptf	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∈ ( 𝑆 ↾_t 𝐴 ) )
16	14 15	sseldd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∈ 𝑆 )
17	1 2 3 5 6 10	smfpimgtxrmptf	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ∈ ( 𝑆 ↾_t 𝐴 ) )
18	14 17	sseldd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ∈ 𝑆 )
19	3 16 18	saluncld	⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) ∈ 𝑆 )
20	13 19	eqeltrd	⊢ ( 𝜑 → 𝐷 ∈ 𝑆 )

Metamath Proof Explorer

Theorem smfdmmblpimne

Proof