Theorem smfpreimaltf

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

Proof

Step	Hyp	Ref	Expression
1		smfpreimaltf.x	⊢ Ⅎ 𝑥 𝐹
2		smfpreimaltf.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		smfpreimaltf.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
4		smfpreimaltf.d	⊢ 𝐷 = dom 𝐹
5		smfpreimaltf.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6	1 2 4	issmff	⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
7	3 6	mpbid	⊢ ( 𝜑 → ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
8	7	simp3d	⊢ ( 𝜑 → ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) )
9		breq2	⊢ ( 𝑎 = 𝐴 → ( ( 𝐹 ‘ 𝑥 ) < 𝑎 ↔ ( 𝐹 ‘ 𝑥 ) < 𝐴 ) )
10	9	rabbidv	⊢ ( 𝑎 = 𝐴 → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } )
11	10	eleq1d	⊢ ( 𝑎 = 𝐴 → ( { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ↔ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
12	11	rspcva	⊢ ( ( 𝐴 ∈ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )
13	5 8 12	syl2anc	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐴 } ∈ ( 𝑆 ↾t 𝐷 ) )