Metamath Proof Explorer

Theorem smflimlem1

Description: Lemma for the proof that the limit of a sequence of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of Fremlin1 p. 38 . This lemma proves that ( D i^i I ) is in the subspace sigma-algebra induced by D . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smflimlem1.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
smflimlem1.2 ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smflimlem1.3 ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
smflimlem1.4 ⊢ 𝑃 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
smflimlem1.5 ⊢ 𝐻 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
smflimlem1.6 ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 )
smflimlem1.7 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 )
Assertion smflimlem1 ( 𝜑 → ( 𝐷 ∩ 𝐼 ) ∈ ( 𝑆 ↾t 𝐷 ) )

Proof

Step Hyp Ref Expression
1 smflimlem1.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 smflimlem1.2 ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3 smflimlem1.3 ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
4 smflimlem1.4 ⊢ 𝑃 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
5 smflimlem1.5 ⊢ 𝐻 = ( 𝑚 ∈ 𝑍 , 𝑘 ∈ ℕ ↦ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
6 smflimlem1.6 ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 )
7 smflimlem1.7 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 )
8 fvex ⊢ ( ℤ≥ ‘ 𝑀 ) ∈ V
9 1 8 eqeltri ⊢ 𝑍 ∈ V
10 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
11 1 eleq2i ⊢ ( 𝑛 ∈ 𝑍 ↔ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
12 11 biimpi ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
13 10 12 sselid ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ )
14 uzid ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
15 13 14 syl ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
16 15 ne0d ⊢ ( 𝑛 ∈ 𝑍 → ( ℤ≥ ‘ 𝑛 ) ≠ ∅ )
17 fvex ⊢ ( 𝐹 ‘ 𝑚 ) ∈ V
18 17 dmex ⊢ dom ( 𝐹 ‘ 𝑚 ) ∈ V
19 18 rgenw ⊢ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V
20 19 a1i ⊢ ( 𝑛 ∈ 𝑍 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
21 iinexg ⊢ ( ( ( ℤ≥ ‘ 𝑛 ) ≠ ∅ ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
22 16 20 21 syl2anc ⊢ ( 𝑛 ∈ 𝑍 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
23 22 rgen ⊢ ∀ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V
24 iunexg ⊢ ( ( 𝑍 ∈ V ∧ ∀ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V ) → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V )
25 9 23 24 mp2an ⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∈ V
26 25 rabex ⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } ∈ V
27 3 26 eqeltri ⊢ 𝐷 ∈ V
28 27 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
29 nnct ⊢ ℕ ≼ ω
30 29 a1i ⊢ ( 𝜑 → ℕ ≼ ω )
31 nnn0 ⊢ ℕ ≠ ∅
32 31 a1i ⊢ ( 𝜑 → ℕ ≠ ∅ )
33 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑆 ∈ SAlg )
34 1 uzct ⊢ 𝑍 ≼ ω
35 34 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑍 ≼ ω )
36 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
37 eqid ⊢ ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑛 )
38 37 uzct ⊢ ( ℤ≥ ‘ 𝑛 ) ≼ ω
39 38 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑛 ) ≼ ω )
40 16 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑛 ) ≠ ∅ )
41 simpll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝜑 )
42 41 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝜑 )
43 simpll ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑘 ∈ ℕ )
44 43 adantlll ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑘 ∈ ℕ )
45 1 uztrn2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑗 ∈ 𝑍 )
46 45 ssd ⊢ ( 𝑛 ∈ 𝑍 → ( ℤ≥ ‘ 𝑛 ) ⊆ 𝑍 )
47 46 sselda ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
48 47 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 )
49 simp3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ 𝑍 )
50 simp2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → 𝑘 ∈ ℕ )
51 fvex ⊢ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ V
52 51 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ V )
53 5 ovmpt4g ⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ V ) → ( 𝑚 𝐻 𝑘 ) = ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
54 49 50 52 53 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝐻 𝑘 ) = ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
55 simp1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → 𝜑 )
56 eqid ⊢ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) }
57 56 2 rabexd ⊢ ( 𝜑 → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
58 55 57 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
59 4 ovmpt4g ⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V ) → ( 𝑚 𝑃 𝑘 ) = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
60 49 50 58 59 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝑃 𝑘 ) = { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } )
61 ssrab2 ⊢ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ⊆ 𝑆
62 60 61 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝑃 𝑘 ) ⊆ 𝑆 )
63 57 ralrimivw ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
64 63 ralrimivw ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
65 64 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V )
66 4 elrnmpoid ⊢ ( ( 𝑚 ∈ 𝑍 ∧ 𝑘 ∈ ℕ ∧ ∀ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ℕ { 𝑠 ∈ 𝑆 ∣ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑚 ) ∣ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) < ( 𝐴 + ( 1 / 𝑘 ) ) } = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑚 ) ) } ∈ V ) → ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 )
67 49 50 65 66 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 )
68 ovex ⊢ ( 𝑚 𝑃 𝑘 ) ∈ V
69 eleq1 ⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( 𝑟 ∈ ran 𝑃 ↔ ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) )
70 69 anbi2d ⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) ↔ ( 𝜑 ∧ ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) ) )
71 fveq2 ⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( 𝐶 ‘ 𝑟 ) = ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) )
72 id ⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → 𝑟 = ( 𝑚 𝑃 𝑘 ) )
73 71 72 eleq12d ⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 ↔ ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) ) )
74 70 73 imbi12d ⊢ ( 𝑟 = ( 𝑚 𝑃 𝑘 ) → ( ( ( 𝜑 ∧ 𝑟 ∈ ran 𝑃 ) → ( 𝐶 ‘ 𝑟 ) ∈ 𝑟 ) ↔ ( ( 𝜑 ∧ ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) ) ) )
75 68 74 7 vtocl ⊢ ( ( 𝜑 ∧ ( 𝑚 𝑃 𝑘 ) ∈ ran 𝑃 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) )
76 55 67 75 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ ( 𝑚 𝑃 𝑘 ) )
77 62 76 sseldd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝐶 ‘ ( 𝑚 𝑃 𝑘 ) ) ∈ 𝑆 )
78 54 77 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 𝐻 𝑘 ) ∈ 𝑆 )
79 42 44 48 78 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝑚 𝐻 𝑘 ) ∈ 𝑆 )
80 36 39 40 79 saliincl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑍 ) → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ∈ 𝑆 )
81 33 35 80 saliuncl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ∈ 𝑆 )
82 2 30 32 81 saliincl ⊢ ( 𝜑 → ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝑚 𝐻 𝑘 ) ∈ 𝑆 )
83 6 82 eqeltrid ⊢ ( 𝜑 → 𝐼 ∈ 𝑆 )
84 incom ⊢ ( 𝐷 ∩ 𝐼 ) = ( 𝐼 ∩ 𝐷 )
85 2 28 83 84 elrestd ⊢ ( 𝜑 → ( 𝐷 ∩ 𝐼 ) ∈ ( 𝑆 ↾t 𝐷 ) )