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	⊢ ( ( 𝐴 ≈ 1o ∧ 𝐵 ≈ 1o ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ( 𝐴 ∪ 𝐵 ) ≈ 2o ) )

Proof

Step	Hyp	Ref	Expression
1		1oex	⊢ 1o ∈ V
2	1	ensn1	⊢ { 1o } ≈ 1o
3	2	ensymi	⊢ 1o ≈ { 1o }
4		entr	⊢ ( ( 𝐵 ≈ 1o ∧ 1o ≈ { 1o } ) → 𝐵 ≈ { 1o } )
5	3 4	mpan2	⊢ ( 𝐵 ≈ 1o → 𝐵 ≈ { 1o } )
6		1on	⊢ 1o ∈ On
7	6	onirri	⊢ ¬ 1o ∈ 1o
8		disjsn	⊢ ( ( 1o ∩ { 1o } ) = ∅ ↔ ¬ 1o ∈ 1o )
9	7 8	mpbir	⊢ ( 1o ∩ { 1o } ) = ∅
10		unen	⊢ ( ( ( 𝐴 ≈ 1o ∧ 𝐵 ≈ { 1o } ) ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ ( 1o ∩ { 1o } ) = ∅ ) ) → ( 𝐴 ∪ 𝐵 ) ≈ ( 1o ∪ { 1o } ) )
11	9 10	mpanr2	⊢ ( ( ( 𝐴 ≈ 1o ∧ 𝐵 ≈ { 1o } ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∪ 𝐵 ) ≈ ( 1o ∪ { 1o } ) )
12	11	ex	⊢ ( ( 𝐴 ≈ 1o ∧ 𝐵 ≈ { 1o } ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ∪ 𝐵 ) ≈ ( 1o ∪ { 1o } ) ) )
13	5 12	sylan2	⊢ ( ( 𝐴 ≈ 1o ∧ 𝐵 ≈ 1o ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ∪ 𝐵 ) ≈ ( 1o ∪ { 1o } ) ) )
14		df-2o	⊢ 2o = suc 1o
15		df-suc	⊢ suc 1o = ( 1o ∪ { 1o } )
16	14 15	eqtri	⊢ 2o = ( 1o ∪ { 1o } )
17	16	breq2i	⊢ ( ( 𝐴 ∪ 𝐵 ) ≈ 2o ↔ ( 𝐴 ∪ 𝐵 ) ≈ ( 1o ∪ { 1o } ) )
18	13 17	syl6ibr	⊢ ( ( 𝐴 ≈ 1o ∧ 𝐵 ≈ 1o ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ∪ 𝐵 ) ≈ 2o ) )
19		en1	⊢ ( 𝐴 ≈ 1o ↔ ∃ 𝑥 𝐴 = { 𝑥 } )
20		en1	⊢ ( 𝐵 ≈ 1o ↔ ∃ 𝑦 𝐵 = { 𝑦 } )
21		unidm	⊢ ( { 𝑥 } ∪ { 𝑥 } ) = { 𝑥 }
22		sneq	⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
23	22	uneq2d	⊢ ( 𝑥 = 𝑦 → ( { 𝑥 } ∪ { 𝑥 } ) = ( { 𝑥 } ∪ { 𝑦 } ) )
24	21 23	syl5reqr	⊢ ( 𝑥 = 𝑦 → ( { 𝑥 } ∪ { 𝑦 } ) = { 𝑥 } )
25		vex	⊢ 𝑥 ∈ V
26	25	ensn1	⊢ { 𝑥 } ≈ 1o
27		1sdom2	⊢ 1o ≺ 2o
28		ensdomtr	⊢ ( ( { 𝑥 } ≈ 1o ∧ 1o ≺ 2o ) → { 𝑥 } ≺ 2o )
29	26 27 28	mp2an	⊢ { 𝑥 } ≺ 2o
30	24 29	eqbrtrdi	⊢ ( 𝑥 = 𝑦 → ( { 𝑥 } ∪ { 𝑦 } ) ≺ 2o )
31		sdomnen	⊢ ( ( { 𝑥 } ∪ { 𝑦 } ) ≺ 2o → ¬ ( { 𝑥 } ∪ { 𝑦 } ) ≈ 2o )
32	30 31	syl	⊢ ( 𝑥 = 𝑦 → ¬ ( { 𝑥 } ∪ { 𝑦 } ) ≈ 2o )
33	32	necon2ai	⊢ ( ( { 𝑥 } ∪ { 𝑦 } ) ≈ 2o → 𝑥 ≠ 𝑦 )
34		disjsn2	⊢ ( 𝑥 ≠ 𝑦 → ( { 𝑥 } ∩ { 𝑦 } ) = ∅ )
35	33 34	syl	⊢ ( ( { 𝑥 } ∪ { 𝑦 } ) ≈ 2o → ( { 𝑥 } ∩ { 𝑦 } ) = ∅ )
36	35	a1i	⊢ ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑦 } ) → ( ( { 𝑥 } ∪ { 𝑦 } ) ≈ 2o → ( { 𝑥 } ∩ { 𝑦 } ) = ∅ ) )
37		uneq12	⊢ ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑦 } ) → ( 𝐴 ∪ 𝐵 ) = ( { 𝑥 } ∪ { 𝑦 } ) )
38	37	breq1d	⊢ ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑦 } ) → ( ( 𝐴 ∪ 𝐵 ) ≈ 2o ↔ ( { 𝑥 } ∪ { 𝑦 } ) ≈ 2o ) )
39		ineq12	⊢ ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑦 } ) → ( 𝐴 ∩ 𝐵 ) = ( { 𝑥 } ∩ { 𝑦 } ) )
40	39	eqeq1d	⊢ ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑦 } ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ( { 𝑥 } ∩ { 𝑦 } ) = ∅ ) )
41	36 38 40	3imtr4d	⊢ ( ( 𝐴 = { 𝑥 } ∧ 𝐵 = { 𝑦 } ) → ( ( 𝐴 ∪ 𝐵 ) ≈ 2o → ( 𝐴 ∩ 𝐵 ) = ∅ ) )
42	41	ex	⊢ ( 𝐴 = { 𝑥 } → ( 𝐵 = { 𝑦 } → ( ( 𝐴 ∪ 𝐵 ) ≈ 2o → ( 𝐴 ∩ 𝐵 ) = ∅ ) ) )
43	42	exlimdv	⊢ ( 𝐴 = { 𝑥 } → ( ∃ 𝑦 𝐵 = { 𝑦 } → ( ( 𝐴 ∪ 𝐵 ) ≈ 2o → ( 𝐴 ∩ 𝐵 ) = ∅ ) ) )
44	43	exlimiv	⊢ ( ∃ 𝑥 𝐴 = { 𝑥 } → ( ∃ 𝑦 𝐵 = { 𝑦 } → ( ( 𝐴 ∪ 𝐵 ) ≈ 2o → ( 𝐴 ∩ 𝐵 ) = ∅ ) ) )
45	44	imp	⊢ ( ( ∃ 𝑥 𝐴 = { 𝑥 } ∧ ∃ 𝑦 𝐵 = { 𝑦 } ) → ( ( 𝐴 ∪ 𝐵 ) ≈ 2o → ( 𝐴 ∩ 𝐵 ) = ∅ ) )
46	19 20 45	syl2anb	⊢ ( ( 𝐴 ≈ 1o ∧ 𝐵 ≈ 1o ) → ( ( 𝐴 ∪ 𝐵 ) ≈ 2o → ( 𝐴 ∩ 𝐵 ) = ∅ ) )
47	18 46	impbid	⊢ ( ( 𝐴 ≈ 1o ∧ 𝐵 ≈ 1o ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ( 𝐴 ∪ 𝐵 ) ≈ 2o ) )