issmfgtlem

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 left-open intervals unbounded above 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 (iii) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

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

Metamath Proof Explorer

Theorem issmfgtlem

Proof