Definition df-smblfn

Description: Define a real-valued measurable function w.r.t. a given sigma-algebra. See Definition 121C of Fremlin1 p. 36 and Definition 135E (b) of Fremlin1 p. 80 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Assertion	df-smblfn	⊢ SMblFn = ( 𝑠 ∈ SAlg ↦ { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑠 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑠 ↾t dom 𝑓 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csmblfn	⊢ SMblFn
1		vs	⊢ 𝑠
2		csalg	⊢ SAlg
3		vf	⊢ 𝑓
4		cr	⊢ ℝ
5		cpm	⊢ ↑pm
6	1	cv	⊢ 𝑠
7	6	cuni	⊢ ∪ 𝑠
8	4 7 5	co	⊢ ( ℝ ↑pm ∪ 𝑠 )
9		va	⊢ 𝑎
10	3	cv	⊢ 𝑓
11	10	ccnv	⊢ ◡ 𝑓
12		cmnf	⊢ -∞
13		cioo	⊢ (,)
14	9	cv	⊢ 𝑎
15	12 14 13	co	⊢ ( -∞ (,) 𝑎 )
16	11 15	cima	⊢ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) )
17		crest	⊢ ↾t
18	10	cdm	⊢ dom 𝑓
19	6 18 17	co	⊢ ( 𝑠 ↾t dom 𝑓 )
20	16 19	wcel	⊢ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑠 ↾t dom 𝑓 )
21	20 9 4	wral	⊢ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑠 ↾t dom 𝑓 )
22	21 3 8	crab	⊢ { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑠 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑠 ↾t dom 𝑓 ) }
23	1 2 22	cmpt	⊢ ( 𝑠 ∈ SAlg ↦ { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑠 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑠 ↾t dom 𝑓 ) } )
24	0 23	wceq	⊢ SMblFn = ( 𝑠 ∈ SAlg ↦ { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑠 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑠 ↾t dom 𝑓 ) } )