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	|- F/ x ph
	adddmmbl.2	|- F/_ x A
	adddmmbl.3	|- F/_ x B
	adddmmbl.4	|- ( ph -> S e. SAlg )
	adddmmbl.5	|- ( ph -> A e. S )
	adddmmbl.6	|- ( ph -> B e. S )
Assertion	adddmmbl	|- ( ph -> dom ( x e. ( A i^i B ) |-> ( C + D ) ) e. S )

Proof

Step	Hyp	Ref	Expression
1		adddmmbl.1	|- F/ x ph
2		adddmmbl.2	|- F/_ x A
3		adddmmbl.3	|- F/_ x B
4		adddmmbl.4	|- ( ph -> S e. SAlg )
5		adddmmbl.5	|- ( ph -> A e. S )
6		adddmmbl.6	|- ( ph -> B e. S )
7	2 3	nfin	|- F/_ x ( A i^i B )
8		eqid	|- ( x e. ( A i^i B ) |-> ( C + D ) ) = ( x e. ( A i^i B ) |-> ( C + D ) )
9		ovexd	|- ( ( ph /\ x e. ( A i^i B ) ) -> ( C + D ) e. _V )
10	1 7 8 9	dmmptdff	|- ( ph -> dom ( x e. ( A i^i B ) |-> ( C + D ) ) = ( A i^i B ) )
11	4 5 6	salincld	|- ( ph -> ( A i^i B ) e. S )
12	10 11	eqeltrd	|- ( ph -> dom ( x e. ( A i^i B ) |-> ( C + D ) ) e. S )