Theorem pm54.43 10063

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 10030), so that their 𝐴 ∈ 1 means, in our notation, 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1_o} which is the same as 𝐴 ≈ 1_o by pm54.43lem 10062. 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 10233 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007.)

Assertion

Ref	Expression
pm54.43	⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2o))

Proof of Theorem pm54.43

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1oex 8470	. . . . . . 7 ⊢ 1o ∈ V
2	1	ensn1 9032	. . . . . 6 ⊢ {1o} ≈ 1o
3	2	ensymi 9015	. . . . 5 ⊢ 1o ≈ {1o}
4		entr 9017	. . . . 5 ⊢ ((𝐵 ≈ 1o ∧ 1o ≈ {1o}) → 𝐵 ≈ {1o})
5	3, 4	mpan2 704	. . . 4 ⊢ (𝐵 ≈ 1o → 𝐵 ≈ {1o})
6		1on 8473	. . . . . . . 8 ⊢ 1o ∈ On
7	6	onirri 6470	. . . . . . 7 ⊢ ¬ 1o ∈ 1o
8		disjsn 4672	. . . . . . 7 ⊢ ((1o ∩ {1o}) = ∅ ↔ ¬ 1o ∈ 1o)
9	7, 8	mpbir 234	. . . . . 6 ⊢ (1o ∩ {1o}) = ∅
10		unen 9057	. . . . . 6 ⊢ (((𝐴 ≈ 1o ∧ 𝐵 ≈ {1o}) ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ (1o ∩ {1o}) = ∅)) → (𝐴 ∪ 𝐵) ≈ (1o ∪ {1o}))
11	9, 10	mpanr2 717	. . . . 5 ⊢ (((𝐴 ≈ 1o ∧ 𝐵 ≈ {1o}) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ≈ (1o ∪ {1o}))
12	11	ex 418	. . . 4 ⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ {1o}) → ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∪ 𝐵) ≈ (1o ∪ {1o})))
13	5, 12	sylan2 605	. . 3 ⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∪ 𝐵) ≈ (1o ∪ {1o})))
14		df-2o 8461	. . . . 5 ⊢ 2o = suc 1o
15		df-suc 6361	. . . . 5 ⊢ suc 1o = (1o ∪ {1o})
16	14, 15	eqtri 2784	. . . 4 ⊢ 2o = (1o ∪ {1o})
17	16	breq2i 5111	. . 3 ⊢ ((𝐴 ∪ 𝐵) ≈ 2o ↔ (𝐴 ∪ 𝐵) ≈ (1o ∪ {1o}))
18	13, 17	imbitrrdi 255	. 2 ⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∪ 𝐵) ≈ 2o))
19		en1 9035	. . 3 ⊢ (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥})
20		en1 9035	. . 3 ⊢ (𝐵 ≈ 1o ↔ ∃𝑦 𝐵 = {𝑦})
21		sneq 4594	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
22	21	uneq2d 4115	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ({𝑥} ∪ {𝑥}) = ({𝑥} ∪ {𝑦}))
23		unidm 4104	. . . . . . . . . . . . . 14 ⊢ ({𝑥} ∪ {𝑥}) = {𝑥}
24	22, 23	eqtr3di 2811	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ({𝑥} ∪ {𝑦}) = {𝑥})
25		vex 3455	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
26	25	ensn1 9032	. . . . . . . . . . . . . 14 ⊢ {𝑥} ≈ 1o
27		1sdom2 9223	. . . . . . . . . . . . . 14 ⊢ 1o ≺ 2o
28		ensdomtr 9116	. . . . . . . . . . . . . 14 ⊢ (({𝑥} ≈ 1o ∧ 1o ≺ 2o) → {𝑥} ≺ 2o)
29	26, 27, 28	mp2an 705	. . . . . . . . . . . . 13 ⊢ {𝑥} ≺ 2o
30	24, 29	eqbrtrdi 5144	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ({𝑥} ∪ {𝑦}) ≺ 2o)
31		sdomnen 8992	. . . . . . . . . . . 12 ⊢ (({𝑥} ∪ {𝑦}) ≺ 2o → ¬ ({𝑥} ∪ {𝑦}) ≈ 2o)
32	30, 31	syl 18	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ¬ ({𝑥} ∪ {𝑦}) ≈ 2o)
33	32	necon2ai 2985	. . . . . . . . . 10 ⊢ (({𝑥} ∪ {𝑦}) ≈ 2o → 𝑥 ≠ 𝑦)
34		disjsn2 4673	. . . . . . . . . 10 ⊢ (𝑥 ≠ 𝑦 → ({𝑥} ∩ {𝑦}) = ∅)
35	33, 34	syl 18	. . . . . . . . 9 ⊢ (({𝑥} ∪ {𝑦}) ≈ 2o → ({𝑥} ∩ {𝑦}) = ∅)
36	35	a1i 11	. . . . . . . 8 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (({𝑥} ∪ {𝑦}) ≈ 2o → ({𝑥} ∩ {𝑦}) = ∅))
37		uneq12 4110	. . . . . . . . 9 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (𝐴 ∪ 𝐵) = ({𝑥} ∪ {𝑦}))
38	37	breq1d 5113	. . . . . . . 8 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴 ∪ 𝐵) ≈ 2o ↔ ({𝑥} ∪ {𝑦}) ≈ 2o))
39		ineq12 4161	. . . . . . . . 9 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (𝐴 ∩ 𝐵) = ({𝑥} ∩ {𝑦}))
40	39	eqeq1d 2763	. . . . . . . 8 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴 ∩ 𝐵) = ∅ ↔ ({𝑥} ∩ {𝑦}) = ∅))
41	36, 38, 40	3imtr4d 297	. . . . . . 7 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴 ∪ 𝐵) ≈ 2o → (𝐴 ∩ 𝐵) = ∅))
42	41	ex 418	. . . . . 6 ⊢ (𝐴 = {𝑥} → (𝐵 = {𝑦} → ((𝐴 ∪ 𝐵) ≈ 2o → (𝐴 ∩ 𝐵) = ∅)))
43	42	exlimdv 1966	. . . . 5 ⊢ (𝐴 = {𝑥} → (∃𝑦 𝐵 = {𝑦} → ((𝐴 ∪ 𝐵) ≈ 2o → (𝐴 ∩ 𝐵) = ∅)))
44	43	exlimiv 1963	. . . 4 ⊢ (∃𝑥 𝐴 = {𝑥} → (∃𝑦 𝐵 = {𝑦} → ((𝐴 ∪ 𝐵) ≈ 2o → (𝐴 ∩ 𝐵) = ∅)))
45	44	imp 412	. . 3 ⊢ ((∃𝑥 𝐴 = {𝑥} ∧ ∃𝑦 𝐵 = {𝑦}) → ((𝐴 ∪ 𝐵) ≈ 2o → (𝐴 ∩ 𝐵) = ∅))
46	19, 20, 45	syl2anb 610	. 2 ⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∪ 𝐵) ≈ 2o → (𝐴 ∩ 𝐵) = ∅))
47	18, 46	impbid 215	1 ⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2o))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2956   ∪ cun 3897   ∩ cin 3898  ∅c0 4279  {csn 4584   class class class wbr 5103  suc csuc 6357  1_oc1o 8453  2_oc2o 8454   ≈ cen 8954   ≺ csdm 8956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-ord 6358  df-on 6359  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-1o 8460  df-2o 8461  df-er 8701  df-en 8958  df-dom 8959  df-sdom 8960

This theorem is used by:  dju1p1e2  10233