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 sseldi ( 𝑛𝑍𝑛 ∈ ℤ )
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 𝐷 ) )