Metamath Proof Explorer


Theorem smfaddlem2

Description: The sum of two sigma-measurable functions is measurable. Proposition 121E (b) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfaddlem2.x 𝑥 𝜑
smfaddlem2.s ( 𝜑𝑆 ∈ SAlg )
smfaddlem2.a ( 𝜑𝐴𝑉 )
smfaddlem2.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
smfaddlem2.d ( ( 𝜑𝑥𝐶 ) → 𝐷 ∈ ℝ )
smfaddlem2.m ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
smfaddlem2.7 ( 𝜑 → ( 𝑥𝐶𝐷 ) ∈ ( SMblFn ‘ 𝑆 ) )
smfaddlem2.r ( 𝜑𝑅 ∈ ℝ )
smfaddlem2.k 𝐾 = ( 𝑝 ∈ ℚ ↦ { 𝑞 ∈ ℚ ∣ ( 𝑝 + 𝑞 ) < 𝑅 } )
Assertion smfaddlem2 ( 𝜑 → { 𝑥 ∈ ( 𝐴𝐶 ) ∣ ( 𝐵 + 𝐷 ) < 𝑅 } ∈ ( 𝑆t ( 𝐴𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 smfaddlem2.x 𝑥 𝜑
2 smfaddlem2.s ( 𝜑𝑆 ∈ SAlg )
3 smfaddlem2.a ( 𝜑𝐴𝑉 )
4 smfaddlem2.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
5 smfaddlem2.d ( ( 𝜑𝑥𝐶 ) → 𝐷 ∈ ℝ )
6 smfaddlem2.m ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
7 smfaddlem2.7 ( 𝜑 → ( 𝑥𝐶𝐷 ) ∈ ( SMblFn ‘ 𝑆 ) )
8 smfaddlem2.r ( 𝜑𝑅 ∈ ℝ )
9 smfaddlem2.k 𝐾 = ( 𝑝 ∈ ℚ ↦ { 𝑞 ∈ ℚ ∣ ( 𝑝 + 𝑞 ) < 𝑅 } )
10 1 4 5 8 9 smfaddlem1 ( 𝜑 → { 𝑥 ∈ ( 𝐴𝐶 ) ∣ ( 𝐵 + 𝐷 ) < 𝑅 } = 𝑝 ∈ ℚ 𝑞 ∈ ( 𝐾𝑝 ) { 𝑥 ∈ ( 𝐴𝐶 ) ∣ ( 𝐵 < 𝑝𝐷 < 𝑞 ) } )
11 elinel1 ( 𝑥 ∈ ( 𝐴𝐶 ) → 𝑥𝐴 )
12 11 adantl ( ( 𝜑𝑥 ∈ ( 𝐴𝐶 ) ) → 𝑥𝐴 )
13 1 12 ssdf ( 𝜑 → ( 𝐴𝐶 ) ⊆ 𝐴 )
14 3 13 ssexd ( 𝜑 → ( 𝐴𝐶 ) ∈ V )
15 eqid ( 𝑆t ( 𝐴𝐶 ) ) = ( 𝑆t ( 𝐴𝐶 ) )
16 2 14 15 subsalsal ( 𝜑 → ( 𝑆t ( 𝐴𝐶 ) ) ∈ SAlg )
17 qct ℚ ≼ ω
18 17 a1i ( 𝜑 → ℚ ≼ ω )
19 16 adantr ( ( 𝜑𝑝 ∈ ℚ ) → ( 𝑆t ( 𝐴𝐶 ) ) ∈ SAlg )
20 qex ℚ ∈ V
21 20 a1i ( ( 𝜑𝑝 ∈ ℚ ) → ℚ ∈ V )
22 9 a1i ( 𝜑𝐾 = ( 𝑝 ∈ ℚ ↦ { 𝑞 ∈ ℚ ∣ ( 𝑝 + 𝑞 ) < 𝑅 } ) )
23 20 rabex { 𝑞 ∈ ℚ ∣ ( 𝑝 + 𝑞 ) < 𝑅 } ∈ V
24 23 a1i ( ( 𝜑𝑝 ∈ ℚ ) → { 𝑞 ∈ ℚ ∣ ( 𝑝 + 𝑞 ) < 𝑅 } ∈ V )
25 22 24 fvmpt2d ( ( 𝜑𝑝 ∈ ℚ ) → ( 𝐾𝑝 ) = { 𝑞 ∈ ℚ ∣ ( 𝑝 + 𝑞 ) < 𝑅 } )
26 ssrab2 { 𝑞 ∈ ℚ ∣ ( 𝑝 + 𝑞 ) < 𝑅 } ⊆ ℚ
27 25 26 eqsstrdi ( ( 𝜑𝑝 ∈ ℚ ) → ( 𝐾𝑝 ) ⊆ ℚ )
28 ssdomg ( ℚ ∈ V → ( ( 𝐾𝑝 ) ⊆ ℚ → ( 𝐾𝑝 ) ≼ ℚ ) )
29 21 27 28 sylc ( ( 𝜑𝑝 ∈ ℚ ) → ( 𝐾𝑝 ) ≼ ℚ )
30 17 a1i ( ( 𝜑𝑝 ∈ ℚ ) → ℚ ≼ ω )
31 domtr ( ( ( 𝐾𝑝 ) ≼ ℚ ∧ ℚ ≼ ω ) → ( 𝐾𝑝 ) ≼ ω )
32 29 30 31 syl2anc ( ( 𝜑𝑝 ∈ ℚ ) → ( 𝐾𝑝 ) ≼ ω )
33 inrab ( { 𝑥 ∈ ( 𝐴𝐶 ) ∣ 𝐵 < 𝑝 } ∩ { 𝑥 ∈ ( 𝐴𝐶 ) ∣ 𝐷 < 𝑞 } ) = { 𝑥 ∈ ( 𝐴𝐶 ) ∣ ( 𝐵 < 𝑝𝐷 < 𝑞 ) }
34 16 ad2antrr ( ( ( 𝜑𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ( 𝐾𝑝 ) ) → ( 𝑆t ( 𝐴𝐶 ) ) ∈ SAlg )
35 nfv 𝑥 𝑝 ∈ ℚ
36 1 35 nfan 𝑥 ( 𝜑𝑝 ∈ ℚ )
37 nfv 𝑥 𝑞 ∈ ( 𝐾𝑝 )
38 36 37 nfan 𝑥 ( ( 𝜑𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ( 𝐾𝑝 ) )
39 2 ad2antrr ( ( ( 𝜑𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ( 𝐾𝑝 ) ) → 𝑆 ∈ SAlg )
40 12 4 syldan ( ( 𝜑𝑥 ∈ ( 𝐴𝐶 ) ) → 𝐵 ∈ ℝ )
41 40 ad4ant14 ( ( ( ( 𝜑𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ( 𝐾𝑝 ) ) ∧ 𝑥 ∈ ( 𝐴𝐶 ) ) → 𝐵 ∈ ℝ )
42 2 6 13 sssmfmpt ( 𝜑 → ( 𝑥 ∈ ( 𝐴𝐶 ) ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
43 42 ad2antrr ( ( ( 𝜑𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ( 𝐾𝑝 ) ) → ( 𝑥 ∈ ( 𝐴𝐶 ) ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
44 qre ( 𝑝 ∈ ℚ → 𝑝 ∈ ℝ )
45 44 ad2antlr ( ( ( 𝜑𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ( 𝐾𝑝 ) ) → 𝑝 ∈ ℝ )
46 38 39 41 43 45 smfpimltmpt ( ( ( 𝜑𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ( 𝐾𝑝 ) ) → { 𝑥 ∈ ( 𝐴𝐶 ) ∣ 𝐵 < 𝑝 } ∈ ( 𝑆t ( 𝐴𝐶 ) ) )
47 elinel2 ( 𝑥 ∈ ( 𝐴𝐶 ) → 𝑥𝐶 )
48 47 adantl ( ( 𝜑𝑥 ∈ ( 𝐴𝐶 ) ) → 𝑥𝐶 )
49 48 5 syldan ( ( 𝜑𝑥 ∈ ( 𝐴𝐶 ) ) → 𝐷 ∈ ℝ )
50 49 ad4ant14 ( ( ( ( 𝜑𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ( 𝐾𝑝 ) ) ∧ 𝑥 ∈ ( 𝐴𝐶 ) ) → 𝐷 ∈ ℝ )
51 1 48 ssdf ( 𝜑 → ( 𝐴𝐶 ) ⊆ 𝐶 )
52 2 7 51 sssmfmpt ( 𝜑 → ( 𝑥 ∈ ( 𝐴𝐶 ) ↦ 𝐷 ) ∈ ( SMblFn ‘ 𝑆 ) )
53 52 ad2antrr ( ( ( 𝜑𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ( 𝐾𝑝 ) ) → ( 𝑥 ∈ ( 𝐴𝐶 ) ↦ 𝐷 ) ∈ ( SMblFn ‘ 𝑆 ) )
54 44 ssriv ℚ ⊆ ℝ
55 27 sselda ( ( ( 𝜑𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ( 𝐾𝑝 ) ) → 𝑞 ∈ ℚ )
56 54 55 sselid ( ( ( 𝜑𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ( 𝐾𝑝 ) ) → 𝑞 ∈ ℝ )
57 38 39 50 53 56 smfpimltmpt ( ( ( 𝜑𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ( 𝐾𝑝 ) ) → { 𝑥 ∈ ( 𝐴𝐶 ) ∣ 𝐷 < 𝑞 } ∈ ( 𝑆t ( 𝐴𝐶 ) ) )
58 34 46 57 salincld ( ( ( 𝜑𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ( 𝐾𝑝 ) ) → ( { 𝑥 ∈ ( 𝐴𝐶 ) ∣ 𝐵 < 𝑝 } ∩ { 𝑥 ∈ ( 𝐴𝐶 ) ∣ 𝐷 < 𝑞 } ) ∈ ( 𝑆t ( 𝐴𝐶 ) ) )
59 33 58 eqeltrrid ( ( ( 𝜑𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ( 𝐾𝑝 ) ) → { 𝑥 ∈ ( 𝐴𝐶 ) ∣ ( 𝐵 < 𝑝𝐷 < 𝑞 ) } ∈ ( 𝑆t ( 𝐴𝐶 ) ) )
60 19 32 59 saliuncl ( ( 𝜑𝑝 ∈ ℚ ) → 𝑞 ∈ ( 𝐾𝑝 ) { 𝑥 ∈ ( 𝐴𝐶 ) ∣ ( 𝐵 < 𝑝𝐷 < 𝑞 ) } ∈ ( 𝑆t ( 𝐴𝐶 ) ) )
61 16 18 60 saliuncl ( 𝜑 𝑝 ∈ ℚ 𝑞 ∈ ( 𝐾𝑝 ) { 𝑥 ∈ ( 𝐴𝐶 ) ∣ ( 𝐵 < 𝑝𝐷 < 𝑞 ) } ∈ ( 𝑆t ( 𝐴𝐶 ) ) )
62 10 61 eqeltrd ( 𝜑 → { 𝑥 ∈ ( 𝐴𝐶 ) ∣ ( 𝐵 + 𝐷 ) < 𝑅 } ∈ ( 𝑆t ( 𝐴𝐶 ) ) )