Theorem dju1p1e2

Description: 1+1=2 for cardinal number addition, derived from pm54.43 as promised. Theorem *110.643 ofPrincipia Mathematica, vol. II, p. 86, which adds the remark, "The above proposition is occasionally useful." Whitehead and Russell define cardinal addition on collections of all sets equinumerous to 1 and 2 (which for us are proper classes unless we restrict them as in karden ), but after applying definitions, our theorem is equivalent. Because we use a disjoint union for cardinal addition (as explained in the comment at the top of this section), we use ~ instead of =. See dju1p1e2ALT for a shorter proof that doesn't use pm54.43 . (Contributed by NM, 5-Apr-2007) (Proof modification is discouraged.)

	Ref	Expression
Assertion	dju1p1e2	$$⊢\left(1_{𝑜}\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx 2_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		df-dju	$$⊢\left(1_{𝑜}\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)=\left(\left\{\varnothing \right\}\times 1_{𝑜}\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)$$
2		xp01disjl	$$⊢\left(\left\{\varnothing \right\}\times 1_{𝑜}\right)\cap \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)=\varnothing$$
3		0ex	$$⊢\varnothing \in \mathrm{V}$$
4		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
5		xpsnen2g	$$⊢\left(\varnothing \in \mathrm{V}\wedge 1_{𝑜}\in \mathrm{On}\right)\to \left(\left\{\varnothing \right\}\times 1_{𝑜}\right)\approx 1_{𝑜}$$
6	3 4 5	mp2an	$$⊢\left(\left\{\varnothing \right\}\times 1_{𝑜}\right)\approx 1_{𝑜}$$
7		xpsnen2g	$$⊢\left(1_{𝑜}\in \mathrm{On}\wedge 1_{𝑜}\in \mathrm{On}\right)\to \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\approx 1_{𝑜}$$
8	4 4 7	mp2an	$$⊢\left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\approx 1_{𝑜}$$
9		pm54.43	$$⊢\left(\left(\left\{\varnothing \right\}\times 1_{𝑜}\right)\approx 1_{𝑜}\wedge \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\approx 1_{𝑜}\right)\to \left(\left(\left\{\varnothing \right\}\times 1_{𝑜}\right)\cap \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)=\varnothing \leftrightarrow \left(\left(\left\{\varnothing \right\}\times 1_{𝑜}\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\right)\approx 2_{𝑜}\right)$$
10	6 8 9	mp2an	$$⊢\left(\left\{\varnothing \right\}\times 1_{𝑜}\right)\cap \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)=\varnothing \leftrightarrow \left(\left(\left\{\varnothing \right\}\times 1_{𝑜}\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\right)\approx 2_{𝑜}$$
11	2 10	mpbi	$$⊢\left(\left(\left\{\varnothing \right\}\times 1_{𝑜}\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\right)\approx 2_{𝑜}$$
12	1 11	eqbrtri	$$⊢\left(1_{𝑜}\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx 2_{𝑜}$$