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 1 2 5 smff ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℝ )
9 4 a1i ⊢ ( 𝜑 → ( 𝐵 ∩ dom 𝐹 ) ⊆ dom 𝐹 )
10 fssres ⊢ ( ( 𝐹 : dom 𝐹 ⟶ ℝ ∧ ( 𝐵 ∩ dom 𝐹 ) ⊆ dom 𝐹 ) → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) : ( 𝐵 ∩ dom 𝐹 ) ⟶ ℝ )
11 8 9 10 syl2anc ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) : ( 𝐵 ∩ dom 𝐹 ) ⟶ ℝ )
12 8 freld ⊢ ( 𝜑 → Rel 𝐹 )
13 resindm ⊢ ( Rel 𝐹 → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝐵 ) )
14 12 13 syl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝐵 ) )
15 14 eqcomd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) = ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) )
16 dmres ⊢ dom ( 𝐹 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐹 )
17 16 a1i ⊢ ( 𝜑 → dom ( 𝐹 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐹 ) )
18 15 17 feq12d ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) : dom ( 𝐹 ↾ 𝐵 ) ⟶ ℝ ↔ ( 𝐹 ↾ ( 𝐵 ∩ dom 𝐹 ) ) : ( 𝐵 ∩ dom 𝐹 ) ⟶ ℝ ) )
19 11 18 mpbird ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : dom ( 𝐹 ↾ 𝐵 ) ⟶ ℝ )
20 17 feq2d ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) : dom ( 𝐹 ↾ 𝐵 ) ⟶ ℝ ↔ ( 𝐹 ↾ 𝐵 ) : ( 𝐵 ∩ dom 𝐹 ) ⟶ ℝ ) )
21 19 20 mpbid ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : ( 𝐵 ∩ dom 𝐹 ) ⟶ ℝ )
22 1 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑆 ∈ SAlg )
23 2 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ )
25 22 23 5 24 smfpreimalt ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) )
26 2 dmexd ⊢ ( 𝜑 → dom 𝐹 ∈ V )
27 elrest ⊢ ( ( 𝑆 ∈ SAlg ∧ dom 𝐹 ∈ V ) → ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) ↔ ∃ 𝑤 ∈ 𝑆 { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) )
28 1 26 27 syl2anc ⊢ ( 𝜑 → ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) ↔ ∃ 𝑤 ∈ 𝑆 { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) ↔ ∃ 𝑤 ∈ 𝑆 { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) )
30 25 29 mpbid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ∃ 𝑤 ∈ 𝑆 { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) )
31 elinel1 ⊢ ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) → 𝑥 ∈ 𝐵 )
32 31 fvresd ⊢ ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
33 32 breq1d ⊢ ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) → ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 ↔ ( 𝐹 ‘ 𝑥 ) < 𝑎 ) )
34 33 rabbiia ⊢ { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 } = { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 }
35 34 a1i ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 } = { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
36 rabss2 ⊢ ( ( 𝐵 ∩ dom 𝐹 ) ⊆ dom 𝐹 → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ⊆ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
37 4 36 ax-mp ⊢ { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ⊆ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 }
38 id ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) )
39 inss1 ⊢ ( 𝑤 ∩ dom 𝐹 ) ⊆ 𝑤
40 39 a1i ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → ( 𝑤 ∩ dom 𝐹 ) ⊆ 𝑤 )
41 38 40 eqsstrd ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ⊆ 𝑤 )
42 37 41 sstrid ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ⊆ 𝑤 )
43 ssrab2 ⊢ { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ⊆ ( 𝐵 ∩ dom 𝐹 )
44 43 a1i ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ⊆ ( 𝐵 ∩ dom 𝐹 ) )
45 42 44 ssind ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ⊆ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) )
46 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 }
47 nfcv ⊢ Ⅎ 𝑥 ( 𝑤 ∩ dom 𝐹 )
48 46 47 nfeq ⊢ Ⅎ 𝑥 { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 )
49 elinel2 ⊢ ( 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) → 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) )
50 49 adantl ⊢ ( ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ∧ 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ) → 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) )
51 elinel1 ⊢ ( 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) → 𝑥 ∈ 𝑤 )
52 4 sseli ⊢ ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) → 𝑥 ∈ dom 𝐹 )
53 49 52 syl ⊢ ( 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) → 𝑥 ∈ dom 𝐹 )
54 51 53 elind ⊢ ( 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) → 𝑥 ∈ ( 𝑤 ∩ dom 𝐹 ) )
55 54 adantl ⊢ ( ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ∧ 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ) → 𝑥 ∈ ( 𝑤 ∩ dom 𝐹 ) )
56 38 eqcomd ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → ( 𝑤 ∩ dom 𝐹 ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
57 56 adantr ⊢ ( ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ∧ 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ) → ( 𝑤 ∩ dom 𝐹 ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
58 55 57 eleqtrd ⊢ ( ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ∧ 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ) → 𝑥 ∈ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
59 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) < 𝑎 ) )
60 59 biimpi ⊢ ( 𝑥 ∈ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } → ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) < 𝑎 ) )
61 60 simprd ⊢ ( 𝑥 ∈ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } → ( 𝐹 ‘ 𝑥 ) < 𝑎 )
62 58 61 syl ⊢ ( ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ∧ 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ) → ( 𝐹 ‘ 𝑥 ) < 𝑎 )
63 50 62 jca ⊢ ( ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ∧ 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ) → ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∧ ( 𝐹 ‘ 𝑥 ) < 𝑎 ) )
64 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ↔ ( 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∧ ( 𝐹 ‘ 𝑥 ) < 𝑎 ) )
65 63 64 sylibr ⊢ ( ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ∧ 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ) → 𝑥 ∈ { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
66 65 ex ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → ( 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) → 𝑥 ∈ { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ) )
67 48 66 ralrimi ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → ∀ 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) 𝑥 ∈ { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
68 nfcv ⊢ Ⅎ 𝑥 ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) )
69 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 }
70 68 69 dfss3f ⊢ ( ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ⊆ { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ↔ ∀ 𝑥 ∈ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) 𝑥 ∈ { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
71 67 70 sylibr ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ⊆ { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
72 38 38 38 71 4syl ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ⊆ { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
73 45 72 eqssd ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) )
74 35 73 eqtrd ⊢ ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) )
75 74 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) )
76 75 3adant2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑤 ∈ 𝑆 ∧ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) )
77 22 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑤 ∈ 𝑆 ∧ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) → 𝑆 ∈ SAlg )
78 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑤 ∈ 𝑆 ∧ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) → 𝜑 )
79 26 9 ssexd ⊢ ( 𝜑 → ( 𝐵 ∩ dom 𝐹 ) ∈ V )
80 78 79 syl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑤 ∈ 𝑆 ∧ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) → ( 𝐵 ∩ dom 𝐹 ) ∈ V )
81 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑤 ∈ 𝑆 ∧ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) → 𝑤 ∈ 𝑆 )
82 eqid ⊢ ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) = ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) )
83 77 80 81 82 elrestd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑤 ∈ 𝑆 ∧ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) → ( 𝑤 ∩ ( 𝐵 ∩ dom 𝐹 ) ) ∈ ( 𝑆 ↾t ( 𝐵 ∩ dom 𝐹 ) ) )
84 76 83 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑤 ∈ 𝑆 ∧ { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t ( 𝐵 ∩ dom 𝐹 ) ) )
85 84 3exp ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑤 ∈ 𝑆 → ( { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t ( 𝐵 ∩ dom 𝐹 ) ) ) ) )
86 85 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ∃ 𝑤 ∈ 𝑆 { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( 𝑤 ∩ dom 𝐹 ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t ( 𝐵 ∩ dom 𝐹 ) ) ) )
87 30 86 mpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ( 𝐵 ∩ dom 𝐹 ) ∣ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t ( 𝐵 ∩ dom 𝐹 ) ) )
88 3 1 7 21 87 issmfd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )