Theorem smfliminf

Description: The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	smfliminf.n	⊢ Ⅎ 𝑚 𝐹
	smfliminf.x	⊢ Ⅎ 𝑥 𝐹
	smfliminf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	smfliminf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	smfliminf.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfliminf.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
	smfliminf.d	⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ∈ ℝ }
	smfliminf.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( lim inf ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
Assertion	smfliminf	⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

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