issmflelem

Description: The predicate " F is a real-valued measurable function w.r.t. to the sigma-algebra S ". A function is measurable iff the preimages of all right-closed intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of F is required to be a subset of the underlying set of S . Definition 121C of Fremlin1 p. 36, and Proposition 121B (ii) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		issmflelem.x	$⊢ Ⅎ x φ$
2		issmflelem.a	$⊢ Ⅎ a φ$
3		issmflelem.s	$⊢ φ \to S \in SAlg$
4		issmflelem.d	$⊢ D = dom F$
5		issmflelem.i	$⊢ φ \to D \subseteq ⋃ S$
6		issmflelem.f	$⊢ φ \to F : D ⟶ ℝ$
7		issmflelem.l	$⊢ (φ \land a \in ℝ) \to \{x \in D \| F (x) \leq a\} \in (S ↾_{𝑡} D)$
8	3	adantr	$⊢ (φ \land D \subseteq ⋃ S) \to S \in SAlg$
9		simpr	$⊢ (φ \land D \subseteq ⋃ S) \to D \subseteq ⋃ S$
10	8 9	restuni4	$⊢ (φ \land D \subseteq ⋃ S) \to ⋃ (S ↾_{𝑡} D) = D$
11	10	eqcomd	$⊢ (φ \land D \subseteq ⋃ S) \to D = ⋃ (S ↾_{𝑡} D)$
12	5 11	mpdan	$⊢ φ \to D = ⋃ (S ↾_{𝑡} D)$
13	12	rabeqdv	$⊢ φ \to \{x \in D \| F (x) < b\} = \{x \in ⋃ (S ↾_{𝑡} D) \| F (x) < b\}$
14	13	adantr	$⊢ (φ \land b \in ℝ) \to \{x \in D \| F (x) < b\} = \{x \in ⋃ (S ↾_{𝑡} D) \| F (x) < b\}$
15		nfv	$⊢ Ⅎ x b \in ℝ$
16	1 15	nfan	$⊢ Ⅎ x (φ \land b \in ℝ)$
17		nfv	$⊢ Ⅎ a b \in ℝ$
18	2 17	nfan	$⊢ Ⅎ a (φ \land b \in ℝ)$
19	3	uniexd	$⊢ φ \to ⋃ S \in V$
20	19	adantr	$⊢ (φ \land D \subseteq ⋃ S) \to ⋃ S \in V$
21	20 9	ssexd	$⊢ (φ \land D \subseteq ⋃ S) \to D \in V$
22		eqid	$⊢ S ↾_{𝑡} D = S ↾_{𝑡} D$
23	8 21 22	subsalsal	$⊢ (φ \land D \subseteq ⋃ S) \to S ↾_{𝑡} D \in SAlg$
24	5 23	mpdan	$⊢ φ \to S ↾_{𝑡} D \in SAlg$
25	24	adantr	$⊢ (φ \land b \in ℝ) \to S ↾_{𝑡} D \in SAlg$
26		eqid	$⊢ ⋃ (S ↾_{𝑡} D) = ⋃ (S ↾_{𝑡} D)$
27		simpr	$⊢ (φ \land x \in ⋃ (S ↾_{𝑡} D)) \to x \in ⋃ (S ↾_{𝑡} D)$
28	5 10	mpdan	$⊢ φ \to ⋃ (S ↾_{𝑡} D) = D$
29	28	adantr	$⊢ (φ \land x \in ⋃ (S ↾_{𝑡} D)) \to ⋃ (S ↾_{𝑡} D) = D$
30	27 29	eleqtrd	$⊢ (φ \land x \in ⋃ (S ↾_{𝑡} D)) \to x \in D$
31	6	ffvelcdmda	$⊢ (φ \land x \in D) \to F (x) \in ℝ$
32	30 31	syldan	$⊢ (φ \land x \in ⋃ (S ↾_{𝑡} D)) \to F (x) \in ℝ$
33	32	rexrd	$⊢ (φ \land x \in ⋃ (S ↾_{𝑡} D)) \to F (x) \in ℝ^{*}$
34	33	adantlr	$⊢ ((φ \land b \in ℝ) \land x \in ⋃ (S ↾_{𝑡} D)) \to F (x) \in ℝ^{*}$
35	28	rabeqdv	$⊢ φ \to \{x \in ⋃ (S ↾_{𝑡} D) \| F (x) \leq a\} = \{x \in D \| F (x) \leq a\}$
36	35	adantr	$⊢ (φ \land a \in ℝ) \to \{x \in ⋃ (S ↾_{𝑡} D) \| F (x) \leq a\} = \{x \in D \| F (x) \leq a\}$
37	36 7	eqeltrd	$⊢ (φ \land a \in ℝ) \to \{x \in ⋃ (S ↾_{𝑡} D) \| F (x) \leq a\} \in (S ↾_{𝑡} D)$
38	37	adantlr	$⊢ ((φ \land b \in ℝ) \land a \in ℝ) \to \{x \in ⋃ (S ↾_{𝑡} D) \| F (x) \leq a\} \in (S ↾_{𝑡} D)$
39		simpr	$⊢ (φ \land b \in ℝ) \to b \in ℝ$
40	16 18 25 26 34 38 39	salpreimalelt	$⊢ (φ \land b \in ℝ) \to \{x \in ⋃ (S ↾_{𝑡} D) \| F (x) < b\} \in (S ↾_{𝑡} D)$
41	14 40	eqeltrd	$⊢ (φ \land b \in ℝ) \to \{x \in D \| F (x) < b\} \in (S ↾_{𝑡} D)$
42	41	ralrimiva	$⊢ φ \to \forall b \in ℝ \{x \in D \| F (x) < b\} \in (S ↾_{𝑡} D)$
43	5 6 42	3jca	$⊢ φ \to (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{x \in D \| F (x) < b\} \in (S ↾_{𝑡} D))$
44	3 4	issmf	$⊢ φ \to (F \in SMblFn (S) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{x \in D \| F (x) < b\} \in (S ↾_{𝑡} D)))$
45	43 44	mpbird	$⊢ φ \to F \in SMblFn (S)$

Metamath Proof Explorer

Theorem issmflelem

Proof