issmfdf

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	issmfdf.x	$⊢ \underline{Ⅎ} x F$
	issmfdf.a	$⊢ Ⅎ a φ$
	issmfdf.s	$⊢ φ \to S \in SAlg$
	issmfdf.d	$⊢ φ \to D \subseteq ⋃ S$
	issmfdf.f	$⊢ φ \to F : D ⟶ ℝ$
	issmfdf.p	$⊢ (φ \land a \in ℝ) \to \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D)$
Assertion	issmfdf	$⊢ φ \to F \in SMblFn (S)$

Proof

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

Metamath Proof Explorer

Theorem issmfdf

Proof