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 ) )