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	$⊢ (1_{𝑜} ⊔︀ 1_{𝑜}) \approx 2_{𝑜}$

Proof

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

Metamath Proof Explorer

Theorem dju1p1e2

Proof