Metamath Proof Explorer

Theorem smfsssmf

Description: If a function is measurable w.r.t. to a sigma-algebra, then it is measurable w.r.t. to a larger sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021)

		Ref	Expression
	Hypotheses	smfsssmf.r	$⊢ φ \to R \in SAlg$
		smfsssmf.s	$⊢ φ \to S \in SAlg$
		smfsssmf.i	$⊢ φ \to R \subseteq S$
		smfsssmf.f	$⊢ φ \to F \in SMblFn (R)$
	Assertion	smfsssmf	$⊢ φ \to F \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		smfsssmf.r	$⊢ φ \to R \in SAlg$
2		smfsssmf.s	$⊢ φ \to S \in SAlg$
3		smfsssmf.i	$⊢ φ \to R \subseteq S$
4		smfsssmf.f	$⊢ φ \to F \in SMblFn (R)$
5		nfv	$⊢ Ⅎ a φ$
6		eqid	$⊢ dom F = dom F$
7	1 4 6	smfdmss	$⊢ φ \to dom F \subseteq ⋃ R$
8	3	unissd	$⊢ φ \to ⋃ R \subseteq ⋃ S$
9	7 8	sstrd	$⊢ φ \to dom F \subseteq ⋃ S$
10	1 4 6	smff	$⊢ φ \to F : dom F ⟶ ℝ$
11		ssrest	$⊢ (S \in SAlg \land R \subseteq S) \to R ↾_{𝑡} dom F \subseteq S ↾_{𝑡} dom F$
12	2 3 11	syl2anc	$⊢ φ \to R ↾_{𝑡} dom F \subseteq S ↾_{𝑡} dom F$
13	12	adantr	$⊢ (φ \land a \in ℝ) \to R ↾_{𝑡} dom F \subseteq S ↾_{𝑡} dom F$
14	1	adantr	$⊢ (φ \land a \in ℝ) \to R \in SAlg$
15	4	adantr	$⊢ (φ \land a \in ℝ) \to F \in SMblFn (R)$
16		simpr	$⊢ (φ \land a \in ℝ) \to a \in ℝ$
17	14 15 6 16	smfpreimalt	$⊢ (φ \land a \in ℝ) \to \{x \in dom F \| F (x) < a\} \in (R ↾_{𝑡} dom F)$
18	13 17	sseldd	$⊢ (φ \land a \in ℝ) \to \{x \in dom F \| F (x) < a\} \in (S ↾_{𝑡} dom F)$
19	5 2 9 10 18	issmfd	$⊢ φ \to F \in SMblFn (S)$