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	⊢ ( 𝜑 → 𝑅 ∈ SAlg )
	smfsssmf.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfsssmf.i	⊢ ( 𝜑 → 𝑅 ⊆ 𝑆 )
	smfsssmf.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑅 ) )
Assertion	smfsssmf	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		smfsssmf.r	⊢ ( 𝜑 → 𝑅 ∈ SAlg )
2		smfsssmf.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		smfsssmf.i	⊢ ( 𝜑 → 𝑅 ⊆ 𝑆 )
4		smfsssmf.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑅 ) )
5		nfv	⊢ Ⅎ 𝑎 𝜑
6		eqid	⊢ dom 𝐹 = dom 𝐹
7	1 4 6	smfdmss	⊢ ( 𝜑 → dom 𝐹 ⊆ ∪ 𝑅 )
8	3	unissd	⊢ ( 𝜑 → ∪ 𝑅 ⊆ ∪ 𝑆 )
9	7 8	sstrd	⊢ ( 𝜑 → dom 𝐹 ⊆ ∪ 𝑆 )
10	1 4 6	smff	⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℝ )
11		ssrest	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝑅 ⊆ 𝑆 ) → ( 𝑅 ↾t dom 𝐹 ) ⊆ ( 𝑆 ↾t dom 𝐹 ) )
12	2 3 11	syl2anc	⊢ ( 𝜑 → ( 𝑅 ↾t dom 𝐹 ) ⊆ ( 𝑆 ↾t dom 𝐹 ) )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑅 ↾t dom 𝐹 ) ⊆ ( 𝑆 ↾t dom 𝐹 ) )
14	1	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑅 ∈ SAlg )
15	4	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐹 ∈ ( SMblFn ‘ 𝑅 ) )
16		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ )
17	14 15 6 16	smfpreimalt	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑅 ↾t dom 𝐹 ) )
18	13 17	sseldd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) )
19	5 2 9 10 18	issmfd	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )