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 φ R SAlg
smfsssmf.s φ S SAlg
smfsssmf.i φ R S
smfsssmf.f φ F SMblFn R
Assertion smfsssmf φ F SMblFn S

Proof

Step Hyp Ref Expression
1 smfsssmf.r φ R SAlg
2 smfsssmf.s φ S SAlg
3 smfsssmf.i φ R S
4 smfsssmf.f φ F SMblFn R
5 nfv a φ
6 eqid dom F = dom F
7 1 4 6 smfdmss φ dom F R
8 3 unissd φ R S
9 7 8 sstrd φ dom F S
10 1 4 6 smff φ F : dom F
11 ssrest S SAlg R S R 𝑡 dom F S 𝑡 dom F
12 2 3 11 syl2anc φ R 𝑡 dom F S 𝑡 dom F
13 12 adantr φ a R 𝑡 dom F S 𝑡 dom F
14 1 adantr φ a R SAlg
15 4 adantr φ a F SMblFn R
16 simpr φ a a
17 14 15 6 16 smfpreimalt φ a x dom F | F x < a R 𝑡 dom F
18 13 17 sseldd φ a x dom F | F x < a S 𝑡 dom F
19 5 2 9 10 18 issmfd φ F SMblFn S