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