Description: Two times a cardinal number. Exercise 4.56(g) of Mendelson p. 258. (Contributed by NM, 27-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | xp2dju | |- ( 2o X. A ) = ( A |_| A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xpundir | |- ( ( { (/) } u. { 1o } ) X. A ) = ( ( { (/) } X. A ) u. ( { 1o } X. A ) ) |
|
| 2 | df2o3 | |- 2o = { (/) , 1o } |
|
| 3 | df-pr | |- { (/) , 1o } = ( { (/) } u. { 1o } ) |
|
| 4 | 2 3 | eqtri | |- 2o = ( { (/) } u. { 1o } ) |
| 5 | 4 | xpeq1i | |- ( 2o X. A ) = ( ( { (/) } u. { 1o } ) X. A ) |
| 6 | df-dju | |- ( A |_| A ) = ( ( { (/) } X. A ) u. ( { 1o } X. A ) ) |
|
| 7 | 1 5 6 | 3eqtr4i | |- ( 2o X. A ) = ( A |_| A ) |