Theorem issmf

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

Proof

Step	Hyp	Ref	Expression
1		issmf.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		issmf.d	⊢ 𝐷 = dom 𝐹
3	1 2	issmflem	⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
4		breq2	⊢ ( 𝑏 = 𝑎 → ( ( 𝐹 ‘ 𝑦 ) < 𝑏 ↔ ( 𝐹 ‘ 𝑦 ) < 𝑎 ) )
5	4	rabbidv	⊢ ( 𝑏 = 𝑎 → { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑏 } = { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑎 } )
6	5	eleq1d	⊢ ( 𝑏 = 𝑎 → ( { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ↔ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
7		fveq2	⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
8	7	breq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑦 ) < 𝑎 ↔ ( 𝐹 ‘ 𝑥 ) < 𝑎 ) )
9	8	cbvrabv	⊢ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑎 } = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 }
10	9	eleq1i	⊢ ( { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ↔ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) )
11	10	a1i	⊢ ( 𝑏 = 𝑎 → ( { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ↔ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
12	6 11	bitrd	⊢ ( 𝑏 = 𝑎 → ( { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ↔ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
13	12	cbvralvw	⊢ ( ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ↔ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) )
14	13	3anbi3i	⊢ ( ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
15	14	a1i	⊢ ( 𝜑 → ( ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) < 𝑏 } ∈ ( 𝑆 ↾t 𝐷 ) ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
16	3 15	bitrd	⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )