smfpreimale

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of a closed interval unbounded below is in the subspace sigma-algebra induced by its domain. See Proposition 121B (ii) of Fremlin1 p. 35 (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

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

Metamath Proof Explorer

Theorem smfpreimale

Proof