smflim2

Description: The limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of Fremlin1 p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of Fremlin1 p. 39 ). TODO: this has fewer distinct variable conditions than smflim and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smflim2.n	\|- F/_ m F
	smflim2.x	\|- F/_ x F
	smflim2.m	\|- ( ph -> M e. ZZ )
	smflim2.z	\|- Z = ( ZZ>= ` M )
	smflim2.s	\|- ( ph -> S e. SAlg )
	smflim2.f	\|- ( ph -> F : Z --> ( SMblFn ` S ) )
	smflim2.d	\|- D = { x e. U_ n e. Z \|^\|_ m e. ( ZZ>= ` n ) dom ( F ` m ) \| ( m e. Z \|-> ( ( F ` m ) ` x ) ) e. dom ~~> }
	smflim2.g	\|- G = ( x e. D \|-> ( ~~> ` ( m e. Z \|-> ( ( F ` m ) ` x ) ) ) )
Assertion	smflim2	\|- ( ph -> G e. ( SMblFn ` S ) )

Proof

Step	Hyp	Ref	Expression
1		smflim2.n	\|- F/_ m F
2		smflim2.x	\|- F/_ x F
3		smflim2.m	\|- ( ph -> M e. ZZ )
4		smflim2.z	\|- Z = ( ZZ>= ` M )
5		smflim2.s	\|- ( ph -> S e. SAlg )
6		smflim2.f	\|- ( ph -> F : Z --> ( SMblFn ` S ) )
7		smflim2.d	\|- D = { x e. U_ n e. Z \|^\|_ m e. ( ZZ>= ` n ) dom ( F ` m ) \| ( m e. Z \|-> ( ( F ` m ) ` x ) ) e. dom ~~> }
8		smflim2.g	\|- G = ( x e. D \|-> ( ~~> ` ( m e. Z \|-> ( ( F ` m ) ` x ) ) ) )
9		nfcv	\|- F/_ j F
10		nfcv	\|- F/_ y F
11		nfcv	\|- F/_ x Z
12		nfcv	\|- F/_ x ( ZZ>= ` n )
13		nfcv	\|- F/_ x m
14	2 13	nffv	\|- F/_ x ( F ` m )
15	14	nfdm	\|- F/_ x dom ( F ` m )
16	12 15	nfiin	\|- F/_ x \|^\|_ m e. ( ZZ>= ` n ) dom ( F ` m )
17	11 16	nfiun	\|- F/_ x U_ n e. Z \|^\|_ m e. ( ZZ>= ` n ) dom ( F ` m )
18		nfcv	\|- F/_ y U_ n e. Z \|^\|_ m e. ( ZZ>= ` n ) dom ( F ` m )
19		nfv	\|- F/ y ( m e. Z \|-> ( ( F ` m ) ` x ) ) e. dom ~~>
20		nfcv	\|- F/_ j ( ( F ` m ) ` y )
21		nfcv	\|- F/_ m j
22	1 21	nffv	\|- F/_ m ( F ` j )
23		nfcv	\|- F/_ m y
24	22 23	nffv	\|- F/_ m ( ( F ` j ) ` y )
25		fveq2	\|- ( m = j -> ( F ` m ) = ( F ` j ) )
26	25	fveq1d	\|- ( m = j -> ( ( F ` m ) ` y ) = ( ( F ` j ) ` y ) )
27	20 24 26	cbvmpt	\|- ( m e. Z \|-> ( ( F ` m ) ` y ) ) = ( j e. Z \|-> ( ( F ` j ) ` y ) )
28		nfcv	\|- F/_ x j
29	2 28	nffv	\|- F/_ x ( F ` j )
30		nfcv	\|- F/_ x y
31	29 30	nffv	\|- F/_ x ( ( F ` j ) ` y )
32	11 31	nfmpt	\|- F/_ x ( j e. Z \|-> ( ( F ` j ) ` y ) )
33	27 32	nfcxfr	\|- F/_ x ( m e. Z \|-> ( ( F ` m ) ` y ) )
34		nfcv	\|- F/_ x dom ~~>
35	33 34	nfel	\|- F/ x ( m e. Z \|-> ( ( F ` m ) ` y ) ) e. dom ~~>
36		fveq2	\|- ( x = y -> ( ( F ` m ) ` x ) = ( ( F ` m ) ` y ) )
37	36	mpteq2dv	\|- ( x = y -> ( m e. Z \|-> ( ( F ` m ) ` x ) ) = ( m e. Z \|-> ( ( F ` m ) ` y ) ) )
38	37	eleq1d	\|- ( x = y -> ( ( m e. Z \|-> ( ( F ` m ) ` x ) ) e. dom ~~> <-> ( m e. Z \|-> ( ( F ` m ) ` y ) ) e. dom ~~> ) )
39	17 18 19 35 38	cbvrabw	\|- { x e. U_ n e. Z \|^\|_ m e. ( ZZ>= ` n ) dom ( F ` m ) \| ( m e. Z \|-> ( ( F ` m ) ` x ) ) e. dom ~~> } = { y e. U_ n e. Z \|^\|_ m e. ( ZZ>= ` n ) dom ( F ` m ) \| ( m e. Z \|-> ( ( F ` m ) ` y ) ) e. dom ~~> }
40		fveq2	\|- ( n = k -> ( ZZ>= ` n ) = ( ZZ>= ` k ) )
41	40	iineq1d	\|- ( n = k -> \|^\|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = \|^\|_ m e. ( ZZ>= ` k ) dom ( F ` m ) )
42		nfcv	\|- F/_ j dom ( F ` m )
43	22	nfdm	\|- F/_ m dom ( F ` j )
44	25	dmeqd	\|- ( m = j -> dom ( F ` m ) = dom ( F ` j ) )
45	42 43 44	cbviin	\|- \|^\|_ m e. ( ZZ>= ` k ) dom ( F ` m ) = \|^\|_ j e. ( ZZ>= ` k ) dom ( F ` j )
46	45	a1i	\|- ( n = k -> \|^\|_ m e. ( ZZ>= ` k ) dom ( F ` m ) = \|^\|_ j e. ( ZZ>= ` k ) dom ( F ` j ) )
47	41 46	eqtrd	\|- ( n = k -> \|^\|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = \|^\|_ j e. ( ZZ>= ` k ) dom ( F ` j ) )
48	47	cbviunv	\|- U_ n e. Z \|^\|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = U_ k e. Z \|^\|_ j e. ( ZZ>= ` k ) dom ( F ` j )
49	48	eleq2i	\|- ( y e. U_ n e. Z \|^\|_ m e. ( ZZ>= ` n ) dom ( F ` m ) <-> y e. U_ k e. Z \|^\|_ j e. ( ZZ>= ` k ) dom ( F ` j ) )
50	27	eleq1i	\|- ( ( m e. Z \|-> ( ( F ` m ) ` y ) ) e. dom ~~> <-> ( j e. Z \|-> ( ( F ` j ) ` y ) ) e. dom ~~> )
51	49 50	anbi12i	\|- ( ( y e. U_ n e. Z \|^\|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ ( m e. Z \|-> ( ( F ` m ) ` y ) ) e. dom ~~> ) <-> ( y e. U_ k e. Z \|^\|_ j e. ( ZZ>= ` k ) dom ( F ` j ) /\ ( j e. Z \|-> ( ( F ` j ) ` y ) ) e. dom ~~> ) )
52	51	rabbia2	\|- { y e. U_ n e. Z \|^\|_ m e. ( ZZ>= ` n ) dom ( F ` m ) \| ( m e. Z \|-> ( ( F ` m ) ` y ) ) e. dom ~~> } = { y e. U_ k e. Z \|^\|_ j e. ( ZZ>= ` k ) dom ( F ` j ) \| ( j e. Z \|-> ( ( F ` j ) ` y ) ) e. dom ~~> }
53	7 39 52	3eqtri	\|- D = { y e. U_ k e. Z \|^\|_ j e. ( ZZ>= ` k ) dom ( F ` j ) \| ( j e. Z \|-> ( ( F ` j ) ` y ) ) e. dom ~~> }
54		nfrab1	\|- F/_ x { x e. U_ n e. Z \|^\|_ m e. ( ZZ>= ` n ) dom ( F ` m ) \| ( m e. Z \|-> ( ( F ` m ) ` x ) ) e. dom ~~> }
55	7 54	nfcxfr	\|- F/_ x D
56		nfcv	\|- F/_ y D
57		nfcv	\|- F/_ y ( ~~> ` ( m e. Z \|-> ( ( F ` m ) ` x ) ) )
58		nfcv	\|- F/_ x ~~>
59	58 32	nffv	\|- F/_ x ( ~~> ` ( j e. Z \|-> ( ( F ` j ) ` y ) ) )
60	27	a1i	\|- ( x = y -> ( m e. Z \|-> ( ( F ` m ) ` y ) ) = ( j e. Z \|-> ( ( F ` j ) ` y ) ) )
61	37 60	eqtrd	\|- ( x = y -> ( m e. Z \|-> ( ( F ` m ) ` x ) ) = ( j e. Z \|-> ( ( F ` j ) ` y ) ) )
62	61	fveq2d	\|- ( x = y -> ( ~~> ` ( m e. Z \|-> ( ( F ` m ) ` x ) ) ) = ( ~~> ` ( j e. Z \|-> ( ( F ` j ) ` y ) ) ) )
63	55 56 57 59 62	cbvmptf	\|- ( x e. D \|-> ( ~~> ` ( m e. Z \|-> ( ( F ` m ) ` x ) ) ) ) = ( y e. D \|-> ( ~~> ` ( j e. Z \|-> ( ( F ` j ) ` y ) ) ) )
64	8 63	eqtri	\|- G = ( y e. D \|-> ( ~~> ` ( j e. Z \|-> ( ( F ` j ) ` y ) ) ) )
65	9 10 3 4 5 6 53 64	smflim	\|- ( ph -> G e. ( SMblFn ` S ) )

Metamath Proof Explorer

Theorem smflim2

Proof