Theorem adddmmbl

Description: If two functions have domains in the sigma-algebra, the domain of their addition also belongs to the sigma-algebra. This is the first statement of Proposition 121H of Fremlin1, p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their addition. (Contributed by Glauco Siliprandi, 30-Dec-2024)

	Ref	Expression
Hypotheses	adddmmbl.1	$$⊢Ⅎx\phi$$
	adddmmbl.2	$$⊢\underset{\_}{Ⅎ}xA$$
	adddmmbl.3	$$⊢\underset{\_}{Ⅎ}xB$$
	adddmmbl.4	$$⊢\phi \to S\in \mathrm{SAlg}$$
	adddmmbl.5	$$⊢\phi \to A\in S$$
	adddmmbl.6	$$⊢\phi \to B\in S$$
Assertion	adddmmbl	$$⊢\phi \to \mathrm{dom}\left(x\in \left(A\cap B\right)⟼C+D\right)\in S$$

Proof

Step	Hyp	Ref	Expression
1		adddmmbl.1	$$⊢Ⅎx\phi$$
2		adddmmbl.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		adddmmbl.3	$$⊢\underset{\_}{Ⅎ}xB$$
4		adddmmbl.4	$$⊢\phi \to S\in \mathrm{SAlg}$$
5		adddmmbl.5	$$⊢\phi \to A\in S$$
6		adddmmbl.6	$$⊢\phi \to B\in S$$
7	2 3	nfin	$$⊢\underset{\_}{Ⅎ}x\left(A\cap B\right)$$
8		eqid	$$⊢\left(x\in \left(A\cap B\right)⟼C+D\right)=\left(x\in \left(A\cap B\right)⟼C+D\right)$$
9		ovexd	$$⊢\left(\phi \wedge x\in \left(A\cap B\right)\right)\to C+D\in \mathrm{V}$$
10	1 7 8 9	dmmptdff	$$⊢\phi \to \mathrm{dom}\left(x\in \left(A\cap B\right)⟼C+D\right)=A\cap B$$
11	4 5 6	salincld	$$⊢\phi \to A\cap B\in S$$
12	10 11	eqeltrd	$$⊢\phi \to \mathrm{dom}\left(x\in \left(A\cap B\right)⟼C+D\right)\in S$$