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	$⊢ Ⅎ x φ$
	smfaddlem2.s	$⊢ φ \to S \in SAlg$
	smfaddlem2.a	$⊢ φ \to A \in V$
	smfaddlem2.b	$⊢ (φ \land x \in A) \to B \in ℝ$
	smfaddlem2.d	$⊢ (φ \land x \in C) \to D \in ℝ$
	smfaddlem2.m	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
	smfaddlem2.7	$⊢ φ \to (x \in C ⟼ D) \in SMblFn (S)$
	smfaddlem2.r	$⊢ φ \to R \in ℝ$
	smfaddlem2.k	$⊢ K = (p \in ℚ ⟼ \{q \in ℚ \| p + q < R\})$
Assertion	smfaddlem2	$⊢ φ \to \{x \in (A \cap C) \| B + D < R\} \in (S ↾_{𝑡} (A \cap C))$

Proof

Step	Hyp	Ref	Expression
1		smfaddlem2.x	$⊢ Ⅎ x φ$
2		smfaddlem2.s	$⊢ φ \to S \in SAlg$
3		smfaddlem2.a	$⊢ φ \to A \in V$
4		smfaddlem2.b	$⊢ (φ \land x \in A) \to B \in ℝ$
5		smfaddlem2.d	$⊢ (φ \land x \in C) \to D \in ℝ$
6		smfaddlem2.m	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
7		smfaddlem2.7	$⊢ φ \to (x \in C ⟼ D) \in SMblFn (S)$
8		smfaddlem2.r	$⊢ φ \to R \in ℝ$
9		smfaddlem2.k	$⊢ K = (p \in ℚ ⟼ \{q \in ℚ \| p + q < R\})$
10	1 4 5 8 9	smfaddlem1	$⊢ φ \to \{x \in (A \cap C) \| B + D < R\} = ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\}$
11		elinel1	$⊢ x \in (A \cap C) \to x \in A$
12	11	adantl	$⊢ (φ \land x \in (A \cap C)) \to x \in A$
13	1 12	ssdf	$⊢ φ \to A \cap C \subseteq A$
14	3 13	ssexd	$⊢ φ \to A \cap C \in V$
15		eqid	$⊢ S ↾_{𝑡} (A \cap C) = S ↾_{𝑡} (A \cap C)$
16	2 14 15	subsalsal	$⊢ φ \to S ↾_{𝑡} (A \cap C) \in SAlg$
17		qct	$⊢ ℚ ≼ ω$
18	17	a1i	$⊢ φ \to ℚ ≼ ω$
19	16	adantr	$⊢ (φ \land p \in ℚ) \to S ↾_{𝑡} (A \cap C) \in SAlg$
20		qex	$⊢ ℚ \in V$
21	20	a1i	$⊢ (φ \land p \in ℚ) \to ℚ \in V$
22	9	a1i	$⊢ φ \to K = (p \in ℚ ⟼ \{q \in ℚ \| p + q < R\})$
23	20	rabex	$⊢ \{q \in ℚ \| p + q < R\} \in V$
24	23	a1i	$⊢ (φ \land p \in ℚ) \to \{q \in ℚ \| p + q < R\} \in V$
25	22 24	fvmpt2d	$⊢ (φ \land p \in ℚ) \to K (p) = \{q \in ℚ \| p + q < R\}$
26		ssrab2	$⊢ \{q \in ℚ \| p + q < R\} \subseteq ℚ$
27	25 26	eqsstrdi	$⊢ (φ \land p \in ℚ) \to K (p) \subseteq ℚ$
28		ssdomg	$⊢ ℚ \in V \to (K (p) \subseteq ℚ \to K (p) ≼ ℚ)$
29	21 27 28	sylc	$⊢ (φ \land p \in ℚ) \to K (p) ≼ ℚ$
30	17	a1i	$⊢ (φ \land p \in ℚ) \to ℚ ≼ ω$
31		domtr	$⊢ (K (p) ≼ ℚ \land ℚ ≼ ω) \to K (p) ≼ ω$
32	29 30 31	syl2anc	$⊢ (φ \land p \in ℚ) \to K (p) ≼ ω$
33		inrab	$⊢ \{x \in (A \cap C) \| B < p\} \cap \{x \in (A \cap C) \| D < q\} = \{x \in (A \cap C) \| (B < p \land D < q)\}$
34	16	ad2antrr	$⊢ ((φ \land p \in ℚ) \land q \in K (p)) \to S ↾_{𝑡} (A \cap C) \in SAlg$
35		nfv	$⊢ Ⅎ x p \in ℚ$
36	1 35	nfan	$⊢ Ⅎ x (φ \land p \in ℚ)$
37		nfv	$⊢ Ⅎ x q \in K (p)$
38	36 37	nfan	$⊢ Ⅎ x ((φ \land p \in ℚ) \land q \in K (p))$
39	2	ad2antrr	$⊢ ((φ \land p \in ℚ) \land q \in K (p)) \to S \in SAlg$
40	12 4	syldan	$⊢ (φ \land x \in (A \cap C)) \to B \in ℝ$
41	40	ad4ant14	$⊢ (((φ \land p \in ℚ) \land q \in K (p)) \land x \in (A \cap C)) \to B \in ℝ$
42	2 6 13	sssmfmpt	$⊢ φ \to (x \in (A \cap C) ⟼ B) \in SMblFn (S)$
43	42	ad2antrr	$⊢ ((φ \land p \in ℚ) \land q \in K (p)) \to (x \in (A \cap C) ⟼ B) \in SMblFn (S)$
44		qre	$⊢ p \in ℚ \to p \in ℝ$
45	44	ad2antlr	$⊢ ((φ \land p \in ℚ) \land q \in K (p)) \to p \in ℝ$
46	38 39 41 43 45	smfpimltmpt	$⊢ ((φ \land p \in ℚ) \land q \in K (p)) \to \{x \in (A \cap C) \| B < p\} \in (S ↾_{𝑡} (A \cap C))$
47		elinel2	$⊢ x \in (A \cap C) \to x \in C$
48	47	adantl	$⊢ (φ \land x \in (A \cap C)) \to x \in C$
49	48 5	syldan	$⊢ (φ \land x \in (A \cap C)) \to D \in ℝ$
50	49	ad4ant14	$⊢ (((φ \land p \in ℚ) \land q \in K (p)) \land x \in (A \cap C)) \to D \in ℝ$
51	1 48	ssdf	$⊢ φ \to A \cap C \subseteq C$
52	2 7 51	sssmfmpt	$⊢ φ \to (x \in (A \cap C) ⟼ D) \in SMblFn (S)$
53	52	ad2antrr	$⊢ ((φ \land p \in ℚ) \land q \in K (p)) \to (x \in (A \cap C) ⟼ D) \in SMblFn (S)$
54	44	ssriv	$⊢ ℚ \subseteq ℝ$
55	27	sselda	$⊢ ((φ \land p \in ℚ) \land q \in K (p)) \to q \in ℚ$
56	54 55	sseldi	$⊢ ((φ \land p \in ℚ) \land q \in K (p)) \to q \in ℝ$
57	38 39 50 53 56	smfpimltmpt	$⊢ ((φ \land p \in ℚ) \land q \in K (p)) \to \{x \in (A \cap C) \| D < q\} \in (S ↾_{𝑡} (A \cap C))$
58	34 46 57	salincld	$⊢ ((φ \land p \in ℚ) \land q \in K (p)) \to \{x \in (A \cap C) \| B < p\} \cap \{x \in (A \cap C) \| D < q\} \in (S ↾_{𝑡} (A \cap C))$
59	33 58	eqeltrrid	$⊢ ((φ \land p \in ℚ) \land q \in K (p)) \to \{x \in (A \cap C) \| (B < p \land D < q)\} \in (S ↾_{𝑡} (A \cap C))$
60	19 32 59	saliuncl	$⊢ (φ \land p \in ℚ) \to ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\} \in (S ↾_{𝑡} (A \cap C))$
61	16 18 60	saliuncl	$⊢ φ \to ⋃_{p \in ℚ} ⋃_{q \in K (p)} \{x \in (A \cap C) \| (B < p \land D < q)\} \in (S ↾_{𝑡} (A \cap C))$
62	10 61	eqeltrd	$⊢ φ \to \{x \in (A \cap C) \| B + D < R\} \in (S ↾_{𝑡} (A \cap C))$

Metamath Proof Explorer

Theorem smfaddlem2

Proof