Metamath Proof Explorer


Theorem issmfled

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 issmfled.a aφ
issmfled.s φSSAlg
issmfled.d φDS
issmfled.f φF:D
issmfled.6 φaxD|FxaS𝑡D
Assertion issmfled φFSMblFnS

Proof

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