Theorem smfpimltxr

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021) (Revised by Glauco Siliprandi, 15-Dec-2024)

	Ref	Expression
Hypotheses	smfpimltxr.x	⊢ Ⅎ 𝑥 𝐹
	smfpimltxr.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfpimltxr.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
	smfpimltxr.d	⊢ 𝐷 = dom 𝐹
	smfpimltxr.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
Assertion	smfpimltxr	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		smfpimltxr.x	⊢ Ⅎ 𝑥 𝐹
2		smfpimltxr.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		smfpimltxr.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
4		smfpimltxr.d	⊢ 𝐷 = dom 𝐹
5		smfpimltxr.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
6		breq2	⊢ ( 𝐴 = +∞ → ( ( 𝐹 ‘ 𝑥 ) < 𝐴 ↔ ( 𝐹 ‘ 𝑥 ) < +∞ ) )
7	6	rabbidv	⊢ ( 𝐴 = +∞ → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < +∞ } )
8	1	nfdm	⊢ Ⅎ 𝑥 dom 𝐹
9	4 8	nfcxfr	⊢ Ⅎ 𝑥 𝐷
10	2 3 4	smff	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
11	1 9 10	pimltpnf2f	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < +∞ } = 𝐷 )
12	7 11	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } = 𝐷 )
13	2 3 4	smfdmss	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
14	2 13	subsaluni	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑆 ↾t 𝐷 ) )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → 𝐷 ∈ ( 𝑆 ↾t 𝐷 ) )
16	12 15	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
17		breq2	⊢ ( 𝐴 = -∞ → ( ( 𝐹 ‘ 𝑥 ) < 𝐴 ↔ ( 𝐹 ‘ 𝑥 ) < -∞ ) )
18	17	rabbidv	⊢ ( 𝐴 = -∞ → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < -∞ } )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < -∞ } )
20	10	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → 𝐹 : 𝐷 ⟶ ℝ )
21	1 9 20	pimltmnf2f	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < -∞ } = ∅ )
22	19 21	eqtrd	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } = ∅ )
23	3	dmexd	⊢ ( 𝜑 → dom 𝐹 ∈ V )
24	4 23	eqeltrid	⊢ ( 𝜑 → 𝐷 ∈ V )
25		eqid	⊢ ( 𝑆 ↾t 𝐷 ) = ( 𝑆 ↾t 𝐷 )
26	2 24 25	subsalsal	⊢ ( 𝜑 → ( 𝑆 ↾t 𝐷 ) ∈ SAlg )
27	26	0sald	⊢ ( 𝜑 → ∅ ∈ ( 𝑆 ↾t 𝐷 ) )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → ∅ ∈ ( 𝑆 ↾t 𝐷 ) )
29	22 28	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
30	29	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ +∞ ) ∧ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
31		simpll	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ +∞ ) ∧ ¬ 𝐴 = -∞ ) → 𝜑 )
32	31 5	syl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ +∞ ) ∧ ¬ 𝐴 = -∞ ) → 𝐴 ∈ ℝ* )
33		neqne	⊢ ( ¬ 𝐴 = -∞ → 𝐴 ≠ -∞ )
34	33	adantl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ +∞ ) ∧ ¬ 𝐴 = -∞ ) → 𝐴 ≠ -∞ )
35		simplr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ +∞ ) ∧ ¬ 𝐴 = -∞ ) → 𝐴 ≠ +∞ )
36	32 34 35	xrred	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ +∞ ) ∧ ¬ 𝐴 = -∞ ) → 𝐴 ∈ ℝ )
37	2	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝑆 ∈ SAlg )
38	3	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
39		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
40	1 37 38 4 39	smfpreimaltf	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
41	31 36 40	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ +∞ ) ∧ ¬ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
42	30 41	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝐴 ≠ +∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
43	16 42	pm2.61dane	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )