Theorem smfsup

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

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

Proof

Step	Hyp	Ref	Expression
1		smfsup.n	⊢ Ⅎ 𝑛 𝐹
2		smfsup.x	⊢ Ⅎ 𝑥 𝐹
3		smfsup.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		smfsup.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5		smfsup.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
6		smfsup.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
7		smfsup.d	⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 }
8		smfsup.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ sup ( 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	12 17	nffv	⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 )
19		nfcv	⊢ Ⅎ 𝑥 ≤
20		nfcv	⊢ Ⅎ 𝑥 𝑧
21	18 19 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	breq1d	⊢ ( 𝑥 = 𝑤 → ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ↔ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ≤ 𝑦 ) )
34	33	ralbidv	⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ↔ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ≤ 𝑦 ) )
35		nfv	⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ≤ 𝑦
36		nfcv	⊢ Ⅎ 𝑛 𝑤
37	26 36	nffv	⊢ Ⅎ 𝑛 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 )
38		nfcv	⊢ Ⅎ 𝑛 ≤
39		nfcv	⊢ Ⅎ 𝑛 𝑦
40	37 38 39	nfbr	⊢ Ⅎ 𝑛 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ≤ 𝑦
41	28	fveq1d	⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
42	41	breq1d	⊢ ( 𝑛 = 𝑚 → ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ≤ 𝑦 ↔ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ≤ 𝑦 ) )
43	35 40 42	cbvralw	⊢ ( ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ≤ 𝑦 ↔ ∀ 𝑚 ∈ 𝑍 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ≤ 𝑦 )
44	43	a1i	⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ≤ 𝑦 ↔ ∀ 𝑚 ∈ 𝑍 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ≤ 𝑦 ) )
45	34 44	bitrd	⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ↔ ∀ 𝑚 ∈ 𝑍 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ≤ 𝑦 ) )
46	45	rexbidv	⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑚 ∈ 𝑍 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ≤ 𝑦 ) )
47		breq2	⊢ ( 𝑦 = 𝑧 → ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ≤ 𝑦 ↔ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ≤ 𝑧 ) )
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	⊢ Ⅎ 𝑤 sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < )
58	10 18	nfmpt	⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
59	58	nfrn	⊢ Ⅎ 𝑥 ran ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
60		nfcv	⊢ Ⅎ 𝑥 <
61	59 16 60	nfsup	⊢ Ⅎ 𝑥 sup ( ran ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) , ℝ , < )
62	32	mpteq2dv	⊢ ( 𝑥 = 𝑤 → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) )
63		nfcv	⊢ Ⅎ 𝑚 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 )
64	63 37 41	cbvmpt	⊢ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
65	64	a1i	⊢ ( 𝑥 = 𝑤 → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
66	62 65	eqtrd	⊢ ( 𝑥 = 𝑤 → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
67	66	rneqd	⊢ ( 𝑥 = 𝑤 → ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ran ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
68	67	supeq1d	⊢ ( 𝑥 = 𝑤 → sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) = sup ( ran ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) , ℝ , < ) )
69	55 56 57 61 68	cbvmptf	⊢ ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) = ( 𝑤 ∈ 𝐷 ↦ sup ( ran ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) , ℝ , < ) )
70	8 69	eqtri	⊢ 𝐺 = ( 𝑤 ∈ 𝐷 ↦ sup ( ran ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) , ℝ , < ) )
71	3 4 5 6 53 70	smfsuplem3	⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )