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	|- ( ph -> R e. SAlg )
	smfsssmf.s	|- ( ph -> S e. SAlg )
	smfsssmf.i	|- ( ph -> R C_ S )
	smfsssmf.f	|- ( ph -> F e. ( SMblFn ` R ) )
Assertion	smfsssmf	|- ( ph -> F e. ( SMblFn ` S ) )

Proof

Step	Hyp	Ref	Expression
1		smfsssmf.r	|- ( ph -> R e. SAlg )
2		smfsssmf.s	|- ( ph -> S e. SAlg )
3		smfsssmf.i	|- ( ph -> R C_ S )
4		smfsssmf.f	|- ( ph -> F e. ( SMblFn ` R ) )
5		nfv	|- F/ a ph
6		eqid	|- dom F = dom F
7	1 4 6	smfdmss	|- ( ph -> dom F C_ U. R )
8	3	unissd	|- ( ph -> U. R C_ U. S )
9	7 8	sstrd	|- ( ph -> dom F C_ U. S )
10	1 4 6	smff	|- ( ph -> F : dom F --> RR )
11		ssrest	|- ( ( S e. SAlg /\ R C_ S ) -> ( R |`t dom F ) C_ ( S |`t dom F ) )
12	2 3 11	syl2anc	|- ( ph -> ( R |`t dom F ) C_ ( S |`t dom F ) )
13	12	adantr	|- ( ( ph /\ a e. RR ) -> ( R |`t dom F ) C_ ( S |`t dom F ) )
14	1	adantr	|- ( ( ph /\ a e. RR ) -> R e. SAlg )
15	4	adantr	|- ( ( ph /\ a e. RR ) -> F e. ( SMblFn ` R ) )
16		simpr	|- ( ( ph /\ a e. RR ) -> a e. RR )
17	14 15 6 16	smfpreimalt	|- ( ( ph /\ a e. RR ) -> { x e. dom F | ( F ` x ) < a } e. ( R |`t dom F ) )
18	13 17	sseldd	|- ( ( ph /\ a e. RR ) -> { x e. dom F | ( F ` x ) < a } e. ( S |`t dom F ) )
19	5 2 9 10 18	issmfd	|- ( ph -> F e. ( SMblFn ` S ) )