Metamath Proof Explorer


Theorem issmfgelem

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 left-closed intervals unbounded above 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 (iv) of Fremlin1 p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses issmfgelem.x x φ
issmfgelem.a a φ
issmfgelem.s φ S SAlg
issmfgelem.d D = dom F
issmfgelem.i φ D S
issmfgelem.f φ F : D
issmfgelem.p φ a x D | a F x S 𝑡 D
Assertion issmfgelem φ F SMblFn S

Proof

Step Hyp Ref Expression
1 issmfgelem.x x φ
2 issmfgelem.a a φ
3 issmfgelem.s φ S SAlg
4 issmfgelem.d D = dom F
5 issmfgelem.i φ D S
6 issmfgelem.f φ F : D
7 issmfgelem.p φ a x D | a F x S 𝑡 D
8 3 5 restuni4 φ S 𝑡 D = D
9 8 eqcomd φ D = S 𝑡 D
10 9 rabeqdv φ x D | F x < b = x S 𝑡 D | F x < b
11 10 adantr φ b x D | F x < b = x S 𝑡 D | F x < b
12 nfv x b
13 1 12 nfan x φ b
14 nfv a b
15 2 14 nfan a φ b
16 3 uniexd φ S V
17 16 adantr φ D S S V
18 simpr φ D S D S
19 17 18 ssexd φ D S D V
20 5 19 mpdan φ D V
21 eqid S 𝑡 D = S 𝑡 D
22 3 20 21 subsalsal φ S 𝑡 D SAlg
23 22 adantr φ b S 𝑡 D SAlg
24 eqid S 𝑡 D = S 𝑡 D
25 6 adantr φ x S 𝑡 D F : D
26 simpr φ x S 𝑡 D x S 𝑡 D
27 8 adantr φ x S 𝑡 D S 𝑡 D = D
28 26 27 eleqtrd φ x S 𝑡 D x D
29 25 28 ffvelrnd φ x S 𝑡 D F x
30 29 rexrd φ x S 𝑡 D F x *
31 30 adantlr φ b x S 𝑡 D F x *
32 9 rabeqdv φ x D | a F x = x S 𝑡 D | a F x
33 32 eleq1d φ x D | a F x S 𝑡 D x S 𝑡 D | a F x S 𝑡 D
34 2 33 ralbid φ a x D | a F x S 𝑡 D a x S 𝑡 D | a F x S 𝑡 D
35 7 34 mpbid φ a x S 𝑡 D | a F x S 𝑡 D
36 35 adantr φ a a x S 𝑡 D | a F x S 𝑡 D
37 simpr φ a a
38 rspa a x S 𝑡 D | a F x S 𝑡 D a x S 𝑡 D | a F x S 𝑡 D
39 36 37 38 syl2anc φ a x S 𝑡 D | a F x S 𝑡 D
40 39 adantlr φ b a x S 𝑡 D | a F x S 𝑡 D
41 simpr φ b b
42 13 15 23 24 31 40 41 salpreimagelt φ b x S 𝑡 D | F x < b S 𝑡 D
43 11 42 eqeltrd φ b x D | F x < b S 𝑡 D
44 43 ralrimiva φ b x D | F x < b S 𝑡 D
45 5 6 44 3jca φ D S F : D b x D | F x < b S 𝑡 D
46 3 4 issmf φ F SMblFn S D S F : D b x D | F x < b S 𝑡 D
47 45 46 mpbird φ F SMblFn S