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 Z = M
smflimlem1.2 φ S SAlg
smflimlem1.3 D = x n Z m n dom F m | m Z F m x dom
smflimlem1.4 P = m Z , k s S | x dom F m | F m x < A + 1 k = s dom F m
smflimlem1.5 H = m Z , k C m P k
smflimlem1.6 I = k n Z m n m H k
smflimlem1.7 φ r ran P C r r
Assertion smflimlem1 φ D I S 𝑡 D

Proof

Step Hyp Ref Expression
1 smflimlem1.1 Z = M
2 smflimlem1.2 φ S SAlg
3 smflimlem1.3 D = x n Z m n dom F m | m Z F m x dom
4 smflimlem1.4 P = m Z , k s S | x dom F m | F m x < A + 1 k = s dom F m
5 smflimlem1.5 H = m Z , k C m P k
6 smflimlem1.6 I = k n Z m n m H k
7 smflimlem1.7 φ r ran P C r r
8 fvex M V
9 1 8 eqeltri Z V
10 uzssz M
11 1 eleq2i n Z n M
12 11 biimpi n Z n M
13 10 12 sselid n Z n
14 uzid n n n
15 13 14 syl n Z n n
16 15 ne0d n Z n
17 fvex F m V
18 17 dmex dom F m V
19 18 rgenw m n dom F m V
20 19 a1i n Z m n dom F m V
21 iinexg n m n dom F m V m n dom F m V
22 16 20 21 syl2anc n Z m n dom F m V
23 22 rgen n Z m n dom F m V
24 iunexg Z V n Z m n dom F m V n Z m n dom F m V
25 9 23 24 mp2an n Z m n dom F m V
26 25 rabex x n Z m n dom F m | m Z F m x dom V
27 3 26 eqeltri D V
28 27 a1i φ D V
29 nnct ω
30 29 a1i φ ω
31 nnn0
32 31 a1i φ
33 2 adantr φ k S SAlg
34 1 uzct Z ω
35 34 a1i φ k Z ω
36 33 adantr φ k n Z S SAlg
37 eqid n = n
38 37 uzct n ω
39 38 a1i φ k n Z n ω
40 16 adantl φ k n Z n
41 simpll φ n Z m n φ
42 41 adantllr φ k n Z m n φ
43 simpll k n Z m n k
44 43 adantlll φ k n Z m n k
45 1 uztrn2 n Z j n j Z
46 45 ssd n Z n Z
47 46 sselda n Z m n m Z
48 47 adantll φ k n Z m n m Z
49 simp3 φ k m Z m Z
50 simp2 φ k m Z k
51 fvex C m P k V
52 51 a1i φ k m Z C m P k V
53 5 ovmpt4g m Z k C m P k V m H k = C m P k
54 49 50 52 53 syl3anc φ k m Z m H k = C m P k
55 simp1 φ k m Z φ
56 eqid s S | x dom F m | F m x < A + 1 k = s dom F m = s S | x dom F m | F m x < A + 1 k = s dom F m
57 56 2 rabexd φ s S | x dom F m | F m x < A + 1 k = s dom F m V
58 55 57 syl φ k m Z s S | x dom F m | F m x < A + 1 k = s dom F m V
59 4 ovmpt4g m Z k s S | x dom F m | F m x < A + 1 k = s dom F m V m P k = s S | x dom F m | F m x < A + 1 k = s dom F m
60 49 50 58 59 syl3anc φ k m Z m P k = s S | x dom F m | F m x < A + 1 k = s dom F m
61 ssrab2 s S | x dom F m | F m x < A + 1 k = s dom F m S
62 60 61 eqsstrdi φ k m Z m P k S
63 57 ralrimivw φ k s S | x dom F m | F m x < A + 1 k = s dom F m V
64 63 ralrimivw φ m Z k s S | x dom F m | F m x < A + 1 k = s dom F m V
65 64 3ad2ant1 φ k m Z m Z k s S | x dom F m | F m x < A + 1 k = s dom F m V
66 4 elrnmpoid m Z k m Z k s S | x dom F m | F m x < A + 1 k = s dom F m V m P k ran P
67 49 50 65 66 syl3anc φ k m Z m P k ran P
68 ovex m P k V
69 eleq1 r = m P k r ran P m P k ran P
70 69 anbi2d r = m P k φ r ran P φ m P k ran P
71 fveq2 r = m P k C r = C m P k
72 id r = m P k r = m P k
73 71 72 eleq12d r = m P k C r r C m P k m P k
74 70 73 imbi12d r = m P k φ r ran P C r r φ m P k ran P C m P k m P k
75 68 74 7 vtocl φ m P k ran P C m P k m P k
76 55 67 75 syl2anc φ k m Z C m P k m P k
77 62 76 sseldd φ k m Z C m P k S
78 54 77 eqeltrd φ k m Z m H k S
79 42 44 48 78 syl3anc φ k n Z m n m H k S
80 36 39 40 79 saliincl φ k n Z m n m H k S
81 33 35 80 saliuncl φ k n Z m n m H k S
82 2 30 32 81 saliincl φ k n Z m n m H k S
83 6 82 eqeltrid φ I S
84 incom D I = I D
85 2 28 83 84 elrestd φ D I S 𝑡 D