Theorem issmfle2d

Description: A sufficient condition for " F being a measurable function w.r.t. to the sigma-algebra S ". (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	issmfle2d.a	⊢ Ⅎ 𝑎 𝜑
	issmfle2d.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	issmfle2d.d	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
	issmfle2d.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
	issmfle2d.l	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,] 𝑎 ) ) ∈ ( 𝑆 ↾t 𝐷 ) )
Assertion	issmfle2d	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		issmfle2d.a	⊢ Ⅎ 𝑎 𝜑
2		issmfle2d.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		issmfle2d.d	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
4		issmfle2d.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
5		issmfle2d.l	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,] 𝑎 ) ) ∈ ( 𝑆 ↾t 𝐷 ) )
6	4	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐹 : 𝐷 ⟶ ℝ )
7		rexr	⊢ ( 𝑎 ∈ ℝ → 𝑎 ∈ ℝ* )
8	7	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ* )
9	6 8	preimaiocmnf	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,] 𝑎 ) ) = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≤ 𝑎 } )
10	9 5	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≤ 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) )
11	1 2 3 4 10	issmfled	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )