Theorem smfsuplem2

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

Proof

Step	Hyp	Ref	Expression
1		smfsuplem2.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		smfsuplem2.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		smfsuplem2.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		smfsuplem2.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
5		smfsuplem2.d	⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 }
6		smfsuplem2.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
7		smfsuplem2.8	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
8		nfcv	⊢ Ⅎ 𝑛 𝐹
9		eqid	⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
10		eqid	⊢ ( SalGen ‘ ( topGen ‘ ran (,) ) ) = ( SalGen ‘ ( topGen ‘ ran (,) ) )
11		mnfxr	⊢ -∞ ∈ ℝ*
12	11	a1i	⊢ ( 𝜑 → -∞ ∈ ℝ* )
13	12 7 9 10	iocborel	⊢ ( 𝜑 → ( -∞ (,] 𝐴 ) ∈ ( SalGen ‘ ( topGen ‘ ran (,) ) ) )
14	8 2 3 4 9 10 13	smfpimcc	⊢ ( 𝜑 → ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )
15	1	adantr	⊢ ( ( 𝜑 ∧ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) ) → 𝑀 ∈ ℤ )
16	3	adantr	⊢ ( ( 𝜑 ∧ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) ) → 𝑆 ∈ SAlg )
17	4	adantr	⊢ ( ( 𝜑 ∧ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) ) → 𝐹 : 𝑍 ⟶ ( SMblFn ‘ 𝑆 ) )
18		fveq2	⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑚 ) )
19	18	dmeqd	⊢ ( 𝑛 = 𝑚 → dom ( 𝐹 ‘ 𝑛 ) = dom ( 𝐹 ‘ 𝑚 ) )
20	19	cbviinv	⊢ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) = ∩ 𝑚 ∈ 𝑍 dom ( 𝐹 ‘ 𝑚 )
21	20	a1i	⊢ ( 𝑥 = 𝑤 → ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) = ∩ 𝑚 ∈ 𝑍 dom ( 𝐹 ‘ 𝑚 ) )
22		fveq2	⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) )
23	22	breq1d	⊢ ( 𝑥 = 𝑤 → ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ↔ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ≤ 𝑦 ) )
24	23	ralbidv	⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ↔ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ≤ 𝑦 ) )
25	18	fveq1d	⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
26	25	breq1d	⊢ ( 𝑛 = 𝑚 → ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ≤ 𝑦 ↔ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ≤ 𝑦 ) )
27	26	cbvralvw	⊢ ( ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ≤ 𝑦 ↔ ∀ 𝑚 ∈ 𝑍 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ≤ 𝑦 )
28	27	a1i	⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ≤ 𝑦 ↔ ∀ 𝑚 ∈ 𝑍 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ≤ 𝑦 ) )
29	24 28	bitrd	⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ↔ ∀ 𝑚 ∈ 𝑍 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ≤ 𝑦 ) )
30	29	rexbidv	⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑚 ∈ 𝑍 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ≤ 𝑦 ) )
31	21 30	cbvrabv2w	⊢ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 } = { 𝑤 ∈ ∩ 𝑚 ∈ 𝑍 dom ( 𝐹 ‘ 𝑚 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑚 ∈ 𝑍 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ≤ 𝑦 }
32	5 31	eqtri	⊢ 𝐷 = { 𝑤 ∈ ∩ 𝑚 ∈ 𝑍 dom ( 𝐹 ‘ 𝑚 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑚 ∈ 𝑍 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ≤ 𝑦 }
33	22	mpteq2dv	⊢ ( 𝑥 = 𝑤 → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) )
34	25	cbvmptv	⊢ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) )
35	34	a1i	⊢ ( 𝑥 = 𝑤 → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑤 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
36	33 35	eqtrd	⊢ ( 𝑥 = 𝑤 → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
37	36	rneqd	⊢ ( 𝑥 = 𝑤 → ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) = ran ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) )
38	37	supeq1d	⊢ ( 𝑥 = 𝑤 → sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) = sup ( ran ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) , ℝ , < ) )
39	38	cbvmptv	⊢ ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ) = ( 𝑤 ∈ 𝐷 ↦ sup ( ran ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) , ℝ , < ) )
40	6 39	eqtri	⊢ 𝐺 = ( 𝑤 ∈ 𝐷 ↦ sup ( ran ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑤 ) ) , ℝ , < ) )
41	7	adantr	⊢ ( ( 𝜑 ∧ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) ) → 𝐴 ∈ ℝ )
42		simprl	⊢ ( ( 𝜑 ∧ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) ) → ℎ : 𝑍 ⟶ 𝑆 )
43		simplrr	⊢ ( ( ( 𝜑 ∧ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) ) ∧ 𝑚 ∈ 𝑍 ) → ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) )
44	18	cnveqd	⊢ ( 𝑛 = 𝑚 → ◡ ( 𝐹 ‘ 𝑛 ) = ◡ ( 𝐹 ‘ 𝑚 ) )
45	44	imaeq1d	⊢ ( 𝑛 = 𝑚 → ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ◡ ( 𝐹 ‘ 𝑚 ) “ ( -∞ (,] 𝐴 ) ) )
46		fveq2	⊢ ( 𝑛 = 𝑚 → ( ℎ ‘ 𝑛 ) = ( ℎ ‘ 𝑚 ) )
47	46 19	ineq12d	⊢ ( 𝑛 = 𝑚 → ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) )
48	45 47	eqeq12d	⊢ ( 𝑛 = 𝑚 → ( ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ↔ ( ◡ ( 𝐹 ‘ 𝑚 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) ) )
49	48	rspccva	⊢ ( ( ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑚 ∈ 𝑍 ) → ( ◡ ( 𝐹 ‘ 𝑚 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) )
50	43 49	sylancom	⊢ ( ( ( 𝜑 ∧ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) ) ∧ 𝑚 ∈ 𝑍 ) → ( ◡ ( 𝐹 ‘ 𝑚 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑚 ) ∩ dom ( 𝐹 ‘ 𝑚 ) ) )
51	15 2 16 17 32 40 41 42 50	smfsuplem1	⊢ ( ( 𝜑 ∧ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) ) → ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ∈ ( 𝑆 ↾t 𝐷 ) )
52	51	ex	⊢ ( 𝜑 → ( ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) → ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
53	52	exlimdv	⊢ ( 𝜑 → ( ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ ( -∞ (,] 𝐴 ) ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) → ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
54	14 53	mpd	⊢ ( 𝜑 → ( ◡ 𝐺 “ ( -∞ (,] 𝐴 ) ) ∈ ( 𝑆 ↾t 𝐷 ) )