smfpimne2

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

	Ref	Expression
Hypotheses	smfpimne2.p	$⊢ Ⅎ x φ$
	smfpimne2.x	$⊢ \underline{Ⅎ} x F$
	smfpimne2.s	$⊢ φ \to S \in SAlg$
	smfpimne2.f	$⊢ φ \to F \in SMblFn (S)$
	smfpimne2.d	$⊢ D = dom F$
Assertion	smfpimne2	$⊢ φ \to \{x \in D \| F (x) \neq A\} \in (S ↾_{𝑡} D)$

Proof

Step	Hyp	Ref	Expression
1		smfpimne2.p	$⊢ Ⅎ x φ$
2		smfpimne2.x	$⊢ \underline{Ⅎ} x F$
3		smfpimne2.s	$⊢ φ \to S \in SAlg$
4		smfpimne2.f	$⊢ φ \to F \in SMblFn (S)$
5		smfpimne2.d	$⊢ D = dom F$
6		nfv	$⊢ Ⅎ x A \in ℝ^{*}$
7	1 6	nfan	$⊢ Ⅎ x (φ \land A \in ℝ^{*})$
8	3	adantr	$⊢ (φ \land A \in ℝ^{*}) \to S \in SAlg$
9	4	adantr	$⊢ (φ \land A \in ℝ^{*}) \to F \in SMblFn (S)$
10		simpr	$⊢ (φ \land A \in ℝ^{}) \to A \in ℝ^{}$
11	7 2 8 9 5 10	smfpimne	$⊢ (φ \land A \in ℝ^{*}) \to \{x \in D \| F (x) \neq A\} \in (S ↾_{𝑡} D)$
12	2	nfdm	$⊢ \underline{Ⅎ} x dom F$
13	5 12	nfcxfr	$⊢ \underline{Ⅎ} x D$
14	13	ssrab2f	$⊢ \{x \in D \| F (x) \neq A\} \subseteq D$
15	14	a1i	$⊢ (φ \land \neg A \in ℝ^{*}) \to \{x \in D \| F (x) \neq A\} \subseteq D$
16		nfv	$⊢ Ⅎ x \neg A \in ℝ^{*}$
17	1 16	nfan	$⊢ Ⅎ x (φ \land \neg A \in ℝ^{*})$
18		ssidd	$⊢ (φ \land \neg A \in ℝ^{*}) \to D \subseteq D$
19		nne	$⊢ \neg F (x) \neq A \leftrightarrow F (x) = A$
20		simpr	$⊢ ((φ \land x \in D) \land F (x) = A) \to F (x) = A$
21	3 4 5	smff	$⊢ φ \to F : D ⟶ ℝ$
22	21	ffvelcdmda	$⊢ (φ \land x \in D) \to F (x) \in ℝ$
23	22	rexrd	$⊢ (φ \land x \in D) \to F (x) \in ℝ^{*}$
24	23	adantr	$⊢ ((φ \land x \in D) \land F (x) = A) \to F (x) \in ℝ^{*}$
25	20 24	eqeltrrd	$⊢ ((φ \land x \in D) \land F (x) = A) \to A \in ℝ^{*}$
26	19 25	sylan2b	$⊢ ((φ \land x \in D) \land \neg F (x) \neq A) \to A \in ℝ^{*}$
27	26	adantllr	$⊢ (((φ \land \neg A \in ℝ^{}) \land x \in D) \land \neg F (x) \neq A) \to A \in ℝ^{}$
28		simpllr	$⊢ (((φ \land \neg A \in ℝ^{}) \land x \in D) \land \neg F (x) \neq A) \to \neg A \in ℝ^{}$
29	27 28	condan	$⊢ ((φ \land \neg A \in ℝ^{*}) \land x \in D) \to F (x) \neq A$
30	13 13 17 18 29	ssrabdf	$⊢ (φ \land \neg A \in ℝ^{*}) \to D \subseteq \{x \in D \| F (x) \neq A\}$
31	15 30	eqssd	$⊢ (φ \land \neg A \in ℝ^{*}) \to \{x \in D \| F (x) \neq A\} = D$
32	3 4 5	smfdmss	$⊢ φ \to D \subseteq ⋃ S$
33	3 32	subsaluni	$⊢ φ \to D \in (S ↾_{𝑡} D)$
34	33	adantr	$⊢ (φ \land \neg A \in ℝ^{*}) \to D \in (S ↾_{𝑡} D)$
35	31 34	eqeltrd	$⊢ (φ \land \neg A \in ℝ^{*}) \to \{x \in D \| F (x) \neq A\} \in (S ↾_{𝑡} D)$
36	11 35	pm2.61dan	$⊢ φ \to \{x \in D \| F (x) \neq A\} \in (S ↾_{𝑡} D)$

Metamath Proof Explorer

Theorem smfpimne2

Proof