Metamath Proof Explorer


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 ffvelrnda ( ( 𝜑𝑛𝑍 ) → ( 𝐹𝑛 ) ∈ ( 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 ffvelrnd ( ( ( 𝜑𝑥 𝑛𝑍 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 ffvelrnd ( ( ( 𝜑𝑥𝐷 ) ∧ 𝑛𝑍 ) → ( ( 𝐹𝑛 ) ‘ 𝑥 ) ∈ ℝ )
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 ‘ 𝑆 ) )