This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem djucomen

Description: Commutative law for cardinal addition. Exercise 4.56(c) of Mendelson p. 258. (Contributed by NM, 24-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion djucomen 
|- ( ( A e. V /\ B e. W ) -> ( A |_| B ) ~~ ( B |_| A ) )

Proof

Step Hyp Ref Expression
1 1oex 
 |-  1o e. _V
2 xpsnen2g 
 |-  ( ( 1o e. _V /\ A e. V ) -> ( { 1o } X. A ) ~~ A )
3 1 2 mpan 
 |-  ( A e. V -> ( { 1o } X. A ) ~~ A )
4 0ex 
 |-  (/) e. _V
5 xpsnen2g 
 |-  ( ( (/) e. _V /\ B e. W ) -> ( { (/) } X. B ) ~~ B )
6 4 5 mpan 
 |-  ( B e. W -> ( { (/) } X. B ) ~~ B )
7 ensym 
 |-  ( ( { 1o } X. A ) ~~ A -> A ~~ ( { 1o } X. A ) )
8 ensym 
 |-  ( ( { (/) } X. B ) ~~ B -> B ~~ ( { (/) } X. B ) )
9 incom 
 |-  ( ( { 1o } X. A ) i^i ( { (/) } X. B ) ) = ( ( { (/) } X. B ) i^i ( { 1o } X. A ) )
10 xp01disjl 
 |-  ( ( { (/) } X. B ) i^i ( { 1o } X. A ) ) = (/)
11 9 10 eqtri 
 |-  ( ( { 1o } X. A ) i^i ( { (/) } X. B ) ) = (/)
12 djuenun 
 |-  ( ( A ~~ ( { 1o } X. A ) /\ B ~~ ( { (/) } X. B ) /\ ( ( { 1o } X. A ) i^i ( { (/) } X. B ) ) = (/) ) -> ( A |_| B ) ~~ ( ( { 1o } X. A ) u. ( { (/) } X. B ) ) )
13 11 12 mp3an3 
 |-  ( ( A ~~ ( { 1o } X. A ) /\ B ~~ ( { (/) } X. B ) ) -> ( A |_| B ) ~~ ( ( { 1o } X. A ) u. ( { (/) } X. B ) ) )
14 7 8 13 syl2an 
 |-  ( ( ( { 1o } X. A ) ~~ A /\ ( { (/) } X. B ) ~~ B ) -> ( A |_| B ) ~~ ( ( { 1o } X. A ) u. ( { (/) } X. B ) ) )
15 3 6 14 syl2an 
 |-  ( ( A e. V /\ B e. W ) -> ( A |_| B ) ~~ ( ( { 1o } X. A ) u. ( { (/) } X. B ) ) )
16 df-dju 
 |-  ( B |_| A ) = ( ( { (/) } X. B ) u. ( { 1o } X. A ) )
17 16 equncomi 
 |-  ( B |_| A ) = ( ( { 1o } X. A ) u. ( { (/) } X. B ) )
18 15 17 breqtrrdi 
 |-  ( ( A e. V /\ B e. W ) -> ( A |_| B ) ~~ ( B |_| A ) )