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

Metamath Proof Explorer

Theorem djuassen

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

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

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 simp1 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> A e. V )
3 xpsnen2g 
 |-  ( ( (/) e. _V /\ A e. V ) -> ( { (/) } X. A ) ~~ A )
4 1 2 3 sylancr 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( { (/) } X. A ) ~~ A )
5 4 ensymd 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> A ~~ ( { (/) } X. A ) )
6 1oex 
 |-  1o e. _V
7 snex 
 |-  { (/) } e. _V
8 simp2 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> B e. W )
9 xpexg 
 |-  ( ( { (/) } e. _V /\ B e. W ) -> ( { (/) } X. B ) e. _V )
10 7 8 9 sylancr 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( { (/) } X. B ) e. _V )
11 xpsnen2g 
 |-  ( ( 1o e. _V /\ ( { (/) } X. B ) e. _V ) -> ( { 1o } X. ( { (/) } X. B ) ) ~~ ( { (/) } X. B ) )
12 6 10 11 sylancr 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( { 1o } X. ( { (/) } X. B ) ) ~~ ( { (/) } X. B ) )
13 xpsnen2g 
 |-  ( ( (/) e. _V /\ B e. W ) -> ( { (/) } X. B ) ~~ B )
14 1 8 13 sylancr 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( { (/) } X. B ) ~~ B )
15 entr 
 |-  ( ( ( { 1o } X. ( { (/) } X. B ) ) ~~ ( { (/) } X. B ) /\ ( { (/) } X. B ) ~~ B ) -> ( { 1o } X. ( { (/) } X. B ) ) ~~ B )
16 12 14 15 syl2anc 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( { 1o } X. ( { (/) } X. B ) ) ~~ B )
17 16 ensymd 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> B ~~ ( { 1o } X. ( { (/) } X. B ) ) )
18 xp01disjl 
 |-  ( ( { (/) } X. A ) i^i ( { 1o } X. ( { (/) } X. B ) ) ) = (/)
19 18 a1i 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( { (/) } X. A ) i^i ( { 1o } X. ( { (/) } X. B ) ) ) = (/) )
20 djuenun 
 |-  ( ( A ~~ ( { (/) } X. A ) /\ B ~~ ( { 1o } X. ( { (/) } X. B ) ) /\ ( ( { (/) } X. A ) i^i ( { 1o } X. ( { (/) } X. B ) ) ) = (/) ) -> ( A |_| B ) ~~ ( ( { (/) } X. A ) u. ( { 1o } X. ( { (/) } X. B ) ) ) )
21 5 17 19 20 syl3anc 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A |_| B ) ~~ ( ( { (/) } X. A ) u. ( { 1o } X. ( { (/) } X. B ) ) ) )
22 snex 
 |-  { 1o } e. _V
23 simp3 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> C e. X )
24 xpexg 
 |-  ( ( { 1o } e. _V /\ C e. X ) -> ( { 1o } X. C ) e. _V )
25 22 23 24 sylancr 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( { 1o } X. C ) e. _V )
26 xpsnen2g 
 |-  ( ( 1o e. _V /\ ( { 1o } X. C ) e. _V ) -> ( { 1o } X. ( { 1o } X. C ) ) ~~ ( { 1o } X. C ) )
27 6 25 26 sylancr 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( { 1o } X. ( { 1o } X. C ) ) ~~ ( { 1o } X. C ) )
28 xpsnen2g 
 |-  ( ( 1o e. _V /\ C e. X ) -> ( { 1o } X. C ) ~~ C )
29 6 23 28 sylancr 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( { 1o } X. C ) ~~ C )
30 entr 
 |-  ( ( ( { 1o } X. ( { 1o } X. C ) ) ~~ ( { 1o } X. C ) /\ ( { 1o } X. C ) ~~ C ) -> ( { 1o } X. ( { 1o } X. C ) ) ~~ C )
31 27 29 30 syl2anc 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( { 1o } X. ( { 1o } X. C ) ) ~~ C )
32 31 ensymd 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> C ~~ ( { 1o } X. ( { 1o } X. C ) ) )
33 indir 
 |-  ( ( ( { (/) } X. A ) u. ( { 1o } X. ( { (/) } X. B ) ) ) i^i ( { 1o } X. ( { 1o } X. C ) ) ) = ( ( ( { (/) } X. A ) i^i ( { 1o } X. ( { 1o } X. C ) ) ) u. ( ( { 1o } X. ( { (/) } X. B ) ) i^i ( { 1o } X. ( { 1o } X. C ) ) ) )
34 xp01disjl 
 |-  ( ( { (/) } X. A ) i^i ( { 1o } X. ( { 1o } X. C ) ) ) = (/)
35 xp01disjl 
 |-  ( ( { (/) } X. B ) i^i ( { 1o } X. C ) ) = (/)
