Metamath Proof Explorer

Theorem smfpreimalt

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	smfpreimalt.s	$⊢ φ \to S \in SAlg$
		smfpreimalt.f	$⊢ φ \to F \in SMblFn (S)$
		smfpreimalt.d	$⊢ D = dom F$
		smfpreimalt.a	$⊢ φ \to A \in ℝ$
	Assertion	smfpreimalt	$⊢ φ \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$

Proof

Step	Hyp	Ref	Expression
1		smfpreimalt.s	$⊢ φ \to S \in SAlg$
2		smfpreimalt.f	$⊢ φ \to F \in SMblFn (S)$
3		smfpreimalt.d	$⊢ D = dom F$
4		smfpreimalt.a	$⊢ φ \to A \in ℝ$
5	1 3	issmf	$⊢ φ \to (F \in SMblFn (S) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D)))$
6	2 5	mpbid	$⊢ φ \to (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D))$
7	6	simp3d	$⊢ φ \to \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D)$
8		breq2	$⊢ a = A \to (F (x) < a \leftrightarrow F (x) < A)$
9	8	rabbidv	$⊢ a = A \to \{x \in D \| F (x) < a\} = \{x \in D \| F (x) < A\}$
10	9	eleq1d	$⊢ a = A \to (\{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D) \leftrightarrow \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D))$
11	10	rspcva	$⊢ (A \in ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D)) \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$
12	4 7 11	syl2anc	$⊢ φ \to \{x \in D \| F (x) < A\} \in (S ↾_{𝑡} D)$