Metamath Proof Explorer


Theorem smfdmss

Description: The domain of a function measurable w.r.t. to a sigma-algebra, is a subset of the set underlying the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfdmss.s φSSAlg
smfdmss.f φFSMblFnS
smfdmss.d D=domF
Assertion smfdmss φDS

Proof

Step Hyp Ref Expression
1 smfdmss.s φSSAlg
2 smfdmss.f φFSMblFnS
3 smfdmss.d D=domF
4 1 3 issmf φFSMblFnSDSF:DaxD|Fx<aS𝑡D
5 2 4 mpbid φDSF:DaxD|Fx<aS𝑡D
6 5 simp1d φDS