Description: Cardinal addition with cardinal zero (the empty set). Part (a1) of proof of Theorem 6J of Enderton p. 143. (Contributed by NM, 27-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dju0en | |- ( A e. V -> ( A |_| (/) ) ~~ A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0ex | |- (/) e. _V |
|
| 2 | in0 | |- ( A i^i (/) ) = (/) |
|
| 3 | endjudisj | |- ( ( A e. V /\ (/) e. _V /\ ( A i^i (/) ) = (/) ) -> ( A |_| (/) ) ~~ ( A u. (/) ) ) |
|
| 4 | 1 2 3 | mp3an23 | |- ( A e. V -> ( A |_| (/) ) ~~ ( A u. (/) ) ) |
| 5 | un0 | |- ( A u. (/) ) = A |
|
| 6 | 4 5 | breqtrdi | |- ( A e. V -> ( A |_| (/) ) ~~ A ) |