Metamath Proof Explorer

Theorem smfpreimagt

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

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

Proof

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