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	sseldi	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ( 𝐾 ‘ 𝑝 ) ) → 𝑞 ∈ ℝ )
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 ( 𝐴 ∩ 𝐶 ) ) )