Theorem pm54.43

Description: Theorem *54.43 of WhiteheadRussell p. 360. "From this proposition it will follow, when arithmetical addition has been defined, that 1+1=2." See http://en.wikipedia.org/wiki/Principia_Mathematica#Quotations . This theorem states that two sets of cardinality 1 are disjoint iff their union has cardinality 2.

Whitehead and Russell define 1 as the collection of all sets with cardinality 1 (i.e. all singletons; see card1 ), so that their A e. 1 means, in our notation, A e. { x | ( cardx ) = 1o } which is the same as A ~1o by pm54.43lem . We do not have several of their earlier lemmas available (which would otherwise be unused by our different approach to arithmetic), so our proof is longer. (It is also longer because we must show every detail.)

Theorem dju1p1e2 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007)

	Ref	Expression
Assertion	pm54.43	$$⊢\left(A\approx 1_{𝑜}\wedge B\approx 1_{𝑜}\right)\to \left(A\cap B=\varnothing \leftrightarrow \left(A\cup B\right)\approx 2_{𝑜}\right)$$

Proof

Step	Hyp	Ref	Expression
1		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
2	1	ensn1	$$⊢\left\{1_{𝑜}\right\}\approx 1_{𝑜}$$
3	2	ensymi	$$⊢1_{𝑜}\approx \left\{1_{𝑜}\right\}$$
4		entr	$$⊢\left(B\approx 1_{𝑜}\wedge 1_{𝑜}\approx \left\{1_{𝑜}\right\}\right)\to B\approx \left\{1_{𝑜}\right\}$$
5	3 4	mpan2	$$⊢B\approx 1_{𝑜}\to B\approx \left\{1_{𝑜}\right\}$$
6		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
7	6	onirri	$$⊢\neg 1_{𝑜}\in 1_{𝑜}$$
8		disjsn	$$⊢1_{𝑜}\cap \left\{1_{𝑜}\right\}=\varnothing \leftrightarrow \neg 1_{𝑜}\in 1_{𝑜}$$
9	7 8	mpbir	$$⊢1_{𝑜}\cap \left\{1_{𝑜}\right\}=\varnothing$$
10		unen	$$⊢\left(\left(A\approx 1_{𝑜}\wedge B\approx \left\{1_{𝑜}\right\}\right)\wedge \left(A\cap B=\varnothing \wedge 1_{𝑜}\cap \left\{1_{𝑜}\right\}=\varnothing \right)\right)\to \left(A\cup B\right)\approx \left(1_{𝑜}\cup \left\{1_{𝑜}\right\}\right)$$
11	9 10	mpanr2	$$⊢\left(\left(A\approx 1_{𝑜}\wedge B\approx \left\{1_{𝑜}\right\}\right)\wedge A\cap B=\varnothing \right)\to \left(A\cup B\right)\approx \left(1_{𝑜}\cup \left\{1_{𝑜}\right\}\right)$$
12	11	ex	$$⊢\left(A\approx 1_{𝑜}\wedge B\approx \left\{1_{𝑜}\right\}\right)\to \left(A\cap B=\varnothing \to \left(A\cup B\right)\approx \left(1_{𝑜}\cup \left\{1_{𝑜}\right\}\right)\right)$$
13	5 12	sylan2	$$⊢\left(A\approx 1_{𝑜}\wedge B\approx 1_{𝑜}\right)\to \left(A\cap B=\varnothing \to \left(A\cup B\right)\approx \left(1_{𝑜}\cup \left\{1_{𝑜}\right\}\right)\right)$$
14		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
15		df-suc	$$⊢\mathrm{suc}{1}_{𝑜}=1_{𝑜}\cup \left\{1_{𝑜}\right\}$$
16	14 15	eqtri	$$⊢2_{𝑜}=1_{𝑜}\cup \left\{1_{𝑜}\right\}$$
17	16	breq2i	$$⊢\left(A\cup B\right)\approx 2_{𝑜}\leftrightarrow \left(A\cup B\right)\approx \left(1_{𝑜}\cup \left\{1_{𝑜}\right\}\right)$$
18	13 17	syl6ibr	$$⊢\left(A\approx 1_{𝑜}\wedge B\approx 1_{𝑜}\right)\to \left(A\cap B=\varnothing \to \left(A\cup B\right)\approx 2_{𝑜}\right)$$
19		en1	$$⊢A\approx 1_{𝑜}\leftrightarrow \exists xA=\left\{x\right\}$$
20		en1	$$⊢B\approx 1_{𝑜}\leftrightarrow \exists yB=\left\{y\right\}$$
21		sneq	$$⊢x=y\to \left\{x\right\}=\left\{y\right\}$$
22	21	uneq2d	$$⊢x=y\to \left\{x\right\}\cup \left\{x\right\}=\left\{x\right\}\cup \left\{y\right\}$$
23		unidm	$$⊢\left\{x\right\}\cup \left\{x\right\}=\left\{x\right\}$$
24	22 23	eqtr3di	$$⊢x=y\to \left\{x\right\}\cup \left\{y\right\}=\left\{x\right\}$$
25		vex	$$⊢x\in \mathrm{V}$$
26	25	ensn1	$$⊢\left\{x\right\}\approx 1_{𝑜}$$
27		1sdom2	$$⊢1_{𝑜}\prec 2_{𝑜}$$
28		ensdomtr	$$⊢\left(\left\{x\right\}\approx 1_{𝑜}\wedge 1_{𝑜}\prec 2_{𝑜}\right)\to \left\{x\right\}\prec 2_{𝑜}$$
29	26 27 28	mp2an	$$⊢\left\{x\right\}\prec 2_{𝑜}$$
30	24 29	eqbrtrdi	$$⊢x=y\to \left(\left\{x\right\}\cup \left\{y\right\}\right)\prec 2_{𝑜}$$
31		sdomnen	$$⊢\left(\left\{x\right\}\cup \left\{y\right\}\right)\prec 2_{𝑜}\to \neg \left(\left\{x\right\}\cup \left\{y\right\}\right)\approx 2_{𝑜}$$
32	30 31	syl	$$⊢x=y\to \neg \left(\left\{x\right\}\cup \left\{y\right\}\right)\approx 2_{𝑜}$$
33	32	necon2ai	$$⊢\left(\left\{x\right\}\cup \left\{y\right\}\right)\approx 2_{𝑜}\to x\ne y$$
34		disjsn2	$$⊢x\ne y\to \left\{x\right\}\cap \left\{y\right\}=\varnothing$$
35	33 34	syl	$$⊢\left(\left\{x\right\}\cup \left\{y\right\}\right)\approx 2_{𝑜}\to \left\{x\right\}\cap \left\{y\right\}=\varnothing$$
36	35	a1i	$$⊢\left(A=\left\{x\right\}\wedge B=\left\{y\right\}\right)\to \left(\left(\left\{x\right\}\cup \left\{y\right\}\right)\approx 2_{𝑜}\to \left\{x\right\}\cap \left\{y\right\}=\varnothing \right)$$
37		uneq12	$$⊢\left(A=\left\{x\right\}\wedge B=\left\{y\right\}\right)\to A\cup B=\left\{x\right\}\cup \left\{y\right\}$$
38	37	breq1d	$$⊢\left(A=\left\{x\right\}\wedge B=\left\{y\right\}\right)\to \left(\left(A\cup B\right)\approx 2_{𝑜}\leftrightarrow \left(\left\{x\right\}\cup \left\{y\right\}\right)\approx 2_{𝑜}\right)$$
39		ineq12	$$⊢\left(A=\left\{x\right\}\wedge B=\left\{y\right\}\right)\to A\cap B=\left\{x\right\}\cap \left\{y\right\}$$
40	39	eqeq1d	$$⊢\left(A=\left\{x\right\}\wedge B=\left\{y\right\}\right)\to \left(A\cap B=\varnothing \leftrightarrow \left\{x\right\}\cap \left\{y\right\}=\varnothing \right)$$
41	36 38 40	3imtr4d	$$⊢\left(A=\left\{x\right\}\wedge B=\left\{y\right\}\right)\to \left(\left(A\cup B\right)\approx 2_{𝑜}\to A\cap B=\varnothing \right)$$
42	41	ex	$$⊢A=\left\{x\right\}\to \left(B=\left\{y\right\}\to \left(\left(A\cup B\right)\approx 2_{𝑜}\to A\cap B=\varnothing \right)\right)$$
43	42	exlimdv	$$⊢A=\left\{x\right\}\to \left(\exists yB=\left\{y\right\}\to \left(\left(A\cup B\right)\approx 2_{𝑜}\to A\cap B=\varnothing \right)\right)$$
44	43	exlimiv	$$⊢\exists xA=\left\{x\right\}\to \left(\exists yB=\left\{y\right\}\to \left(\left(A\cup B\right)\approx 2_{𝑜}\to A\cap B=\varnothing \right)\right)$$
45	44	imp	$$⊢\left(\exists xA=\left\{x\right\}\wedge \exists yB=\left\{y\right\}\right)\to \left(\left(A\cup B\right)\approx 2_{𝑜}\to A\cap B=\varnothing \right)$$
46	19 20 45	syl2anb	$$⊢\left(A\approx 1_{𝑜}\wedge B\approx 1_{𝑜}\right)\to \left(\left(A\cup B\right)\approx 2_{𝑜}\to A\cap B=\varnothing \right)$$
47	18 46	impbid	$$⊢\left(A\approx 1_{𝑜}\wedge B\approx 1_{𝑜}\right)\to \left(A\cap B=\varnothing \leftrightarrow \left(A\cup B\right)\approx 2_{𝑜}\right)$$