Theorem unsnen

Description: Equinumerosity of a set with a new element added. (Contributed by NM, 7-Nov-2008)

	Ref	Expression
Hypotheses	unsnen.1	$$⊢A\in \mathrm{V}$$
	unsnen.2	$$⊢B\in \mathrm{V}$$
Assertion	unsnen	$$⊢\neg B\in A\to \left(A\cup \left\{B\right\}\right)\approx \mathrm{suc}\mathrm{card}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		unsnen.1	$$⊢A\in \mathrm{V}$$
2		unsnen.2	$$⊢B\in \mathrm{V}$$
3		disjsn	$$⊢A\cap \left\{B\right\}=\varnothing \leftrightarrow \neg B\in A$$
4		cardon	$$⊢\mathrm{card}\left(A\right)\in \mathrm{On}$$
5	4	onordi	$$⊢\mathrm{Ord}\mathrm{card}\left(A\right)$$
6		orddisj	$$⊢\mathrm{Ord}\mathrm{card}\left(A\right)\to \mathrm{card}\left(A\right)\cap \left\{\mathrm{card}\left(A\right)\right\}=\varnothing$$
7	5 6	ax-mp	$$⊢\mathrm{card}\left(A\right)\cap \left\{\mathrm{card}\left(A\right)\right\}=\varnothing$$
8	1	cardid	$$⊢\mathrm{card}\left(A\right)\approx A$$
9	8	ensymi	$$⊢A\approx \mathrm{card}\left(A\right)$$
10		fvex	$$⊢\mathrm{card}\left(A\right)\in \mathrm{V}$$
11		en2sn	$$⊢\left(B\in \mathrm{V}\wedge \mathrm{card}\left(A\right)\in \mathrm{V}\right)\to \left\{B\right\}\approx \left\{\mathrm{card}\left(A\right)\right\}$$
12	2 10 11	mp2an	$$⊢\left\{B\right\}\approx \left\{\mathrm{card}\left(A\right)\right\}$$
13		unen	$$⊢\left(\left(A\approx \mathrm{card}\left(A\right)\wedge \left\{B\right\}\approx \left\{\mathrm{card}\left(A\right)\right\}\right)\wedge \left(A\cap \left\{B\right\}=\varnothing \wedge \mathrm{card}\left(A\right)\cap \left\{\mathrm{card}\left(A\right)\right\}=\varnothing \right)\right)\to \left(A\cup \left\{B\right\}\right)\approx \left(\mathrm{card}\left(A\right)\cup \left\{\mathrm{card}\left(A\right)\right\}\right)$$
14	9 12 13	mpanl12	$$⊢\left(A\cap \left\{B\right\}=\varnothing \wedge \mathrm{card}\left(A\right)\cap \left\{\mathrm{card}\left(A\right)\right\}=\varnothing \right)\to \left(A\cup \left\{B\right\}\right)\approx \left(\mathrm{card}\left(A\right)\cup \left\{\mathrm{card}\left(A\right)\right\}\right)$$
15	7 14	mpan2	$$⊢A\cap \left\{B\right\}=\varnothing \to \left(A\cup \left\{B\right\}\right)\approx \left(\mathrm{card}\left(A\right)\cup \left\{\mathrm{card}\left(A\right)\right\}\right)$$
16	3 15	sylbir	$$⊢\neg B\in A\to \left(A\cup \left\{B\right\}\right)\approx \left(\mathrm{card}\left(A\right)\cup \left\{\mathrm{card}\left(A\right)\right\}\right)$$
17		df-suc	$$⊢\mathrm{suc}\mathrm{card}\left(A\right)=\mathrm{card}\left(A\right)\cup \left\{\mathrm{card}\left(A\right)\right\}$$
18	16 17	breqtrrdi	$$⊢\neg B\in A\to \left(A\cup \left\{B\right\}\right)\approx \mathrm{suc}\mathrm{card}\left(A\right)$$