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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 ⊔ 𝐵 ) ⊔ 𝐶 ) ≈ ( 𝐴 ⊔ ( 𝐵 ⊔ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 simp1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐴 ∈ 𝑉 )
3 xpsnen2g ⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
4 1 2 3 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
5 4 ensymd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐴 ≈ ( { ∅ } × 𝐴 ) )
6 1oex ⊢ 1o ∈ V
7 snex ⊢ { ∅ } ∈ V
8 simp2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐵 ∈ 𝑊 )
9 xpexg ⊢ ( ( { ∅ } ∈ V ∧ 𝐵 ∈ 𝑊 ) → ( { ∅ } × 𝐵 ) ∈ V )
10 7 8 9 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { ∅ } × 𝐵 ) ∈ V )
11 xpsnen2g ⊢ ( ( 1o ∈ V ∧ ( { ∅ } × 𝐵 ) ∈ V ) → ( { 1o } × ( { ∅ } × 𝐵 ) ) ≈ ( { ∅ } × 𝐵 ) )
12 6 10 11 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × ( { ∅ } × 𝐵 ) ) ≈ ( { ∅ } × 𝐵 ) )
13 xpsnen2g ⊢ ( ( ∅ ∈ V ∧ 𝐵 ∈ 𝑊 ) → ( { ∅ } × 𝐵 ) ≈ 𝐵 )
14 1 8 13 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { ∅ } × 𝐵 ) ≈ 𝐵 )
15 entr ⊢ ( ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ≈ ( { ∅ } × 𝐵 ) ∧ ( { ∅ } × 𝐵 ) ≈ 𝐵 ) → ( { 1o } × ( { ∅ } × 𝐵 ) ) ≈ 𝐵 )
16 12 14 15 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × ( { ∅ } × 𝐵 ) ) ≈ 𝐵 )
17 16 ensymd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐵 ≈ ( { 1o } × ( { ∅ } × 𝐵 ) ) )
18 xp01disjl ⊢ ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) = ∅
19 18 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) = ∅ )
20 djuenun ⊢ ( ( 𝐴 ≈ ( { ∅ } × 𝐴 ) ∧ 𝐵 ≈ ( { 1o } × ( { ∅ } × 𝐵 ) ) ∧ ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) = ∅ ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) )
21 5 17 19 20 syl3anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) )
22 snex ⊢ { 1o } ∈ V
23 simp3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐶 ∈ 𝑋 )
24 xpexg ⊢ ( ( { 1o } ∈ V ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ∈ V )
25 22 23 24 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ∈ V )
26 xpsnen2g ⊢ ( ( 1o ∈ V ∧ ( { 1o } × 𝐶 ) ∈ V ) → ( { 1o } × ( { 1o } × 𝐶 ) ) ≈ ( { 1o } × 𝐶 ) )
27 6 25 26 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × ( { 1o } × 𝐶 ) ) ≈ ( { 1o } × 𝐶 ) )
28 xpsnen2g ⊢ ( ( 1o ∈ V ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ≈ 𝐶 )
29 6 23 28 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ≈ 𝐶 )
30 entr ⊢ ( ( ( { 1o } × ( { 1o } × 𝐶 ) ) ≈ ( { 1o } × 𝐶 ) ∧ ( { 1o } × 𝐶 ) ≈ 𝐶 ) → ( { 1o } × ( { 1o } × 𝐶 ) ) ≈ 𝐶 )
31 27 29 30 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × ( { 1o } × 𝐶 ) ) ≈ 𝐶 )
32 31 ensymd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐶 ≈ ( { 1o } × ( { 1o } × 𝐶 ) ) )
33 indir ⊢ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) = ( ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) ∪ ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) )
34 xp01disjl ⊢ ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) = ∅
35 xp01disjl ⊢ ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) = ∅
36 35 xpeq2i ⊢ ( { 1o } × ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) ) = ( { 1o } × ∅ )
37 xpindi ⊢ ( { 1o } × ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) ) = ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) )
38 xp0 ⊢ ( { 1o } × ∅ ) = ∅
39 36 37 38 3eqtr3i ⊢ ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) = ∅
40 34 39 uneq12i ⊢ ( ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) ∪ ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) ) = ( ∅ ∪ ∅ )
41 un0 ⊢ ( ∅ ∪ ∅ ) = ∅
42 40 41 eqtri ⊢ ( ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) ∪ ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) ) = ∅
43 33 42 eqtri ⊢ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) = ∅
44 43 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) = ∅ )
45 djuenun ⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ≈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∧ 𝐶 ≈ ( { 1o } × ( { 1o } × 𝐶 ) ) ∧ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∩ ( { 1o } × ( { 1o } × 𝐶 ) ) ) = ∅ ) → ( ( 𝐴 ⊔ 𝐵 ) ⊔ 𝐶 ) ≈ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∪ ( { 1o } × ( { 1o } × 𝐶 ) ) ) )
46 21 32 44 45 syl3anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 ⊔ 𝐵 ) ⊔ 𝐶 ) ≈ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∪ ( { 1o } × ( { 1o } × 𝐶 ) ) ) )
47 df-dju ⊢ ( 𝐵 ⊔ 𝐶 ) = ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) )
48 47 xpeq2i ⊢ ( { 1o } × ( 𝐵 ⊔ 𝐶 ) ) = ( { 1o } × ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) )
49 xpundi ⊢ ( { 1o } × ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) ) = ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∪ ( { 1o } × ( { 1o } × 𝐶 ) ) )
50 48 49 eqtri ⊢ ( { 1o } × ( 𝐵 ⊔ 𝐶 ) ) = ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∪ ( { 1o } × ( { 1o } × 𝐶 ) ) )
51 50 uneq2i ⊢ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( 𝐵 ⊔ 𝐶 ) ) ) = ( ( { ∅ } × 𝐴 ) ∪ ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∪ ( { 1o } × ( { 1o } × 𝐶 ) ) ) )
52 df-dju ⊢ ( 𝐴 ⊔ ( 𝐵 ⊔ 𝐶 ) ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( 𝐵 ⊔ 𝐶 ) ) )
53 unass ⊢ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∪ ( { 1o } × ( { 1o } × 𝐶 ) ) ) = ( ( { ∅ } × 𝐴 ) ∪ ( ( { 1o } × ( { ∅ } × 𝐵 ) ) ∪ ( { 1o } × ( { 1o } × 𝐶 ) ) ) )
54 51 52 53 3eqtr4i ⊢ ( 𝐴 ⊔ ( 𝐵 ⊔ 𝐶 ) ) = ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × ( { ∅ } × 𝐵 ) ) ) ∪ ( { 1o } × ( { 1o } × 𝐶 ) ) )
55 46 54 breqtrrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 ⊔ 𝐵 ) ⊔ 𝐶 ) ≈ ( 𝐴 ⊔ ( 𝐵 ⊔ 𝐶 ) ) )