Theorem hashunsngx

Description: The size of the union of a set with a disjoint singleton is the extended real addition of the size of the set and 1, analogous to hashunsng . (Contributed by BTernaryTau, 9-Sep-2023)

	Ref	Expression
Assertion	hashunsngx	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\neg B\in A\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		hashunx	$$⊢\left(A\in V\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 V\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 V\wedge \neg B\in A\right)\to \left|A\cup \left\{B\right\}\right|=\left|A\right|{+}_{𝑒}\left|\left\{B\right\}\right|$$
6	5	3adant2	$$⊢\left(A\in V\wedge B\in W\wedge \neg B\in A\right)\to \left|A\cup \left\{B\right\}\right|=\left|A\right|{+}_{𝑒}\left|\left\{B\right\}\right|$$
7		hashsng	$$⊢B\in W\to \left|\left\{B\right\}\right|=1$$
8	7	3ad2ant2	$$⊢\left(A\in V\wedge B\in W\wedge \neg B\in A\right)\to \left|\left\{B\right\}\right|=1$$
9	8	oveq2d	$$⊢\left(A\in V\wedge B\in W\wedge \neg B\in A\right)\to \left|A\right|{+}_{𝑒}\left|\left\{B\right\}\right|=\left|A\right|{+}_{𝑒}1$$
10	6 9	eqtrd	$$⊢\left(A\in V\wedge B\in W\wedge \neg B\in A\right)\to \left|A\cup \left\{B\right\}\right|=\left|A\right|{+}_{𝑒}1$$
11	10	3expia	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\neg B\in A\to \left|A\cup \left\{B\right\}\right|=\left|A\right|{+}_{𝑒}1\right)$$