Metamath Proof Explorer

Theorem issmfled

Description: A sufficient condition for " F being a real-valued measurable function w.r.t. to the sigma-algebra S ". (Contributed by Glauco Siliprandi, 26-Jun-2021)

		Ref	Expression
	Hypotheses	issmfled.a	$⊢ Ⅎ a φ$
		issmfled.s	$⊢ φ \to S \in SAlg$
		issmfled.d	$⊢ φ \to D \subseteq ⋃ S$
		issmfled.f	$⊢ φ \to F : D ⟶ ℝ$
		issmfled.6	$⊢ (φ \land a \in ℝ) \to \{x \in D \| F (x) \leq a\} \in (S ↾_{𝑡} D)$
	Assertion	issmfled	$⊢ φ \to F \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		issmfled.a	$⊢ Ⅎ a φ$
2		issmfled.s	$⊢ φ \to S \in SAlg$
3		issmfled.d	$⊢ φ \to D \subseteq ⋃ S$
4		issmfled.f	$⊢ φ \to F : D ⟶ ℝ$
5		issmfled.6	$⊢ (φ \land a \in ℝ) \to \{x \in D \| F (x) \leq a\} \in (S ↾_{𝑡} D)$
6	4	fdmd	$⊢ φ \to dom F = D$
7	6 3	eqsstrd	$⊢ φ \to dom F \subseteq ⋃ S$
8	4	ffdmd	$⊢ φ \to F : dom F ⟶ ℝ$
9	6	rabeqdv	$⊢ φ \to \{x \in dom F \| F (x) \leq a\} = \{x \in D \| F (x) \leq a\}$
10	6	oveq2d	$⊢ φ \to S ↾_{𝑡} dom F = S ↾_{𝑡} D$
11	9 10	eleq12d	$⊢ φ \to (\{x \in dom F \| F (x) \leq a\} \in (S ↾_{𝑡} dom F) \leftrightarrow \{x \in D \| F (x) \leq a\} \in (S ↾_{𝑡} D))$
12	11	adantr	$⊢ (φ \land a \in ℝ) \to (\{x \in dom F \| F (x) \leq a\} \in (S ↾_{𝑡} dom F) \leftrightarrow \{x \in D \| F (x) \leq a\} \in (S ↾_{𝑡} D))$
13	5 12	mpbird	$⊢ (φ \land a \in ℝ) \to \{x \in dom F \| F (x) \leq a\} \in (S ↾_{𝑡} dom F)$
14	13	ex	$⊢ φ \to (a \in ℝ \to \{x \in dom F \| F (x) \leq a\} \in (S ↾_{𝑡} dom F))$
15	1 14	ralrimi	$⊢ φ \to \forall a \in ℝ \{x \in dom F \| F (x) \leq a\} \in (S ↾_{𝑡} dom F)$
16	7 8 15	3jca	$⊢ φ \to (dom F \subseteq ⋃ S \land F : dom F ⟶ ℝ \land \forall a \in ℝ \{x \in dom F \| F (x) \leq a\} \in (S ↾_{𝑡} dom F))$
17		eqid	$⊢ dom F = dom F$
18	2 17	issmfle	$⊢ φ \to (F \in SMblFn (S) \leftrightarrow (dom F \subseteq ⋃ S \land F : dom F ⟶ ℝ \land \forall a \in ℝ \{x \in dom F \| F (x) \leq a\} \in (S ↾_{𝑡} dom F)))$
19	16 18	mpbird	$⊢ φ \to F \in SMblFn (S)$