![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm110.643 | Structured version Visualization version GIF version |
Description: 1+1=2 for cardinal number addition, derived from pm54.43 9027 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 8923), but after applying definitions, our theorem is equivalent. The comment for cdaval 9195 explains why we use ≈ instead of =. See pm110.643ALT 9203 for a shorter proof that doesn't use pm54.43 9027. (Contributed by NM, 5-Apr-2007.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
pm110.643 | ⊢ (1𝑜 +𝑐 1𝑜) ≈ 2𝑜 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1on 7721 | . . 3 ⊢ 1𝑜 ∈ On | |
2 | cdaval 9195 | . . 3 ⊢ ((1𝑜 ∈ On ∧ 1𝑜 ∈ On) → (1𝑜 +𝑐 1𝑜) = ((1𝑜 × {∅}) ∪ (1𝑜 × {1𝑜}))) | |
3 | 1, 1, 2 | mp2an 666 | . 2 ⊢ (1𝑜 +𝑐 1𝑜) = ((1𝑜 × {∅}) ∪ (1𝑜 × {1𝑜})) |
4 | xp01disj 7731 | . . 3 ⊢ ((1𝑜 × {∅}) ∩ (1𝑜 × {1𝑜})) = ∅ | |
5 | 1 | elexi 3365 | . . . . 5 ⊢ 1𝑜 ∈ V |
6 | 0ex 4925 | . . . . 5 ⊢ ∅ ∈ V | |
7 | 5, 6 | xpsnen 8201 | . . . 4 ⊢ (1𝑜 × {∅}) ≈ 1𝑜 |
8 | 5, 5 | xpsnen 8201 | . . . 4 ⊢ (1𝑜 × {1𝑜}) ≈ 1𝑜 |
9 | pm54.43 9027 | . . . 4 ⊢ (((1𝑜 × {∅}) ≈ 1𝑜 ∧ (1𝑜 × {1𝑜}) ≈ 1𝑜) → (((1𝑜 × {∅}) ∩ (1𝑜 × {1𝑜})) = ∅ ↔ ((1𝑜 × {∅}) ∪ (1𝑜 × {1𝑜})) ≈ 2𝑜)) | |
10 | 7, 8, 9 | mp2an 666 | . . 3 ⊢ (((1𝑜 × {∅}) ∩ (1𝑜 × {1𝑜})) = ∅ ↔ ((1𝑜 × {∅}) ∪ (1𝑜 × {1𝑜})) ≈ 2𝑜) |
11 | 4, 10 | mpbi 220 | . 2 ⊢ ((1𝑜 × {∅}) ∪ (1𝑜 × {1𝑜})) ≈ 2𝑜 |
12 | 3, 11 | eqbrtri 4808 | 1 ⊢ (1𝑜 +𝑐 1𝑜) ≈ 2𝑜 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 = wceq 1631 ∈ wcel 2145 ∪ cun 3722 ∩ cin 3723 ∅c0 4064 {csn 4317 class class class wbr 4787 × cxp 5248 Oncon0 5867 (class class class)co 6794 1𝑜c1o 7707 2𝑜c2o 7708 ≈ cen 8107 +𝑐 ccda 9192 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4916 ax-nul 4924 ax-pow 4975 ax-pr 5035 ax-un 7097 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-3or 1072 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-ral 3066 df-rex 3067 df-reu 3068 df-rab 3070 df-v 3353 df-sbc 3589 df-dif 3727 df-un 3729 df-in 3731 df-ss 3738 df-pss 3740 df-nul 4065 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-tp 4322 df-op 4324 df-uni 4576 df-int 4613 df-br 4788 df-opab 4848 df-mpt 4865 df-tr 4888 df-id 5158 df-eprel 5163 df-po 5171 df-so 5172 df-fr 5209 df-we 5211 df-xp 5256 df-rel 5257 df-cnv 5258 df-co 5259 df-dm 5260 df-rn 5261 df-res 5262 df-ima 5263 df-ord 5870 df-on 5871 df-lim 5872 df-suc 5873 df-iota 5995 df-fun 6034 df-fn 6035 df-f 6036 df-f1 6037 df-fo 6038 df-f1o 6039 df-fv 6040 df-ov 6797 df-oprab 6798 df-mpt2 6799 df-om 7214 df-1o 7714 df-2o 7715 df-er 7897 df-en 8111 df-dom 8112 df-sdom 8113 df-cda 9193 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |