Metamath Proof Explorer

Theorem sssmf

Description: The restriction of a sigma-measurable function, is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses sssmf.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
sssmf.f ⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
Assertion sssmf ( 𝜑 → ( 𝐹 ↾ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 sssmf.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2 sssmf.f ⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
3 nfv ⊢ Ⅎ 𝑎 𝜑
4 inss2 ⊢ ( 𝐵 ∩ dom 𝐹 ) ⊆ dom 𝐹
5 eqid ⊢ dom 𝐹 = dom 𝐹
6 1 2 5 smfdmss ⊢ ( 𝜑 → dom 𝐹 ⊆ ∪ 𝑆 )
7 4 6 sstrid ⊢ ( 𝜑 → ( 𝐵 ∩ dom 𝐹 ) ⊆ ∪ 𝑆 )
8 resindm ⊢ ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝐵 )
9 8 a1i ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝐵 ) )
10 1 2 5 smff ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℝ )
11 4 a1i ⊢ ( 𝜑 → ( 𝐵 ∩ dom 𝐹 ) ⊆ dom 𝐹 )
12 10 11 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) : ( 𝐵 ∩ dom 𝐹 ) ⟶ ℝ )
13 9 12 feq1dd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : ( 𝐵 ∩ dom 𝐹 ) ⟶ ℝ )
14 1 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑆 ∈ SAlg )
15 2 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ )
17 14 15 5 16 smfpreimalt ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) )
18 2 dmexd ⊢ ( 𝜑 → dom 𝐹 ∈ V )
19 elrest ⊢ ( ( 𝑆 ∈ SAlg ∧ dom 𝐹 ∈ V ) → ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) ↔ ∃ 𝑤 ∈ 𝑆 { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) )
20 1 18 19 syl2anc ⊢ ( 𝜑 → ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) ↔ ∃ 𝑤 ∈ 𝑆 { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) ↔ ∃ 𝑤 ∈ 𝑆 { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) )
22 17 21 mpbid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ∃ 𝑤 ∈ 𝑆 { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) )
23 elinel1 ⊢ ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) → 𝑥 ∈ 𝐵 )
24 23 fvresd ⊢ ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
25 24 breq1d ⊢ ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) → ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 ↔ ( 𝐹 ‘ 𝑥 ) < 𝑎 ) )
26 25 rabbiia ⊢ { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 } = { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 }
27 rabss2 ⊢ ( ( 𝐵 ∩ dom 𝐹 ) ⊆ dom 𝐹 → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ⊆ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
28 4 27 ax-mp ⊢ { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ⊆ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 }
29 id ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) )
30 inss1 ⊢ ( 𝑤 ∩ dom 𝐹 ) ⊆ 𝑤
31 29 30 eqsstrdi ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ⊆ 𝑤 )
32 28 31 sstrid ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ⊆ 𝑤 )
33 ssrab2 ⊢ { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ⊆ ( 𝐵 ∩ dom 𝐹 )
34 33 a1i ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ⊆ ( 𝐵 ∩ dom 𝐹 ) )
35 32 34 ssind ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ⊆ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) )
36 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 }
37 36 nfeq1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 )
38 nfcv ⊢ Ⅎ 𝑥 ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) )
39 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 }
40 elinel2 ⊢ ( 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) → 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) )
41 40 adantl ⊢ ( ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ∧ 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ) → 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) )
42 elinel1 ⊢ ( 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) → 𝑥 ∈ 𝑤 )
43 40 elin2d ⊢ ( 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) → 𝑥 ∈ dom 𝐹 )
44 42 43 elind ⊢ ( 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) → 𝑥 ∈ ( 𝑤 ∩ dom 𝐹 ) )
45 44 adantl ⊢ ( ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ∧ 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ) → 𝑥 ∈ ( 𝑤 ∩ dom 𝐹 ) )
46 29 eqcomd ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → ( 𝑤 ∩ dom 𝐹 ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
47 46 adantr ⊢ ( ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ∧ 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ) → ( 𝑤 ∩ dom 𝐹 ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
48 45 47 eleqtrd ⊢ ( ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ∧ 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
49 rabidim2 ⊢ ( 𝑥 ∈ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } → ( 𝐹 ‘ 𝑥 ) < 𝑎 )
50 48 49 syl ⊢ ( ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ∧ 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ) → ( 𝐹 ‘ 𝑥 ) < 𝑎 )
51 41 50 rabidd ⊢ ( ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ∧ 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ) → 𝑥 ∈ { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
52 37 38 39 51 ssdf2 ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ⊆ { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
53 35 52 eqssd ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) )
54 26 53 eqtrid ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) )
55 54 3ad2ant3 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑤 ∈ 𝑆 ∧ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) )
56 14 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑤 ∈ 𝑆 ∧ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) → 𝑆 ∈ SAlg )
57 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑤 ∈ 𝑆 ∧ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) → 𝜑 )
58 18 11 ssexd ⊢ ( 𝜑 → ( 𝐵 ∩ dom 𝐹 ) ∈ V )
59 57 58 syl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑤 ∈ 𝑆 ∧ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) → ( 𝐵 ∩ dom 𝐹 ) ∈ V )
60 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑤 ∈ 𝑆 ∧ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) → 𝑤 ∈ 𝑆 )
61 eqid ⊢ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) = ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) )
62 56 59 60 61 elrestd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑤 ∈ 𝑆 ∧ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) → ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ∈ ( 𝑆 ↾t ( 𝐵 ∩ dom 𝐹 ) ) )
63 55 62 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑤 ∈ 𝑆 ∧ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t ( 𝐵 ∩ dom 𝐹 ) ) )
64 63 rexlimdv3a ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ∃ 𝑤 ∈ 𝑆 { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t ( 𝐵 ∩ dom 𝐹 ) ) ) )
65 22 64 mpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t ( 𝐵 ∩ dom 𝐹 ) ) )
66 3 1 7 13 65 issmfd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )