![]() |
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 9008 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 9176 explains why we use ≈ instead of =. See pm110.643ALT 9184 for a shorter proof that doesn't use pm54.43 9008. (Contributed by NM, 5-Apr-2007.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
pm110.643 | ⊢ (1𝑜 +𝑐 1𝑜) ≈ 2𝑜 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1on 7728 | . . 3 ⊢ 1𝑜 ∈ On | |
2 | cdaval 9176 | . . 3 ⊢ ((1𝑜 ∈ On ∧ 1𝑜 ∈ On) → (1𝑜 +𝑐 1𝑜) = ((1𝑜 × {∅}) ∪ (1𝑜 × {1𝑜}))) | |
3 | 1, 1, 2 | mp2an 710 | . 2 ⊢ (1𝑜 +𝑐 1𝑜) = ((1𝑜 × {∅}) ∪ (1𝑜 × {1𝑜})) |
4 | xp01disj 7737 | . . 3 ⊢ ((1𝑜 × {∅}) ∩ (1𝑜 × {1𝑜})) = ∅ | |
5 | 1 | elexi 3345 | . . . . 5 ⊢ 1𝑜 ∈ V |
6 | 0ex 4934 | . . . . 5 ⊢ ∅ ∈ V | |
7 | 5, 6 | xpsnen 8201 | . . . 4 ⊢ (1𝑜 × {∅}) ≈ 1𝑜 |
8 | 5, 5 | xpsnen 8201 | . . . 4 ⊢ (1𝑜 × {1𝑜}) ≈ 1𝑜 |
9 | pm54.43 9008 | . . . 4 ⊢ (((1𝑜 × {∅}) ≈ 1𝑜 ∧ (1𝑜 × {1𝑜}) ≈ 1𝑜) → (((1𝑜 × {∅}) ∩ (1𝑜 × {1𝑜})) = ∅ ↔ ((1𝑜 × {∅}) ∪ (1𝑜 × {1𝑜})) ≈ 2𝑜)) | |
10 | 7, 8, 9 | mp2an 710 | . . 3 ⊢ (((1𝑜 × {∅}) ∩ (1𝑜 × {1𝑜})) = ∅ ↔ ((1𝑜 × {∅}) ∪ (1𝑜 × {1𝑜})) ≈ 2𝑜) |
11 | 4, 10 | mpbi 220 | . 2 ⊢ ((1𝑜 × {∅}) ∪ (1𝑜 × {1𝑜})) ≈ 2𝑜 |
12 | 3, 11 | eqbrtri 4817 | 1 ⊢ (1𝑜 +𝑐 1𝑜) ≈ 2𝑜 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 = wceq 1624 ∈ wcel 2131 ∪ cun 3705 ∩ cin 3706 ∅c0 4050 {csn 4313 class class class wbr 4796 × cxp 5256 Oncon0 5876 (class class class)co 6805 1𝑜c1o 7714 2𝑜c2o 7715 ≈ cen 8110 +𝑐 ccda 9173 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-8 2133 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-sep 4925 ax-nul 4933 ax-pow 4984 ax-pr 5047 ax-un 7106 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ne 2925 df-ral 3047 df-rex 3048 df-reu 3049 df-rab 3051 df-v 3334 df-sbc 3569 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-pss 3723 df-nul 4051 df-if 4223 df-pw 4296 df-sn 4314 df-pr 4316 df-tp 4318 df-op 4320 df-uni 4581 df-int 4620 df-br 4797 df-opab 4857 df-mpt 4874 df-tr 4897 df-id 5166 df-eprel 5171 df-po 5179 df-so 5180 df-fr 5217 df-we 5219 df-xp 5264 df-rel 5265 df-cnv 5266 df-co 5267 df-dm 5268 df-rn 5269 df-res 5270 df-ima 5271 df-ord 5879 df-on 5880 df-lim 5881 df-suc 5882 df-iota 6004 df-fun 6043 df-fn 6044 df-f 6045 df-f1 6046 df-fo 6047 df-f1o 6048 df-fv 6049 df-ov 6808 df-oprab 6809 df-mpt2 6810 df-om 7223 df-1o 7721 df-2o 7722 df-er 7903 df-en 8114 df-dom 8115 df-sdom 8116 df-cda 9174 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |