Theorem smfsuplem3

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

Proof

Step	Hyp	Ref	Expression
1		smfsuplem3.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		smfsuplem3.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		smfsuplem3.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		smfsuplem3.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
5		smfsuplem3.d	⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 }
6		smfsuplem3.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
7		nfv	⊢ Ⅎ 𝑎 𝜑
8		ssrab2	⊢ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 } ⊆ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
9	5 8	eqsstri	⊢ 𝐷 ⊆ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
10	9	a1i	⊢ ( 𝜑 → 𝐷 ⊆ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
11		uzid	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
12	1 11	syl	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
13	12 2	eleqtrrdi	⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
14		fveq2	⊢ ( 𝑛 = 𝑀 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑀 ) )
15	14	dmeqd	⊢ ( 𝑛 = 𝑀 → dom ( 𝐹 ‘ 𝑛 ) = dom ( 𝐹 ‘ 𝑀 ) )
16	4 13	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ( SMblFn ‘ 𝑆 ) )
17		eqid	⊢ dom ( 𝐹 ‘ 𝑀 ) = dom ( 𝐹 ‘ 𝑀 )
18	3 16 17	smfdmss	⊢ ( 𝜑 → dom ( 𝐹 ‘ 𝑀 ) ⊆ ∪ 𝑆 )
19	13 15 18	iinssd	⊢ ( 𝜑 → ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ⊆ ∪ 𝑆 )
20	10 19	sstrd	⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
21		nfv	⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ 𝐷 )
22	13	ne0d	⊢ ( 𝜑 → 𝑍 ≠ ∅ )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑍 ≠ ∅ )
24	3	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑆 ∈ SAlg )
25	4	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( SMblFn ‘ 𝑆 ) )
26		eqid	⊢ dom ( 𝐹 ‘ 𝑛 ) = dom ( 𝐹 ‘ 𝑛 )
27	24 25 26	smff	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ )
28	27	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ )
29		iinss2	⊢ ( 𝑛 ∈ 𝑍 → ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ⊆ dom ( 𝐹 ‘ 𝑛 ) )
30	29	adantl	⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍 ) → ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ⊆ dom ( 𝐹 ‘ 𝑛 ) )
31	9	sseli	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
32	31	adantr	⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
33	30 32	sseldd	⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
34	33	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
35	28 34	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ )
36	5	rabeq2i	⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) )
37	36	simprbi	⊢ ( 𝑥 ∈ 𝐷 → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
38	37	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
39	21 23 35 38	suprclrnmpt	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ∈ ℝ )
40	39 6	fmptd	⊢ ( 𝜑 → 𝐺 : 𝐷 ⟶ ℝ )
41	1	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑀 ∈ ℤ )
42	3	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑆 ∈ SAlg )
43	4	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
44		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ )
45	41 2 42 43 5 6 44	smfsuplem2	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ◡ 𝐺 “ ( -∞ (,] 𝑎 ) ) ∈ ( 𝑆 ↾t 𝐷 ) )
46	7 3 20 40 45	issmfle2d	⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )