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	|- ( ph -> S e. SAlg )
	smfdmss.f	|- ( ph -> F e. ( SMblFn ` S ) )
	smfdmss.d	|- D = dom F
Assertion	smfdmss	|- ( ph -> D C_ U. S )

Proof

Step	Hyp	Ref	Expression
1		smfdmss.s	|- ( ph -> S e. SAlg )
2		smfdmss.f	|- ( ph -> F e. ( SMblFn ` S ) )
3		smfdmss.d	|- D = dom F
4	1 3	issmf	|- ( ph -> ( F e. ( SMblFn ` S ) <-> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) ) )
5	2 4	mpbid	|- ( ph -> ( D C_ U. S /\ F : D --> RR /\ A. a e. RR { x e. D | ( F ` x ) < a } e. ( S |`t D ) ) )
6	5	simp1d	|- ( ph -> D C_ U. S )