36 35 xpeq2i 
 |-  ( { 1o } X. ( ( { (/) } X. B ) i^i ( { 1o } X. C ) ) ) = ( { 1o } X. (/) )
37 xpindi 
 |-  ( { 1o } X. ( ( { (/) } X. B ) i^i ( { 1o } X. C ) ) ) = ( ( { 1o } X. ( { (/) } X. B ) ) i^i ( { 1o } X. ( { 1o } X. C ) ) )
38 xp0 
 |-  ( { 1o } X. (/) ) = (/)
39 36 37 38 3eqtr3i 
 |-  ( ( { 1o } X. ( { (/) } X. B ) ) i^i ( { 1o } X. ( { 1o } X. C ) ) ) = (/)
40 34 39 uneq12i 
 |-  ( ( ( { (/) } X. A ) i^i ( { 1o } X. ( { 1o } X. C ) ) ) u. ( ( { 1o } X. ( { (/) } X. B ) ) i^i ( { 1o } X. ( { 1o } X. C ) ) ) ) = ( (/) u. (/) )
41 un0 
 |-  ( (/) u. (/) ) = (/)
42 40 41 eqtri 
 |-  ( ( ( { (/) } X. A ) i^i ( { 1o } X. ( { 1o } X. C ) ) ) u. ( ( { 1o } X. ( { (/) } X. B ) ) i^i ( { 1o } X. ( { 1o } X. C ) ) ) ) = (/)
43 33 42 eqtri 
 |-  ( ( ( { (/) } X. A ) u. ( { 1o } X. ( { (/) } X. B ) ) ) i^i ( { 1o } X. ( { 1o } X. C ) ) ) = (/)
44 43 a1i 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( ( { (/) } X. A ) u. ( { 1o } X. ( { (/) } X. B ) ) ) i^i ( { 1o } X. ( { 1o } X. C ) ) ) = (/) )
45 djuenun 
 |-  ( ( ( A |_| B ) ~~ ( ( { (/) } X. A ) u. ( { 1o } X. ( { (/) } X. B ) ) ) /\ C ~~ ( { 1o } X. ( { 1o } X. C ) ) /\ ( ( ( { (/) } X. A ) u. ( { 1o } X. ( { (/) } X. B ) ) ) i^i ( { 1o } X. ( { 1o } X. C ) ) ) = (/) ) -> ( ( A |_| B ) |_| C ) ~~ ( ( ( { (/) } X. A ) u. ( { 1o } X. ( { (/) } X. B ) ) ) u. ( { 1o } X. ( { 1o } X. C ) ) ) )
46 21 32 44 45 syl3anc 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A |_| B ) |_| C ) ~~ ( ( ( { (/) } X. A ) u. ( { 1o } X. ( { (/) } X. B ) ) ) u. ( { 1o } X. ( { 1o } X. C ) ) ) )
47 df-dju 
 |-  ( B |_| C ) = ( ( { (/) } X. B ) u. ( { 1o } X. C ) )
48 47 xpeq2i 
 |-  ( { 1o } X. ( B |_| C ) ) = ( { 1o } X. ( ( { (/) } X. B ) u. ( { 1o } X. C ) ) )
49 xpundi 
 |-  ( { 1o } X. ( ( { (/) } X. B ) u. ( { 1o } X. C ) ) ) = ( ( { 1o } X. ( { (/) } X. B ) ) u. ( { 1o } X. ( { 1o } X. C ) ) )
50 48 49 eqtri 
 |-  ( { 1o } X. ( B |_| C ) ) = ( ( { 1o } X. ( { (/) } X. B ) ) u. ( { 1o } X. ( { 1o } X. C ) ) )
51 50 uneq2i 
 |-  ( ( { (/) } X. A ) u. ( { 1o } X. ( B |_| C ) ) ) = ( ( { (/) } X. A ) u. ( ( { 1o } X. ( { (/) } X. B ) ) u. ( { 1o } X. ( { 1o } X. C ) ) ) )
52 df-dju 
 |-  ( A |_| ( B |_| C ) ) = ( ( { (/) } X. A ) u. ( { 1o } X. ( B |_| C ) ) )
53 unass 
 |-  ( ( ( { (/) } X. A ) u. ( { 1o } X. ( { (/) } X. B ) ) ) u. ( { 1o } X. ( { 1o } X. C ) ) ) = ( ( { (/) } X. A ) u. ( ( { 1o } X. ( { (/) } X. B ) ) u. ( { 1o } X. ( { 1o } X. C ) ) ) )
54 51 52 53 3eqtr4i 
 |-  ( A |_| ( B |_| C ) ) = ( ( ( { (/) } X. A ) u. ( { 1o } X. ( { (/) } X. B ) ) ) u. ( { 1o } X. ( { 1o } X. C ) ) )
55 46 54 breqtrrdi 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A |_| B ) |_| C ) ~~ ( A |_| ( B |_| C ) ) )