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	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfdmss.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
	smfdmss.d	⊢ 𝐷 = dom 𝐹
Assertion	smfdmss	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		smfdmss.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		smfdmss.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
3		smfdmss.d	⊢ 𝐷 = dom 𝐹
4	1 3	issmf	⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
5	2 4	mpbid	⊢ ( 𝜑 → ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
6	5	simp1d	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )