Theorem ovnsubadd2

Description: ( voln*X ) is subadditive. Proposition 115D (a)(iv) of Fremlin1 p. 31 . The special case of the union of 2 sets. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovnsubadd2.x	$$⊢\phi \to X\in \mathrm{Fin}$$
	ovnsubadd2.a	$$⊢\phi \to A\subseteq {ℝ}^X$$
	ovnsubadd2.b	$$⊢\phi \to B\subseteq {ℝ}^X$$
Assertion	ovnsubadd2	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(A\cup B\right)\le \mathrm{voln*}\left(X\right)\left(A\right){+}_{𝑒}\mathrm{voln*}\left(X\right)\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ovnsubadd2.x	$$⊢\phi \to X\in \mathrm{Fin}$$
2		ovnsubadd2.a	$$⊢\phi \to A\subseteq {ℝ}^X$$
3		ovnsubadd2.b	$$⊢\phi \to B\subseteq {ℝ}^X$$
4		eqeq1	$$⊢m=n\to \left(m=1\leftrightarrow n=1\right)$$
5		eqeq1	$$⊢m=n\to \left(m=2\leftrightarrow n=2\right)$$
6	5	ifbid	$$⊢m=n\to if\left(m=2,B,\varnothing \right)=if\left(n=2,B,\varnothing \right)$$
7	4 6	ifbieq2d	$$⊢m=n\to if\left(m=1,A,if\left(m=2,B,\varnothing \right)\right)=if\left(n=1,A,if\left(n=2,B,\varnothing \right)\right)$$
8	7	cbvmptv	$$⊢\left(m\in \mathbb{N}⟼if\left(m=1,A,if\left(m=2,B,\varnothing \right)\right)\right)=\left(n\in \mathbb{N}⟼if\left(n=1,A,if\left(n=2,B,\varnothing \right)\right)\right)$$
9	1 2 3 8	ovnsubadd2lem	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(A\cup B\right)\le \mathrm{voln*}\left(X\right)\left(A\right){+}_{𝑒}\mathrm{voln*}\left(X\right)\left(B\right)$$