Metamath Proof Explorer

Theorem issmfdmpt

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	issmfdmpt.x	$⊢ Ⅎ x φ$
		issmfdmpt.a	$⊢ Ⅎ a φ$
		issmfdmpt.s	$⊢ φ \to S \in SAlg$
		issmfdmpt.i	$⊢ φ \to A \subseteq ⋃ S$
		issmfdmpt.b	$⊢ (φ \land x \in A) \to B \in ℝ$
		issmfdmpt.p	$⊢ (φ \land a \in ℝ) \to \{x \in A \| B < a\} \in (S ↾_{𝑡} A)$
	Assertion	issmfdmpt	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		issmfdmpt.x	$⊢ Ⅎ x φ$
2		issmfdmpt.a	$⊢ Ⅎ a φ$
3		issmfdmpt.s	$⊢ φ \to S \in SAlg$
4		issmfdmpt.i	$⊢ φ \to A \subseteq ⋃ S$
5		issmfdmpt.b	$⊢ (φ \land x \in A) \to B \in ℝ$
6		issmfdmpt.p	$⊢ (φ \land a \in ℝ) \to \{x \in A \| B < a\} \in (S ↾_{𝑡} A)$
7		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
8		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
9	1 5 8	fmptdf	$⊢ φ \to (x \in A ⟼ B) : A ⟶ ℝ$
10		eqidd	$⊢ φ \to (x \in A ⟼ B) = (x \in A ⟼ B)$
11	10 5	fvmpt2d	$⊢ (φ \land x \in A) \to (x \in A ⟼ B) (x) = B$
12	11	breq1d	$⊢ (φ \land x \in A) \to ((x \in A ⟼ B) (x) < a \leftrightarrow B < a)$
13	12	ex	$⊢ φ \to (x \in A \to ((x \in A ⟼ B) (x) < a \leftrightarrow B < a))$
14	1 13	ralrimi	$⊢ φ \to \forall x \in A ((x \in A ⟼ B) (x) < a \leftrightarrow B < a)$
15		rabbi	$⊢ \forall x \in A ((x \in A ⟼ B) (x) < a \leftrightarrow B < a) \leftrightarrow \{x \in A \| (x \in A ⟼ B) (x) < a\} = \{x \in A \| B < a\}$
16	14 15	sylib	$⊢ φ \to \{x \in A \| (x \in A ⟼ B) (x) < a\} = \{x \in A \| B < a\}$
17	16	adantr	$⊢ (φ \land a \in ℝ) \to \{x \in A \| (x \in A ⟼ B) (x) < a\} = \{x \in A \| B < a\}$
18	17 6	eqeltrd	$⊢ (φ \land a \in ℝ) \to \{x \in A \| (x \in A ⟼ B) (x) < a\} \in (S ↾_{𝑡} A)$
19	7 2 3 4 9 18	issmfdf	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$