Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-smblfn Structured version   Visualization version   GIF version

Definition df-smblfn 40673
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.)
Assertion
Ref Expression
df-smblfn SMblFn = (𝑠 ∈ SAlg ↦ {𝑓 ∈ (ℝ ↑pm 𝑠) ∣ ∀𝑎 ∈ ℝ (𝑓 “ (-∞(,)𝑎)) ∈ (𝑠t dom 𝑓)})
Distinct variable group:   𝑓,𝑠,𝑎

Detailed syntax breakdown of Definition df-smblfn
StepHypRef Expression
1 csmblfn 40672 . 2 class SMblFn
2 vs . . 3 setvar 𝑠
3 csalg 40291 . . 3 class SAlg
4 vf . . . . . . . . 9 setvar 𝑓
54cv 1480 . . . . . . . 8 class 𝑓
65ccnv 5103 . . . . . . 7 class 𝑓
7 cmnf 10057 . . . . . . . 8 class -∞
8 va . . . . . . . . 9 setvar 𝑎
98cv 1480 . . . . . . . 8 class 𝑎
10 cioo 12160 . . . . . . . 8 class (,)
117, 9, 10co 6635 . . . . . . 7 class (-∞(,)𝑎)
126, 11cima 5107 . . . . . 6 class (𝑓 “ (-∞(,)𝑎))
132cv 1480 . . . . . . 7 class 𝑠
145cdm 5104 . . . . . . 7 class dom 𝑓
15 crest 16062 . . . . . . 7 class t
1613, 14, 15co 6635 . . . . . 6 class (𝑠t dom 𝑓)
1712, 16wcel 1988 . . . . 5 wff (𝑓 “ (-∞(,)𝑎)) ∈ (𝑠t dom 𝑓)
18 cr 9920 . . . . 5 class
1917, 8, 18wral 2909 . . . 4 wff 𝑎 ∈ ℝ (𝑓 “ (-∞(,)𝑎)) ∈ (𝑠t dom 𝑓)
2013cuni 4427 . . . . 5 class 𝑠
21 cpm 7843 . . . . 5 class pm
2218, 20, 21co 6635 . . . 4 class (ℝ ↑pm 𝑠)
2319, 4, 22crab 2913 . . 3 class {𝑓 ∈ (ℝ ↑pm 𝑠) ∣ ∀𝑎 ∈ ℝ (𝑓 “ (-∞(,)𝑎)) ∈ (𝑠t dom 𝑓)}
242, 3, 23cmpt 4720 . 2 class (𝑠 ∈ SAlg ↦ {𝑓 ∈ (ℝ ↑pm 𝑠) ∣ ∀𝑎 ∈ ℝ (𝑓 “ (-∞(,)𝑎)) ∈ (𝑠t dom 𝑓)})
251, 24wceq 1481 1 wff SMblFn = (𝑠 ∈ SAlg ↦ {𝑓 ∈ (ℝ ↑pm 𝑠) ∣ ∀𝑎 ∈ ℝ (𝑓 “ (-∞(,)𝑎)) ∈ (𝑠t dom 𝑓)})
Colors of variables: wff setvar class
This definition is referenced by:  issmflem  40699
  Copyright terms: Public domain W3C validator