Metamath Proof Explorer


Theorem dju1p1e2

Description: 1+1=2 for cardinal number addition, derived from pm54.43 as promised. Theorem *110.643 ofPrincipia 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 ), 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 for a shorter proof that doesn't use pm54.43 . (Contributed by NM, 5-Apr-2007) (Proof modification is discouraged.)

Ref Expression
Assertion dju1p1e2
|- ( 1o |_| 1o ) ~~ 2o

Proof

Step Hyp Ref Expression
1 df-dju
 |-  ( 1o |_| 1o ) = ( ( { (/) } X. 1o ) u. ( { 1o } X. 1o ) )
2 xp01disjl
 |-  ( ( { (/) } X. 1o ) i^i ( { 1o } X. 1o ) ) = (/)
3 0ex
 |-  (/) e. _V
4 1on
 |-  1o e. On
5 xpsnen2g
 |-  ( ( (/) e. _V /\ 1o e. On ) -> ( { (/) } X. 1o ) ~~ 1o )
6 3 4 5 mp2an
 |-  ( { (/) } X. 1o ) ~~ 1o
7 xpsnen2g
 |-  ( ( 1o e. On /\ 1o e. On ) -> ( { 1o } X. 1o ) ~~ 1o )
8 4 4 7 mp2an
 |-  ( { 1o } X. 1o ) ~~ 1o
9 pm54.43
 |-  ( ( ( { (/) } X. 1o ) ~~ 1o /\ ( { 1o } X. 1o ) ~~ 1o ) -> ( ( ( { (/) } X. 1o ) i^i ( { 1o } X. 1o ) ) = (/) <-> ( ( { (/) } X. 1o ) u. ( { 1o } X. 1o ) ) ~~ 2o ) )
10 6 8 9 mp2an
 |-  ( ( ( { (/) } X. 1o ) i^i ( { 1o } X. 1o ) ) = (/) <-> ( ( { (/) } X. 1o ) u. ( { 1o } X. 1o ) ) ~~ 2o )
11 2 10 mpbi
 |-  ( ( { (/) } X. 1o ) u. ( { 1o } X. 1o ) ) ~~ 2o
12 1 11 eqbrtri
 |-  ( 1o |_| 1o ) ~~ 2o