df-smblfn

Description: Define a real-valued measurable function w.r.t. a given sigma-algebra. See Definition 121C of Fremlin1 p. 36 and Definition 135E (b) of Fremlin1 p. 80 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

		Ref	Expression
	Assertion	df-smblfn	$⊢ SMblFn = (s \in SAlg ⟼ \{f \in (ℝ ↑_{𝑝𝑚} ⋃ s) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (s ↾_{𝑡} dom f)\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csmblfn	$class SMblFn$
1		vs	$setvar s$
2		csalg	$class SAlg$
3		vf	$setvar f$
4		cr	$class ℝ$
5		cpm	$class ↑_{𝑝𝑚}$
6	1	cv	$setvar s$
7	6	cuni	$class ⋃ s$
8	4 7 5	co	$class (ℝ ↑_{𝑝𝑚} ⋃ s)$
9		va	$setvar a$
10	3	cv	$setvar f$
11	10	ccnv	$class f^{-1}$
12		cmnf	$class −∞$
13		cioo	$class (.)$
14	9	cv	$setvar a$
15	12 14 13	co	$class (−∞, a)$
16	11 15	cima	$class f^{-1} [(−∞, a)]$
17		crest	$class ↾_{𝑡}$
18	10	cdm	$class dom f$
19	6 18 17	co	$class (s ↾_{𝑡} dom f)$
20	16 19	wcel	$wff f^{-1} [(−∞, a)] \in (s ↾_{𝑡} dom f)$
21	20 9 4	wral	$wff \forall a \in ℝ f^{-1} [(−∞, a)] \in (s ↾_{𝑡} dom f)$
22	21 3 8	crab	$class \{f \in (ℝ ↑_{𝑝𝑚} ⋃ s) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (s ↾_{𝑡} dom f)\}$
23	1 2 22	cmpt	$class (s \in SAlg ⟼ \{f \in (ℝ ↑_{𝑝𝑚} ⋃ s) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (s ↾_{𝑡} dom f)\})$
24	0 23	wceq	$wff SMblFn = (s \in SAlg ⟼ \{f \in (ℝ ↑_{𝑝𝑚} ⋃ s) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (s ↾_{𝑡} dom f)\})$

Metamath Proof Explorer

Definition df-smblfn

Detailed syntax breakdown