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)

	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	7	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < +∞ } )
9	1 2 4	issmff	⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
10	3 9	mpbid	⊢ ( 𝜑 → ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
11	10	simp2d	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
12	1 11	pimltpnf2	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < +∞ } = 𝐷 )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < +∞ } = 𝐷 )
14		eqidd	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → 𝐷 = 𝐷 )
15	8 13 14	3eqtrd	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } = 𝐷 )
16	10	simp1d	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
17	2 16	restuni4	⊢ ( 𝜑 → ∪ ( 𝑆 ↾t 𝐷 ) = 𝐷 )
18	17	eqcomd	⊢ ( 𝜑 → 𝐷 = ∪ ( 𝑆 ↾t 𝐷 ) )
19	3	dmexd	⊢ ( 𝜑 → dom 𝐹 ∈ V )
20	4 19	eqeltrid	⊢ ( 𝜑 → 𝐷 ∈ V )
21		eqid	⊢ ( 𝑆 ↾t 𝐷 ) = ( 𝑆 ↾t 𝐷 )
22	2 20 21	subsalsal	⊢ ( 𝜑 → ( 𝑆 ↾t 𝐷 ) ∈ SAlg )
23	22	salunid	⊢ ( 𝜑 → ∪ ( 𝑆 ↾t 𝐷 ) ∈ ( 𝑆 ↾t 𝐷 ) )
24	18 23	eqeltrd	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑆 ↾t 𝐷 ) )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → 𝐷 ∈ ( 𝑆 ↾t 𝐷 ) )
26	15 25	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
27		neqne	⊢ ( ¬ 𝐴 = +∞ → 𝐴 ≠ +∞ )
28	27	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = +∞ ) → 𝐴 ≠ +∞ )
29		breq2	⊢ ( 𝐴 = -∞ → ( ( 𝐹 ‘ 𝑥 ) < 𝐴 ↔ ( 𝐹 ‘ 𝑥 ) < -∞ ) )
30	29	rabbidv	⊢ ( 𝐴 = -∞ → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < -∞ } )
31	30	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < -∞ } )
32	11	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → 𝐹 : 𝐷 ⟶ ℝ )
33	1 32	pimltmnf2	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < -∞ } = ∅ )
34	31 33	eqtrd	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } = ∅ )
35	22	0sald	⊢ ( 𝜑 → ∅ ∈ ( 𝑆 ↾t 𝐷 ) )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → ∅ ∈ ( 𝑆 ↾t 𝐷 ) )
37	34 36	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
38	37	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ +∞ ) ∧ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
39		simpll	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ +∞ ) ∧ ¬ 𝐴 = -∞ ) → 𝜑 )
40	39 5	syl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ +∞ ) ∧ ¬ 𝐴 = -∞ ) → 𝐴 ∈ ℝ* )
41		neqne	⊢ ( ¬ 𝐴 = -∞ → 𝐴 ≠ -∞ )
42	41	adantl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ +∞ ) ∧ ¬ 𝐴 = -∞ ) → 𝐴 ≠ -∞ )
43		simplr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ +∞ ) ∧ ¬ 𝐴 = -∞ ) → 𝐴 ≠ +∞ )
44	40 42 43	xrred	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ +∞ ) ∧ ¬ 𝐴 = -∞ ) → 𝐴 ∈ ℝ )
45	2	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝑆 ∈ SAlg )
46	3	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
47		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
48	1 45 46 4 47	smfpreimaltf	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
49	39 44 48	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ +∞ ) ∧ ¬ 𝐴 = -∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
50	38 49	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝐴 ≠ +∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
51	28 50	syldan	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = +∞ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
52	26 51	pm2.61dan	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )