Theorem 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	⊢ Ⅎ 𝑚 𝐹
	smflim2.x	⊢ Ⅎ 𝑥 𝐹
	smflim2.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	smflim2.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	smflim2.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smflim2.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
	smflim2.d	⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
	smflim2.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
Assertion	smflim2	⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		smflim2.n	⊢ Ⅎ 𝑚 𝐹
2		smflim2.x	⊢ Ⅎ 𝑥 𝐹
3		smflim2.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		smflim2.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5		smflim2.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
6		smflim2.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
7		smflim2.d	⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
8		smflim2.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
9		nfcv	⊢ Ⅎ 𝑗 𝐹
10		nfcv	⊢ Ⅎ 𝑦 𝐹
11		nfcv	⊢ Ⅎ 𝑥 𝑍
12		nfcv	⊢ Ⅎ 𝑥 ( ℤ≥ ‘ 𝑛 )
13		nfcv	⊢ Ⅎ 𝑥 𝑚
14	2 13	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑚 )
15	14	nfdm	⊢ Ⅎ 𝑥 dom ( 𝐹 ‘ 𝑚 )
16	12 15	nfiin	⊢ Ⅎ 𝑥 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
17	11 16	nfiun	⊢ Ⅎ 𝑥 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
18		nfcv	⊢ Ⅎ 𝑦 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
19		nfv	⊢ Ⅎ 𝑦 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝
20		nfcv	⊢ Ⅎ 𝑗 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 )
21		nfcv	⊢ Ⅎ 𝑚 𝑗
22	1 21	nffv	⊢ Ⅎ 𝑚 ( 𝐹 ‘ 𝑗 )
23		nfcv	⊢ Ⅎ 𝑚 𝑦
24	22 23	nffv	⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 )
25		fveq2	⊢ ( 𝑚 = 𝑗 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑗 ) )
26	25	fveq1d	⊢ ( 𝑚 = 𝑗 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) )
27	20 24 26	cbvmpt	⊢ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) = ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) )
28		nfcv	⊢ Ⅎ 𝑥 𝑗
29	2 28	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑗 )
30		nfcv	⊢ Ⅎ 𝑥 𝑦
31	29 30	nffv	⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 )
32	11 31	nfmpt	⊢ Ⅎ 𝑥 ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) )
33	27 32	nfcxfr	⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) )
34		nfcv	⊢ Ⅎ 𝑥 dom ⇝
35	33 34	nfel	⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝
36		fveq2	⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) )
37	36	mpteq2dv	⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) )
38	37	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ ) )
39	17 18 19 35 38	cbvrabw	⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } = { 𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ }
40		fveq2	⊢ ( 𝑛 = 𝑘 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑘 ) )
41	40	iineq1d	⊢ ( 𝑛 = 𝑘 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑚 ) )
42		nfcv	⊢ Ⅎ 𝑗 dom ( 𝐹 ‘ 𝑚 )
43	22	nfdm	⊢ Ⅎ 𝑚 dom ( 𝐹 ‘ 𝑗 )
44	25	dmeqd	⊢ ( 𝑚 = 𝑗 → dom ( 𝐹 ‘ 𝑚 ) = dom ( 𝐹 ‘ 𝑗 ) )
45	42 43 44	cbviin	⊢ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑗 )
46	45	a1i	⊢ ( 𝑛 = 𝑘 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑗 ) )
47	41 46	eqtrd	⊢ ( 𝑛 = 𝑘 → ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑗 ) )
48	47	cbviunv	⊢ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) = ∪ 𝑘 ∈ 𝑍 ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑗 )
49	48	eleq2i	⊢ ( 𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ↔ 𝑦 ∈ ∪ 𝑘 ∈ 𝑍 ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑗 ) )
50	27	eleq1i	⊢ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ ↔ ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ∈ dom ⇝ )
51	49 50	anbi12i	⊢ ( ( 𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ ) ↔ ( 𝑦 ∈ ∪ 𝑘 ∈ 𝑍 ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑗 ) ∧ ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ∈ dom ⇝ ) )
52	51	rabbia2	⊢ { 𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ } = { 𝑦 ∈ ∪ 𝑘 ∈ 𝑍 ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑗 ) ∣ ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ∈ dom ⇝ }
53	7 39 52	3eqtri	⊢ 𝐷 = { 𝑦 ∈ ∪ 𝑘 ∈ 𝑍 ∩ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) dom ( 𝐹 ‘ 𝑗 ) ∣ ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ∈ dom ⇝ }
54		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
55	7 54	nfcxfr	⊢ Ⅎ 𝑥 𝐷
56		nfcv	⊢ Ⅎ 𝑦 𝐷
57		nfcv	⊢ Ⅎ 𝑦 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
58		nfcv	⊢ Ⅎ 𝑥 ⇝
59	58 32	nffv	⊢ Ⅎ 𝑥 ( ⇝ ‘ ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) )
60	27	a1i	⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) = ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) )
61	37 60	eqtrd	⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) )
62	61	fveq2d	⊢ ( 𝑥 = 𝑦 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) )
63	55 56 57 59 62	cbvmptf	⊢ ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) )
64	8 63	eqtri	⊢ 𝐺 = ( 𝑦 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑦 ) ) ) )
65	9 10 3 4 5 6 53 64	smflim	⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )