Theorem issmfle

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 b 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	issmfle.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	issmfle.d	⊢ 𝐷 = dom 𝐹
Assertion	issmfle	⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≤ 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		issmfle.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		issmfle.d	⊢ 𝐷 = dom 𝐹
3	1	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝑆 ∈ SAlg )
4		simpr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
5	3 4 2	smfdmss	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐷 ⊆ ∪ 𝑆 )
6	3 4 2	smff	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐹 : 𝐷 ⟶ ℝ )
7		nfv	⊢ Ⅎ 𝑏 𝜑
8		nfv	⊢ Ⅎ 𝑏 𝐹 ∈ ( SMblFn ‘ 𝑆 )
9	7 8	nfan	⊢ Ⅎ 𝑏 ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
10		nfv	⊢ Ⅎ 𝑦 𝜑
11		nfv	⊢ Ⅎ 𝑦 𝐹 ∈ ( SMblFn ‘ 𝑆 )
12	10 11	nfan	⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
13		nfv	⊢ Ⅎ 𝑦 𝑏 ∈ ℝ
14	12 13	nfan	⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ )
15		nfv	⊢ Ⅎ 𝑐 ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ )
16	1	uniexd	⊢ ( 𝜑 → ∪ 𝑆 ∈ V )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ⊆ ∪ 𝑆 ) → ∪ 𝑆 ∈ V )
18		simpr	⊢ ( ( 𝜑 ∧ 𝐷 ⊆ ∪ 𝑆 ) → 𝐷 ⊆ ∪ 𝑆 )
19	17 18	ssexd	⊢ ( ( 𝜑 ∧ 𝐷 ⊆ ∪ 𝑆 ) → 𝐷 ∈ V )
20	5 19	syldan	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐷 ∈ V )
21		eqid	⊢ ( 𝑆 ↾t 𝐷 ) = ( 𝑆 ↾t 𝐷 )
22	3 20 21	subsalsal	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ( 𝑆 ↾t 𝐷 ) ∈ SAlg )
23	22	adantr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) → ( 𝑆 ↾t 𝐷 ) ∈ SAlg )
24	6	frexr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐹 : 𝐷 ⟶ ℝ* )
25	24	adantr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) → 𝐹 : 𝐷 ⟶ ℝ* )
26	25	ffvelcdmda	⊢ ( ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
27	3	adantr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℝ ) → 𝑆 ∈ SAlg )
28	4	adantr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℝ ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
29		simpr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℝ ) → 𝑐 ∈ ℝ )
30	27 28 2 29	smfpreimalt	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℝ ) → { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑐 } ∈ ( 𝑆 ↾t 𝐷 ) )
31	30	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) ∧ 𝑐 ∈ ℝ ) → { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑐 } ∈ ( 𝑆 ↾t 𝐷 ) )
32		simpr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) → 𝑏 ∈ ℝ )
33	14 15 23 26 31 32	salpreimaltle	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) → { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) )
34	33	ex	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ( 𝑏 ∈ ℝ → { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
35	9 34	ralrimi	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) )
36	5 6 35	3jca	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
37	36	ex	⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) → ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
38		nfv	⊢ Ⅎ 𝑦 𝐷 ⊆ ∪ 𝑆
39		nfv	⊢ Ⅎ 𝑦 𝐹 : 𝐷 ⟶ ℝ
40		nfcv	⊢ Ⅎ 𝑦 ℝ
41		nfrab1	⊢ Ⅎ 𝑦 { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 }
42		nfcv	⊢ Ⅎ 𝑦 ( 𝑆 ↾t 𝐷 )
43	41 42	nfel	⊢ Ⅎ 𝑦 { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 )
44	40 43	nfralw	⊢ Ⅎ 𝑦 ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 )
45	38 39 44	nf3an	⊢ Ⅎ 𝑦 ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) )
46	10 45	nfan	⊢ Ⅎ 𝑦 ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
47		nfv	⊢ Ⅎ 𝑏 𝐷 ⊆ ∪ 𝑆
48		nfv	⊢ Ⅎ 𝑏 𝐹 : 𝐷 ⟶ ℝ
49		nfra1	⊢ Ⅎ 𝑏 ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 )
50	47 48 49	nf3an	⊢ Ⅎ 𝑏 ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) )
51	7 50	nfan	⊢ Ⅎ 𝑏 ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
52	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) → 𝑆 ∈ SAlg )
53		simpr1	⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) → 𝐷 ⊆ ∪ 𝑆 )
54		simpr2	⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) → 𝐹 : 𝐷 ⟶ ℝ )
55		rspa	⊢ ( ( ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ∧ 𝑏 ∈ ℝ ) → { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) )
56	55	3ad2antl3	⊢ ( ( ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) ∧ 𝑏 ∈ ℝ ) → { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) )
57	56	adantll	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) ∧ 𝑏 ∈ ℝ ) → { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) )
58	46 51 52 2 53 54 57	issmflelem	⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
59	58	ex	⊢ ( 𝜑 → ( ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) )
60	37 59	impbid	⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
61		breq2	⊢ ( 𝑏 = 𝑎 → ( ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 ↔ ( 𝐹 ‘ 𝑦 ) ≤ 𝑎 ) )
62	61	rabbidv	⊢ ( 𝑏 = 𝑎 → { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } = { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑎 } )
63		fveq2	⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
64	63	breq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑦 ) ≤ 𝑎 ↔ ( 𝐹 ‘ 𝑥 ) ≤ 𝑎 ) )
65	64	cbvrabv	⊢ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑎 } = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≤ 𝑎 }
66	65	a1i	⊢ ( 𝑏 = 𝑎 → { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑎 } = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≤ 𝑎 } )
67	62 66	eqtrd	⊢ ( 𝑏 = 𝑎 → { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≤ 𝑎 } )
68	67	eleq1d	⊢ ( 𝑏 = 𝑎 → ( { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ↔ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≤ 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
69	68	cbvralvw	⊢ ( ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ↔ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≤ 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) )
70	69	3anbi3i	⊢ ( ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≤ 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
71	70	a1i	⊢ ( 𝜑 → ( ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≤ 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
72	60 71	bitrd	⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ≤ 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )