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

Proof

Step	Hyp	Ref	Expression
1		smfpimne2.p	⊢ Ⅎ 𝑥 𝜑
2		smfpimne2.x	⊢ Ⅎ 𝑥 𝐹
3		smfpimne2.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		smfpimne2.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
5		smfpimne2.d	⊢ 𝐷 = dom 𝐹
6		nfv	⊢ Ⅎ 𝑥 𝐴 ∈ ℝ*
7	1 6	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝐴 ∈ ℝ* )
8	3	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ* ) → 𝑆 ∈ SAlg )
9	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ* ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
10		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ* ) → 𝐴 ∈ ℝ* )
11	7 2 8 9 5 10	smfpimne	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ* ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
12	2	nfdm	⊢ Ⅎ 𝑥 dom 𝐹
13	5 12	nfcxfr	⊢ Ⅎ 𝑥 𝐷
14	13	ssrab2f	⊢ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝐴 } ⊆ 𝐷
15	14	a1i	⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ* ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝐴 } ⊆ 𝐷 )
16		nfv	⊢ Ⅎ 𝑥 ¬ 𝐴 ∈ ℝ*
17	1 16	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ* )
18		ssidd	⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ* ) → 𝐷 ⊆ 𝐷 )
19		nne	⊢ ( ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝐴 ↔ ( 𝐹 ‘ 𝑥 ) = 𝐴 )
20		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐴 )
21	3 4 5	smff	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
22	21	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
23	22	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
24	23	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
25	20 24	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝐴 ) → 𝐴 ∈ ℝ* )
26	19 25	sylan2b	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝐴 ) → 𝐴 ∈ ℝ* )
27	26	adantllr	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝐴 ) → 𝐴 ∈ ℝ* )
28		simpllr	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝐴 ) → ¬ 𝐴 ∈ ℝ* )
29	27 28	condan	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ* ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑥 ) ≠ 𝐴 )
30	13 13 17 18 29	ssrabdf	⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ* ) → 𝐷 ⊆ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝐴 } )
31	15 30	eqssd	⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ* ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝐴 } = 𝐷 )
32	3 4 5	smfdmss	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
33	3 32	subsaluni	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑆 ↾t 𝐷 ) )
34	33	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ* ) → 𝐷 ∈ ( 𝑆 ↾t 𝐷 ) )
35	31 34	eqeltrd	⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ* ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
36	11 35	pm2.61dan	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )