Theorem issmfgelem

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-closed 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 (iv) of Fremlin1 p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	issmfgelem.x	⊢ Ⅎ 𝑥 𝜑
	issmfgelem.a	⊢ Ⅎ 𝑎 𝜑
	issmfgelem.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	issmfgelem.d	⊢ 𝐷 = dom 𝐹
	issmfgelem.i	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
	issmfgelem.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
	issmfgelem.p	⊢ ( 𝜑 → ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ 𝑎 ≤ ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
Assertion	issmfgelem	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		issmfgelem.x	⊢ Ⅎ 𝑥 𝜑
2		issmfgelem.a	⊢ Ⅎ 𝑎 𝜑
3		issmfgelem.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		issmfgelem.d	⊢ 𝐷 = dom 𝐹
5		issmfgelem.i	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
6		issmfgelem.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
7		issmfgelem.p	⊢ ( 𝜑 → ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ 𝑎 ≤ ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
8	3 5	restuni4	⊢ ( 𝜑 → ∪ ( 𝑆 ↾t 𝐷 ) = 𝐷 )
9	8	eqcomd	⊢ ( 𝜑 → 𝐷 = ∪ ( 𝑆 ↾t 𝐷 ) )
10	9	rabeqdv	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑏 } = { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑏 } )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑏 } = { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑏 } )
12		nfv	⊢ Ⅎ 𝑥 𝑏 ∈ ℝ
13	1 12	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑏 ∈ ℝ )
14		nfv	⊢ Ⅎ 𝑎 𝑏 ∈ ℝ
15	2 14	nfan	⊢ Ⅎ 𝑎 ( 𝜑 ∧ 𝑏 ∈ ℝ )
16	3	uniexd	⊢ ( 𝜑 → ∪ 𝑆 ∈ V )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ⊆ ∪ 𝑆 ) → ∪ 𝑆 ∈ V )
18		simpr	⊢ ( ( 𝜑 ∧ 𝐷 ⊆ ∪ 𝑆 ) → 𝐷 ⊆ ∪ 𝑆 )
19	17 18	ssexd	⊢ ( ( 𝜑 ∧ 𝐷 ⊆ ∪ 𝑆 ) → 𝐷 ∈ V )
20	5 19	mpdan	⊢ ( 𝜑 → 𝐷 ∈ V )
21		eqid	⊢ ( 𝑆 ↾t 𝐷 ) = ( 𝑆 ↾t 𝐷 )
22	3 20 21	subsalsal	⊢ ( 𝜑 → ( 𝑆 ↾t 𝐷 ) ∈ SAlg )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → ( 𝑆 ↾t 𝐷 ) ∈ SAlg )
24		eqid	⊢ ∪ ( 𝑆 ↾t 𝐷 ) = ∪ ( 𝑆 ↾t 𝐷 )
25	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → 𝐹 : 𝐷 ⟶ ℝ )
26		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) )
27	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → ∪ ( 𝑆 ↾t 𝐷 ) = 𝐷 )
28	26 27	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → 𝑥 ∈ 𝐷 )
29	25 28	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
30	29	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
31	30	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
32	9	rabeqdv	⊢ ( 𝜑 → { 𝑥 ∈ 𝐷 ∣ 𝑎 ≤ ( 𝐹 ‘ 𝑥 ) } = { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹 ‘ 𝑥 ) } )
33	32	eleq1d	⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐷 ∣ 𝑎 ≤ ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) ↔ { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) )
34	2 33	ralbid	⊢ ( 𝜑 → ( ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ 𝑎 ≤ ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) ↔ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) )
35	7 34	mpbid	⊢ ( 𝜑 → ∀ 𝑎 ∈ ℝ { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ∀ 𝑎 ∈ ℝ { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
37		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ )
38		rspa	⊢ ( ( ∀ 𝑎 ∈ ℝ { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
39	36 37 38	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
40	39	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ 𝑎 ≤ ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
41		simpr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → 𝑏 ∈ ℝ )
42	13 15 23 24 31 40 41	salpreimagelt	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → { 𝑥 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) )
43	11 42	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) )
44	43	ralrimiva	⊢ ( 𝜑 → ∀ 𝑏 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) )
45	5 6 44	3jca	⊢ ( 𝜑 → ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
46	3 4	issmf	⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
47	45 46	mpbird	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )