Theorem hashunsng

Description: The size of the union of a finite set with a disjoint singleton is one more than the size of the set. (Contributed by Paul Chapman, 30-Nov-2012)

	Ref	Expression
Assertion	hashunsng	$$⊢B\in V\to \left(\left(A\in \mathrm{Fin}\wedge \neg B\in A\right)\to \left|A\cup \left\{B\right\}\right|=\left|A\right|+1\right)$$

Proof

Step	Hyp	Ref	Expression
1		disjsn	$$⊢A\cap \left\{B\right\}=\varnothing \leftrightarrow \neg B\in A$$
2		snfi	$$⊢\left\{B\right\}\in \mathrm{Fin}$$
3		hashun	$$⊢\left(A\in \mathrm{Fin}\wedge \left\{B\right\}\in \mathrm{Fin}\wedge A\cap \left\{B\right\}=\varnothing \right)\to \left|A\cup \left\{B\right\}\right|=\left|A\right|+\left|\left\{B\right\}\right|$$
4	2 3	mp3an2	$$⊢\left(A\in \mathrm{Fin}\wedge A\cap \left\{B\right\}=\varnothing \right)\to \left|A\cup \left\{B\right\}\right|=\left|A\right|+\left|\left\{B\right\}\right|$$
5	1 4	sylan2br	$$⊢\left(A\in \mathrm{Fin}\wedge \neg B\in A\right)\to \left|A\cup \left\{B\right\}\right|=\left|A\right|+\left|\left\{B\right\}\right|$$
6		hashsng	$$⊢B\in V\to \left|\left\{B\right\}\right|=1$$
7	6	oveq2d	$$⊢B\in V\to \left|A\right|+\left|\left\{B\right\}\right|=\left|A\right|+1$$
8	5 7	sylan9eq	$$⊢\left(\left(A\in \mathrm{Fin}\wedge \neg B\in A\right)\wedge B\in V\right)\to \left|A\cup \left\{B\right\}\right|=\left|A\right|+1$$
9	8	expcom	$$⊢B\in V\to \left(\left(A\in \mathrm{Fin}\wedge \neg B\in A\right)\to \left|A\cup \left\{B\right\}\right|=\left|A\right|+1\right)$$