Theorem smfinf

Description: The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smfinf.n	⊢ Ⅎ 𝑛 𝐹
	smfinf.x	⊢ Ⅎ 𝑥 𝐹
	smfinf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	smfinf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	smfinf.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfinf.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
	smfinf.d	⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) }
	smfinf.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ inf ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
Assertion	smfinf	⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		smfinf.n	⊢ Ⅎ 𝑛 𝐹
2		smfinf.x	⊢ Ⅎ 𝑥 𝐹
3		smfinf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		smfinf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5		smfinf.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
6		smfinf.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
7		smfinf.d	⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) }
8		smfinf.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ inf ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
9		nfcv	⊢ Ⅎ 𝑤 ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
10		nfcv	⊢ Ⅎ 𝑥 𝑍
11		nfcv	⊢ Ⅎ 𝑥 𝑚
12	2 11	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑚 )
13	12	nfdm	⊢ Ⅎ 𝑥 dom ( 𝐹 ‘ 𝑚 )
14	10 13	nfiin	⊢ Ⅎ 𝑥 ∩ 𝑚 ∈ 𝑍 dom ( 𝐹 ‘ 𝑚 )
15		nfv	⊢ Ⅎ 𝑤 ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 )
16		nfcv	⊢ Ⅎ 𝑥 ℝ
17		nfcv	⊢ Ⅎ 𝑥 𝑧
18		nfcv	⊢ Ⅎ 𝑥 ≤
19		nfcv	⊢ Ⅎ 𝑥 𝑤
20	12 19	nffv	⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 )
21	17 18 20	nfbr	⊢ Ⅎ 𝑥 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 )
22	10 21	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 )
23	16 22	nfrex	⊢ Ⅎ 𝑥 ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 )
24		nfcv	⊢ Ⅎ 𝑚 dom ( 𝐹 ‘ 𝑛 )
25		nfcv	⊢ Ⅎ 𝑛 𝑚
26	1 25	nffv	⊢ Ⅎ 𝑛 ( 𝐹 ‘ 𝑚 )
27	26	nfdm	⊢ Ⅎ 𝑛 dom ( 𝐹 ‘ 𝑚 )
28		fveq2	⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑚 ) )
29	28	dmeqd	⊢ ( 𝑛 = 𝑚 → dom ( 𝐹 ‘ 𝑛 ) = dom ( 𝐹 ‘ 𝑚 ) )
30	24 27 29	cbviin	⊢ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) = ∩ 𝑚 ∈ 𝑍 dom ( 𝐹 ‘ 𝑚 )
31	30	a1i	⊢ ( 𝑥 = 𝑤 → ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) = ∩ 𝑚 ∈ 𝑍 dom ( 𝐹 ‘ 𝑚 ) )
32		fveq2	⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) )
33	32	breq2d	⊢ ( 𝑥 = 𝑤 → ( 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) )
34	33	ralbidv	⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) )
35		nfv	⊢ Ⅎ 𝑚 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 )
36		nfcv	⊢ Ⅎ 𝑛 𝑦
37		nfcv	⊢ Ⅎ 𝑛 ≤
38		nfcv	⊢ Ⅎ 𝑛 𝑤
39	26 38	nffv	⊢ Ⅎ 𝑛 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 )
40	36 37 39	nfbr	⊢ Ⅎ 𝑛 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 )
41	28	fveq1d	⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
42	41	breq2d	⊢ ( 𝑛 = 𝑚 → ( 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ↔ 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
43	35 40 42	cbvralw	⊢ ( ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ↔ ∀ 𝑚 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
44	43	a1i	⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ↔ ∀ 𝑚 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
45	34 44	bitrd	⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ∀ 𝑚 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
46	45	rexbidv	⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
47		breq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ↔ 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
48	47	ralbidv	⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑚 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ↔ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
49	48	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ↔ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
50	49	a1i	⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ↔ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
51	46 50	bitrd	⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
52	9 14 15 23 31 51	cbvrabcsfw	⊢ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } = { 𝑤 ∈ ∩ 𝑚 ∈ 𝑍 dom ( 𝐹 ‘ 𝑚 ) ∣ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) }
53	7 52	eqtri	⊢ 𝐷 = { 𝑤 ∈ ∩ 𝑚 ∈ 𝑍 dom ( 𝐹 ‘ 𝑚 ) ∣ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ 𝑍 𝑧 ≤ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) }
54		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) }
55	7 54	nfcxfr	⊢ Ⅎ 𝑥 𝐷
56		nfcv	⊢ Ⅎ 𝑤 𝐷
57		nfcv	⊢ Ⅎ 𝑤 inf ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < )
58	10 20	nfmpt	⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
59	58	nfrn	⊢ Ⅎ 𝑥 ran ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
60		nfcv	⊢ Ⅎ 𝑥 <
61	59 16 60	nfinf	⊢ Ⅎ 𝑥 inf ( ran ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) , ℝ , < )
62	32	mpteq2dv	⊢ ( 𝑥 = 𝑤 → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) )
63		nfcv	⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 )
64	63 39 41	cbvmpt	⊢ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
65	64	a1i	⊢ ( 𝑥 = 𝑤 → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
66	62 65	eqtrd	⊢ ( 𝑥 = 𝑤 → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
67	66	rneqd	⊢ ( 𝑥 = 𝑤 → ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ran ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
68	67	infeq1d	⊢ ( 𝑥 = 𝑤 → inf ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) = inf ( ran ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) , ℝ , < ) )
69	55 56 57 61 68	cbvmptf	⊢ ( 𝑥 ∈ 𝐷 ↦ inf ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) = ( 𝑤 ∈ 𝐷 ↦ inf ( ran ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) , ℝ , < ) )
70	8 69	eqtri	⊢ 𝐺 = ( 𝑤 ∈ 𝐷 ↦ inf ( ran ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) , ℝ , < ) )
71	3 4 5 6 53 70	smfinflem	⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )