Theorem smfsupxr

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	smfsupxr.n	⊢ Ⅎ 𝑛 𝐹
	smfsupxr.x	⊢ Ⅎ 𝑥 𝐹
	smfsupxr.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	smfsupxr.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	smfsupxr.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfsupxr.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
	smfsupxr.d	⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ }
	smfsupxr.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) )
Assertion	smfsupxr	⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		smfsupxr.n	⊢ Ⅎ 𝑛 𝐹
2		smfsupxr.x	⊢ Ⅎ 𝑥 𝐹
3		smfsupxr.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		smfsupxr.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5		smfsupxr.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
6		smfsupxr.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
7		smfsupxr.d	⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ }
8		smfsupxr.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) )
9	8	a1i	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) ) )
10	7	a1i	⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
11		nfv	⊢ Ⅎ 𝑛 𝜑
12		nfcv	⊢ Ⅎ 𝑛 𝑥
13		nfii1	⊢ Ⅎ 𝑛 ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
14	12 13	nfel	⊢ Ⅎ 𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
15	11 14	nfan	⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
16	3 4	uzn0d	⊢ ( 𝜑 → 𝑍 ≠ ∅ )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) → 𝑍 ≠ ∅ )
18	5	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
19	6	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( SMblFn ‘ 𝑆 ) )
20		eqid	⊢ dom ( 𝐹 ‘ 𝑛 ) = dom ( 𝐹 ‘ 𝑛 )
21	18 19 20	smff	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ )
22	21	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ )
23		eliinid	⊢ ( ( 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
24	23	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
25	22 24	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
26	15 17 25	supxrre3rnmpt	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) → ( sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) )
27	26	rabbidva	⊢ ( 𝜑 → { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 } )
28	10 27	eqtrd	⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 } )
29		nfmpt1	⊢ Ⅎ 𝑛 ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
30	29	nfrn	⊢ Ⅎ 𝑛 ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
31		nfcv	⊢ Ⅎ 𝑛 ℝ*
32		nfcv	⊢ Ⅎ 𝑛 <
33	30 31 32	nfsup	⊢ Ⅎ 𝑛 sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < )
34		nfcv	⊢ Ⅎ 𝑛 ℝ
35	33 34	nfel	⊢ Ⅎ 𝑛 sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ
36	35 13	nfrabw	⊢ Ⅎ 𝑛 { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ }
37	7 36	nfcxfr	⊢ Ⅎ 𝑛 𝐷
38	12 37	nfel	⊢ Ⅎ 𝑛 𝑥 ∈ 𝐷
39	11 38	nfan	⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ 𝐷 )
40	16	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑍 ≠ ∅ )
41	21	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ )
42		nfcv	⊢ Ⅎ 𝑥 𝑍
43		nfcv	⊢ Ⅎ 𝑥 𝑛
44	2 43	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑛 )
45	44	nfdm	⊢ Ⅎ 𝑥 dom ( 𝐹 ‘ 𝑛 )
46	42 45	nfiin	⊢ Ⅎ 𝑥 ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
47	46	ssrab2f	⊢ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } ⊆ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
48	7 47	eqsstri	⊢ 𝐷 ⊆ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
49		id	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ 𝐷 )
50	48 49	sselid	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
51	50 23	sylan	⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
52	51	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
53	41 52	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
54	49 7	eleqtrdi	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } )
55		rabidim2	⊢ ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ } → sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ )
56	54 55	syl	⊢ ( 𝑥 ∈ 𝐷 → sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ )
57	56	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ )
58	50	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
59	58 26	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) )
60	57 59	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
61	39 40 53 60	supxrrernmpt	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) = sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
62	28 61	mpteq12dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ* , < ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 } ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) )
63	9 62	eqtrd	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 } ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) )
64		eqid	⊢ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 } = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 }
65		eqid	⊢ ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 } ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) = ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 } ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
66	1 2 3 4 5 6 64 65	smfsup	⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 } ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) ∈ ( SMblFn ‘ 𝑆 ) )
67	63 66	eqeltrd	⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )