Theorem pm54.43 8709

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

Assertion

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

Proof of Theorem pm54.43

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

Step	Hyp	Ref	Expression
1		1on 7454	. . . . . . . 8 ⊢ 1𝑜 ∈ On
2	1	elexi 3186	. . . . . . 7 ⊢ 1𝑜 ∈ V
3	2	ensn1 7906	. . . . . 6 ⊢ {1𝑜} ≈ 1𝑜
4	3	ensymi 7892	. . . . 5 ⊢ 1𝑜 ≈ {1𝑜}
5		entr 7894	. . . . 5 ⊢ ((𝐵 ≈ 1𝑜 ∧ 1𝑜 ≈ {1𝑜}) → 𝐵 ≈ {1𝑜})
6	4, 5	mpan2 703	. . . 4 ⊢ (𝐵 ≈ 1𝑜 → 𝐵 ≈ {1𝑜})
7	1	onirri 5751	. . . . . . 7 ⊢ ¬ 1𝑜 ∈ 1𝑜
8		disjsn 4192	. . . . . . 7 ⊢ ((1𝑜 ∩ {1𝑜}) = ∅ ↔ ¬ 1𝑜 ∈ 1𝑜)
9	7, 8	mpbir 220	. . . . . 6 ⊢ (1𝑜 ∩ {1𝑜}) = ∅
10		unen 7925	. . . . . 6 ⊢ (((𝐴 ≈ 1𝑜 ∧ 𝐵 ≈ {1𝑜}) ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ (1𝑜 ∩ {1𝑜}) = ∅)) → (𝐴 ∪ 𝐵) ≈ (1𝑜 ∪ {1𝑜}))
11	9, 10	mpanr2 716	. . . . 5 ⊢ (((𝐴 ≈ 1𝑜 ∧ 𝐵 ≈ {1𝑜}) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ≈ (1𝑜 ∪ {1𝑜}))
12	11	ex 449	. . . 4 ⊢ ((𝐴 ≈ 1𝑜 ∧ 𝐵 ≈ {1𝑜}) → ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∪ 𝐵) ≈ (1𝑜 ∪ {1𝑜})))
13	6, 12	sylan2 490	. . 3 ⊢ ((𝐴 ≈ 1𝑜 ∧ 𝐵 ≈ 1𝑜) → ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∪ 𝐵) ≈ (1𝑜 ∪ {1𝑜})))
14		df-2o 7448	. . . . 5 ⊢ 2𝑜 = suc 1𝑜
15		df-suc 5646	. . . . 5 ⊢ suc 1𝑜 = (1𝑜 ∪ {1𝑜})
16	14, 15	eqtri 2632	. . . 4 ⊢ 2𝑜 = (1𝑜 ∪ {1𝑜})
17	16	breq2i 4591	. . 3 ⊢ ((𝐴 ∪ 𝐵) ≈ 2𝑜 ↔ (𝐴 ∪ 𝐵) ≈ (1𝑜 ∪ {1𝑜}))
18	13, 17	syl6ibr 241	. 2 ⊢ ((𝐴 ≈ 1𝑜 ∧ 𝐵 ≈ 1𝑜) → ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∪ 𝐵) ≈ 2𝑜))
19		en1 7909	. . 3 ⊢ (𝐴 ≈ 1𝑜 ↔ ∃𝑥 𝐴 = {𝑥})
20		en1 7909	. . 3 ⊢ (𝐵 ≈ 1𝑜 ↔ ∃𝑦 𝐵 = {𝑦})
21		unidm 3718	. . . . . . . . . . . . . 14 ⊢ ({𝑥} ∪ {𝑥}) = {𝑥}
22		sneq 4135	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
23	22	uneq2d 3729	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ({𝑥} ∪ {𝑥}) = ({𝑥} ∪ {𝑦}))
24	21, 23	syl5reqr 2659	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ({𝑥} ∪ {𝑦}) = {𝑥})
25		vex 3176	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
26	25	ensn1 7906	. . . . . . . . . . . . . 14 ⊢ {𝑥} ≈ 1𝑜
27		1sdom2 8044	. . . . . . . . . . . . . 14 ⊢ 1𝑜 ≺ 2𝑜
28		ensdomtr 7981	. . . . . . . . . . . . . 14 ⊢ (({𝑥} ≈ 1𝑜 ∧ 1𝑜 ≺ 2𝑜) → {𝑥} ≺ 2𝑜)
29	26, 27, 28	mp2an 704	. . . . . . . . . . . . 13 ⊢ {𝑥} ≺ 2𝑜
30	24, 29	syl6eqbr 4622	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ({𝑥} ∪ {𝑦}) ≺ 2𝑜)
31		sdomnen 7870	. . . . . . . . . . . 12 ⊢ (({𝑥} ∪ {𝑦}) ≺ 2𝑜 → ¬ ({𝑥} ∪ {𝑦}) ≈ 2𝑜)
32	30, 31	syl 17	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ¬ ({𝑥} ∪ {𝑦}) ≈ 2𝑜)
33	32	necon2ai 2811	. . . . . . . . . 10 ⊢ (({𝑥} ∪ {𝑦}) ≈ 2𝑜 → 𝑥 ≠ 𝑦)
34		disjsn2 4193	. . . . . . . . . 10 ⊢ (𝑥 ≠ 𝑦 → ({𝑥} ∩ {𝑦}) = ∅)
35	33, 34	syl 17	. . . . . . . . 9 ⊢ (({𝑥} ∪ {𝑦}) ≈ 2𝑜 → ({𝑥} ∩ {𝑦}) = ∅)
36	35	a1i 11	. . . . . . . 8 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (({𝑥} ∪ {𝑦}) ≈ 2𝑜 → ({𝑥} ∩ {𝑦}) = ∅))
37		uneq12 3724	. . . . . . . . 9 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (𝐴 ∪ 𝐵) = ({𝑥} ∪ {𝑦}))
38	37	breq1d 4593	. . . . . . . 8 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴 ∪ 𝐵) ≈ 2𝑜 ↔ ({𝑥} ∪ {𝑦}) ≈ 2𝑜))
39		ineq12 3771	. . . . . . . . 9 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (𝐴 ∩ 𝐵) = ({𝑥} ∩ {𝑦}))
40	39	eqeq1d 2612	. . . . . . . 8 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴 ∩ 𝐵) = ∅ ↔ ({𝑥} ∩ {𝑦}) = ∅))
41	36, 38, 40	3imtr4d 282	. . . . . . 7 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴 ∪ 𝐵) ≈ 2𝑜 → (𝐴 ∩ 𝐵) = ∅))
42	41	ex 449	. . . . . 6 ⊢ (𝐴 = {𝑥} → (𝐵 = {𝑦} → ((𝐴 ∪ 𝐵) ≈ 2𝑜 → (𝐴 ∩ 𝐵) = ∅)))
43	42	exlimdv 1848	. . . . 5 ⊢ (𝐴 = {𝑥} → (∃𝑦 𝐵 = {𝑦} → ((𝐴 ∪ 𝐵) ≈ 2𝑜 → (𝐴 ∩ 𝐵) = ∅)))
44	43	exlimiv 1845	. . . 4 ⊢ (∃𝑥 𝐴 = {𝑥} → (∃𝑦 𝐵 = {𝑦} → ((𝐴 ∪ 𝐵) ≈ 2𝑜 → (𝐴 ∩ 𝐵) = ∅)))
45	44	imp 444	. . 3 ⊢ ((∃𝑥 𝐴 = {𝑥} ∧ ∃𝑦 𝐵 = {𝑦}) → ((𝐴 ∪ 𝐵) ≈ 2𝑜 → (𝐴 ∩ 𝐵) = ∅))
46	19, 20, 45	syl2anb 495	. 2 ⊢ ((𝐴 ≈ 1𝑜 ∧ 𝐵 ≈ 1𝑜) → ((𝐴 ∪ 𝐵) ≈ 2𝑜 → (𝐴 ∩ 𝐵) = ∅))
47	18, 46	impbid 201	1 ⊢ ((𝐴 ≈ 1𝑜 ∧ 𝐵 ≈ 1𝑜) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2𝑜))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780   ∪ cun 3538   ∩ cin 3539  ∅c0 3874  {csn 4125   class class class wbr 4583  Oncon0 5640  suc csuc 5642  1_𝑜c1o 7440  2_𝑜c2o 7441   ≈ cen 7838   ≺ csdm 7840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-om 6958  df-1o 7447  df-2o 7448  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844

This theorem is referenced by:  pr2nelem  8710  pm110.643  8882  isprm2lem  15232