Metamath Proof Explorer

Theorem smfpreimage

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of a closed interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021)

		Ref	Expression
	Hypotheses	smfpreimage.s	$⊢ φ \to S \in SAlg$
		smfpreimage.f	$⊢ φ \to F \in SMblFn (S)$
		smfpreimage.d	$⊢ D = dom F$
		smfpreimage.a	$⊢ φ \to A \in ℝ$
	Assertion	smfpreimage	$⊢ φ \to \{x \in D \| A \leq F (x)\} \in (S ↾_{𝑡} D)$

Proof

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