Metamath Proof Explorer


Theorem issmfd

Description: A sufficient condition for " F being a real-valued measurable function w.r.t. to the sigma-algebra S ". (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses issmfd.a aφ
issmfd.s φSSAlg
issmfd.d φDS
issmfd.f φF:D
issmfd.p φaxD|Fx<aS𝑡D
Assertion issmfd φFSMblFnS

Proof

Step Hyp Ref Expression
1 issmfd.a aφ
2 issmfd.s φSSAlg
3 issmfd.d φDS
4 issmfd.f φF:D
5 issmfd.p φaxD|Fx<aS𝑡D
6 4 fdmd φdomF=D
7 6 3 eqsstrd φdomFS
8 4 ffdmd φF:domF
9 6 rabeqdv φxdomF|Fx<a=xD|Fx<a
10 6 oveq2d φS𝑡domF=S𝑡D
11 9 10 eleq12d φxdomF|Fx<aS𝑡domFxD|Fx<aS𝑡D
12 11 adantr φaxdomF|Fx<aS𝑡domFxD|Fx<aS𝑡D
13 5 12 mpbird φaxdomF|Fx<aS𝑡domF
14 13 ex φaxdomF|Fx<aS𝑡domF
15 1 14 ralrimi φaxdomF|Fx<aS𝑡domF
16 7 8 15 3jca φdomFSF:domFaxdomF|Fx<aS𝑡domF
17 eqid domF=domF
18 2 17 issmf φFSMblFnSdomFSF:domFaxdomF|Fx<aS𝑡domF
19 16 18 mpbird φFSMblFnS