Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dju1p1e2 | Structured version Visualization version GIF version |
Description: 1+1=2 for cardinal number addition, derived from pm54.43 9422 as promised. Theorem *110.643 of Principia 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 9317), 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 9593 for a shorter proof that doesn't use pm54.43 9422. (Contributed by NM, 5-Apr-2007.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
dju1p1e2 | ⊢ (1o ⊔ 1o) ≈ 2o |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dju 9323 | . 2 ⊢ (1o ⊔ 1o) = (({∅} × 1o) ∪ ({1o} × 1o)) | |
2 | xp01disjl 8114 | . . 3 ⊢ (({∅} × 1o) ∩ ({1o} × 1o)) = ∅ | |
3 | 0ex 5204 | . . . . 5 ⊢ ∅ ∈ V | |
4 | 1on 8102 | . . . . 5 ⊢ 1o ∈ On | |
5 | xpsnen2g 8603 | . . . . 5 ⊢ ((∅ ∈ V ∧ 1o ∈ On) → ({∅} × 1o) ≈ 1o) | |
6 | 3, 4, 5 | mp2an 690 | . . . 4 ⊢ ({∅} × 1o) ≈ 1o |
7 | xpsnen2g 8603 | . . . . 5 ⊢ ((1o ∈ On ∧ 1o ∈ On) → ({1o} × 1o) ≈ 1o) | |
8 | 4, 4, 7 | mp2an 690 | . . . 4 ⊢ ({1o} × 1o) ≈ 1o |
9 | pm54.43 9422 | . . . 4 ⊢ ((({∅} × 1o) ≈ 1o ∧ ({1o} × 1o) ≈ 1o) → ((({∅} × 1o) ∩ ({1o} × 1o)) = ∅ ↔ (({∅} × 1o) ∪ ({1o} × 1o)) ≈ 2o)) | |
10 | 6, 8, 9 | mp2an 690 | . . 3 ⊢ ((({∅} × 1o) ∩ ({1o} × 1o)) = ∅ ↔ (({∅} × 1o) ∪ ({1o} × 1o)) ≈ 2o) |
11 | 2, 10 | mpbi 232 | . 2 ⊢ (({∅} × 1o) ∪ ({1o} × 1o)) ≈ 2o |
12 | 1, 11 | eqbrtri 5080 | 1 ⊢ (1o ⊔ 1o) ≈ 2o |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 = wceq 1536 ∈ wcel 2113 Vcvv 3491 ∪ cun 3927 ∩ cin 3928 ∅c0 4284 {csn 4560 class class class wbr 5059 × cxp 5546 Oncon0 6184 1oc1o 8088 2oc2o 8089 ≈ cen 8499 ⊔ cdju 9320 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2792 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5323 ax-un 7454 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1083 df-3an 1084 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2799 df-cleq 2813 df-clel 2892 df-nfc 2962 df-ne 3016 df-ral 3142 df-rex 3143 df-reu 3144 df-rab 3146 df-v 3493 df-sbc 3769 df-dif 3932 df-un 3934 df-in 3936 df-ss 3945 df-pss 3947 df-nul 4285 df-if 4461 df-pw 4534 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-int 4870 df-br 5060 df-opab 5122 df-mpt 5140 df-tr 5166 df-id 5453 df-eprel 5458 df-po 5467 df-so 5468 df-fr 5507 df-we 5509 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-ord 6187 df-on 6188 df-lim 6189 df-suc 6190 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-f1 6353 df-fo 6354 df-f1o 6355 df-fv 6356 df-om 7574 df-1st 7682 df-2nd 7683 df-1o 8095 df-2o 8096 df-er 8282 df-en 8503 df-dom 8504 df-sdom 8505 df-dju 9323 |
This theorem is referenced by: pr2dom 39967 |
Copyright terms: Public domain | W3C validator |