issmfgtd

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

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

Proof

Step	Hyp	Ref	Expression
1		issmfgtd.a	$⊢ Ⅎ a φ$
2		issmfgtd.s	$⊢ φ \to S \in SAlg$
3		issmfgtd.d	$⊢ φ \to D \subseteq ⋃ S$
4		issmfgtd.f	$⊢ φ \to F : D ⟶ ℝ$
5		issmfgtd.p	$⊢ (φ \land a \in ℝ) \to \{x \in D \| a < F (x)\} \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 \| a < F (x)\} = \{x \in D \| a < F (x)\}$
10	9	adantr	$⊢ (φ \land a \in ℝ) \to \{x \in dom F \| a < F (x)\} = \{x \in D \| a < F (x)\}$
11	6	oveq2d	$⊢ φ \to S ↾_{𝑡} dom F = S ↾_{𝑡} D$
12	11	adantr	$⊢ (φ \land a \in ℝ) \to S ↾_{𝑡} dom F = S ↾_{𝑡} D$
13	10 12	eleq12d	$⊢ (φ \land a \in ℝ) \to (\{x \in dom F \| a < F (x)\} \in (S ↾_{𝑡} dom F) \leftrightarrow \{x \in D \| a < F (x)\} \in (S ↾_{𝑡} D))$
14	5 13	mpbird	$⊢ (φ \land a \in ℝ) \to \{x \in dom F \| a < F (x)\} \in (S ↾_{𝑡} dom F)$
15	14	ex	$⊢ φ \to (a \in ℝ \to \{x \in dom F \| a < F (x)\} \in (S ↾_{𝑡} dom F))$
16	1 15	ralrimi	$⊢ φ \to \forall a \in ℝ \{x \in dom F \| a < F (x)\} \in (S ↾_{𝑡} dom F)$
17	7 8 16	3jca	$⊢ φ \to (dom F \subseteq ⋃ S \land F : dom F ⟶ ℝ \land \forall a \in ℝ \{x \in dom F \| a < F (x)\} \in (S ↾_{𝑡} dom F))$
18		eqid	$⊢ dom F = dom F$
19	2 18	issmfgt	$⊢ φ \to (F \in SMblFn (S) \leftrightarrow (dom F \subseteq ⋃ S \land F : dom F ⟶ ℝ \land \forall a \in ℝ \{x \in dom F \| a < F (x)\} \in (S ↾_{𝑡} dom F)))$
20	17 19	mpbird	$⊢ φ \to F \in SMblFn (S)$

Metamath Proof Explorer

Theorem issmfgtd

Proof