Theorem issmff

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

	Ref	Expression
Hypotheses	issmff.x	⊢ Ⅎ 𝑥 𝐹
	issmff.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	issmff.d	⊢ 𝐷 = dom 𝐹
Assertion	issmff	⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		issmff.x	⊢ Ⅎ 𝑥 𝐹
2		issmff.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		issmff.d	⊢ 𝐷 = dom 𝐹
4	2 3	issmf	⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
5		nfcv	⊢ Ⅎ 𝑦 𝐷
6	1	nfdm	⊢ Ⅎ 𝑥 dom 𝐹
7	3 6	nfcxfr	⊢ Ⅎ 𝑥 𝐷
8		nfcv	⊢ Ⅎ 𝑥 𝑦
9	1 8	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
10		nfcv	⊢ Ⅎ 𝑥 <
11		nfcv	⊢ Ⅎ 𝑥 𝑎
12	9 10 11	nfbr	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 ) < 𝑎
13		nfv	⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑥 ) < 𝑎
14		fveq2	⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
15	14	breq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑦 ) < 𝑎 ↔ ( 𝐹 ‘ 𝑥 ) < 𝑎 ) )
16	5 7 12 13 15	cbvrabw	⊢ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑎 } = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 }
17	16	eleq1i	⊢ ( { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ↔ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) )
18	17	ralbii	⊢ ( ∀ 𝑎 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ↔ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) )
19	18	3anbi3i	⊢ ( ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
20	19	a1i	⊢ ( 𝜑 → ( ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
21	4 20	bitrd	⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )