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 = ( ZZ>= ` M )
	smflimlem1.2	\|- ( ph -> S e. SAlg )
	smflimlem1.3	\|- D = { x e. U_ n e. Z \|^\|_ m e. ( ZZ>= ` n ) dom ( F ` m ) \| ( m e. Z \|-> ( ( F ` m ) ` x ) ) e. dom ~~> }
	smflimlem1.4	\|- P = ( m e. Z , k e. NN \|-> { s e. S \| { x e. dom ( F ` m ) \| ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
	smflimlem1.5	\|- H = ( m e. Z , k e. NN \|-> ( C ` ( m P k ) ) )
	smflimlem1.6	\|- I = \|^\|_ k e. NN U_ n e. Z \|^\|_ m e. ( ZZ>= ` n ) ( m H k )
	smflimlem1.7	\|- ( ( ph /\ r e. ran P ) -> ( C ` r ) e. r )
Assertion	smflimlem1	\|- ( ph -> ( D i^i I ) e. ( S \|`t D ) )

Proof

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

Metamath Proof Explorer

Theorem smflimlem1

Proof