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	$⊢ Ⅎ x φ$
	smfpimne.x	$⊢ \underline{Ⅎ} x F$
	smfpimne.s	$⊢ φ \to S \in SAlg$
	smfpimne.f	$⊢ φ \to F \in SMblFn (S)$
	smfpimne.d	$⊢ D = dom F$
	smfpimne.a	$⊢ φ \to A \in ℝ^{*}$
Assertion	smfpimne	$⊢ φ \to \{x \in D \| F (x) \neq A\} \in (S ↾_{𝑡} D)$

Proof

Step	Hyp	Ref	Expression
1		smfpimne.p	$⊢ Ⅎ x φ$
2		smfpimne.x	$⊢ \underline{Ⅎ} x F$
3		smfpimne.s	$⊢ φ \to S \in SAlg$
4		smfpimne.f	$⊢ φ \to F \in SMblFn (S)$
5		smfpimne.d	$⊢ D = dom F$
6		smfpimne.a	$⊢ φ \to A \in ℝ^{*}$
7	3 4 5	smff	$⊢ φ \to F : D ⟶ ℝ$
8	7	ffvelcdmda	$⊢ (φ \land x \in D) \to F (x) \in ℝ$
9	8	rexrd	$⊢ (φ \land x \in D) \to F (x) \in ℝ^{*}$
10	6	adantr	$⊢ (φ \land x \in D) \to A \in ℝ^{*}$
11	1 9 10	pimxrneun	$⊢ φ \to \{x \in D \| F (x) \neq A\} = \{x \in D \| F (x) < A\} \cup \{x \in D \| A < F (x)\}$
12	3 4 5	smfdmss	$⊢ φ \to D \subseteq ⋃ S$
13	3 12	subsaluni	$⊢ φ \to D \in (S ↾_{𝑡} D)$
14		eqid	$⊢ S ↾_{𝑡} D = S ↾_{𝑡} D$
15	3 13 14	subsalsal	$⊢ φ \to S ↾_{𝑡} D \in SAlg$
16	2 3 4 5 6	smfpimltxr	$⊢ φ \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$
17	2 3 4 5 6	smfpimgtxr	$⊢ φ \to \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$
18	15 16 17	saluncld	$⊢ φ \to \{x \in D \| F (x) < A\} \cup \{x \in D \| A < F (x)\} \in (S ↾_{𝑡} D)$
19	11 18	eqeltrd	$⊢ φ \to \{x \in D \| F (x) \neq A\} \in (S ↾_{𝑡} D)$

Metamath Proof Explorer

Theorem smfpimne

Proof