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 φSSAlg
issmfgelem.d D=domF
issmfgelem.i φDS
issmfgelem.f φF:D
issmfgelem.p φaxD|aFxS𝑡D
Assertion issmfgelem φFSMblFnS

Proof

Step Hyp Ref Expression
1 issmfgelem.x xφ
2 issmfgelem.a aφ
3 issmfgelem.s φSSAlg
4 issmfgelem.d D=domF
5 issmfgelem.i φDS
6 issmfgelem.f φF:D
7 issmfgelem.p φaxD|aFxS𝑡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 9 rabeqdv φxD|aFx=xS𝑡D|aFx
33 32 eleq1d φxD|aFxS𝑡DxS𝑡D|aFxS𝑡D
34 2 33 ralbid φaxD|aFxS𝑡DaxS𝑡D|aFxS𝑡D
35 7 34 mpbid φaxS𝑡D|aFxS𝑡D
36 35 adantr φaaxS𝑡D|aFxS𝑡D
37 simpr φaa
38 rspa axS𝑡D|aFxS𝑡DaxS𝑡D|aFxS𝑡D
39 36 37 38 syl2anc φaxS𝑡D|aFxS𝑡D
40 39 adantlr φbaxS𝑡D|aFxS𝑡D
41 simpr φbb
42 13 15 23 24 31 40 41 salpreimagelt φbxS𝑡D|Fx<bS𝑡D
43 11 42 eqeltrd φbxD|Fx<bS𝑡D
44 43 ralrimiva φbxD|Fx<bS𝑡D
45 5 6 44 3jca φDSF:DbxD|Fx<bS𝑡D
46 3 4 issmf φFSMblFnSDSF:DbxD|Fx<bS𝑡D
47 45 46 mpbird φFSMblFnS