Metamath Proof Explorer


Theorem issmfgtlem

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

Ref Expression
Hypotheses issmfgtlem.x xφ
issmfgtlem.a aφ
issmfgtlem.s φSSAlg
issmfgtlem.d D=domF
issmfgtlem.i φDS
issmfgtlem.f φF:D
issmfgtlem.p φaxD|a<FxS𝑡D
Assertion issmfgtlem φFSMblFnS

Proof

Step Hyp Ref Expression
1 issmfgtlem.x xφ
2 issmfgtlem.a aφ
3 issmfgtlem.s φSSAlg
4 issmfgtlem.d D=domF
5 issmfgtlem.i φDS
6 issmfgtlem.f φF:D
7 issmfgtlem.p φaxD|a<FxS𝑡D
8 3 5 restuni4 φS𝑡D=D
9 8 eqcomd φD=S𝑡D
10 9 rabeqdv φxD|Fx<b=xS𝑡D|Fx<b
11 10 adantr φbxD|Fx<b=xS𝑡D|Fx<b
12 nfv xb
13 1 12 nfan xφb
14 nfv ab
15 2 14 nfan aφb
16 3 uniexd φSV
17 16 adantr φDSSV
18 simpr φDSDS
19 17 18 ssexd φDSDV
20 5 19 mpdan φDV
21 eqid S𝑡D=S𝑡D
22 3 20 21 subsalsal φS𝑡DSAlg
23 22 adantr φbS𝑡DSAlg
24 eqid S𝑡D=S𝑡D
25 6 adantr φxS𝑡DF:D
26 simpr φxS𝑡DxS𝑡D
27 8 adantr φxS𝑡DS𝑡D=D
28 26 27 eleqtrd φxS𝑡DxD
29 25 28 ffvelrnd φxS𝑡DFx
30 29 rexrd φxS𝑡DFx*
31 30 adantlr φbxS𝑡DFx*
32 8 rabeqdv φxS𝑡D|a<Fx=xD|a<Fx
33 32 adantr φaxS𝑡D|a<Fx=xD|a<Fx
34 7 r19.21bi φaxD|a<FxS𝑡D
35 33 34 eqeltrd φaxS𝑡D|a<FxS𝑡D
36 35 adantlr φbaxS𝑡D|a<FxS𝑡D
37 simpr φbb
38 13 15 23 24 31 36 37 salpreimagtlt φbxS𝑡D|Fx<bS𝑡D
39 11 38 eqeltrd φbxD|Fx<bS𝑡D
40 39 ralrimiva φbxD|Fx<bS𝑡D
41 5 6 40 3jca φDSF:DbxD|Fx<bS𝑡D
42 3 4 issmf φFSMblFnSDSF:DbxD|Fx<bS𝑡D
43 41 42 mpbird φFSMblFnS