Theorem cdaassen 3725

Description: Associative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258.

Hypotheses

Ref	Expression
cdacomen.1	|- A e. V
cdacomen.2	|- B e. V
cdaassen.3	|- C e. V

Assertion

Ref	Expression
cdaassen	|- ((A +c B) +c C) ~~ (A +c (B +c C))

Proof of Theorem cdaassen

Step	Hyp	Ref	Expression
1		cdacomen.1	. . . . . . . . 9 |- A e. V
2		p0ex 1885	. . . . . . . . 9 |- {(/)} e. V
3	1, 2	xpex 2488	. . . . . . . 8 |- (A X. {(/)}) e. V
4		cdacomen.2	. . . . . . . . 9 |- B e. V
5		snex 1859	. . . . . . . . 9 |- {1o} e. V
6	4, 5	xpex 2488	. . . . . . . 8 |- (B X. {1o}) e. V
7	3, 6	unex 1949	. . . . . . 7 |- ((A X. {(/)}) u. (B X. {1o})) e. V
8	7, 2	xpex 2488	. . . . . 6 |- (((A X. {(/)}) u. (B X. {1o})) X. {(/)}) e. V
9		xpundir 2462	. . . . . 6 |- (((A X. {(/)}) u. (B X. {1o})) X. {(/)}) = (((A X. {(/)}) X. {(/)}) u. ((B X. {1o}) X. {(/)}))
10		eqeng 3296	. . . . . 6 |- ((((A X. {(/)}) u. (B X. {1o})) X. {(/)}) e. V -> ((((A X. {(/)}) u. (B X. {1o})) X. {(/)}) = (((A X. {(/)}) X. {(/)}) u. ((B X. {1o}) X. {(/)})) -> (((A X. {(/)}) u. (B X. {1o})) X. {(/)}) ~~ (((A X. {(/)}) X. {(/)}) u. ((B X. {1o}) X. {(/)}))))
11	8, 9, 10	mp2 43	. . . . 5 |- (((A X. {(/)}) u. (B X. {1o})) X. {(/)}) ~~ (((A X. {(/)}) X. {(/)}) u. ((B X. {1o}) X. {(/)}))
12		cdaassen.3	. . . . . . 7 |- C e. V
13	12, 5	xpex 2488	. . . . . 6 |- (C X. {1o}) e. V
14		1o 3109	. . . . . . . 8 |- 1o e. On
15	14	elisseti 1355	. . . . . . 7 |- 1o e. V
16	13, 15	xpsnen 3339	. . . . . 6 |- ((C X. {1o}) X. {1o}) ~~ (C X. {1o})
17	13, 16	ensymi 3318	. . . . 5 |- (C X. {1o}) ~~ ((C X. {1o}) X. {1o})
18	11, 17	pm3.2i 234	. . . 4 |- ((((A X. {(/)}) u. (B X. {1o})) X. {(/)}) ~~ (((A X. {(/)}) X. {(/)}) u. ((B X. {1o}) X. {(/)})) /\ (C X. {1o}) ~~ ((C X. {1o}) X. {1o}))
19		0ne1oOLD 3113	. . . . . 6 |- -. (/) = 1o
20		xpsndisj 2655	. . . . . 6 |- (-. (/) = 1o -> ((((A X. {(/)}) u. (B X. {1o})) X. {(/)}) i^i (C X. {1o})) = (/))
21	19, 20	ax-mp 6	. . . . 5 |- ((((A X. {(/)}) u. (B X. {1o})) X. {(/)}) i^i (C X. {1o})) = (/)
22		xpsndisj 2655	. . . . . . . 8 |- (-. (/) = 1o -> (((A X. {(/)}) X. {(/)}) i^i ((C X. {1o}) X. {1o})) = (/))
23	19, 22	ax-mp 6	. . . . . . 7 |- (((A X. {(/)}) X. {(/)}) i^i ((C X. {1o}) X. {1o})) = (/)
24		xpsndisj 2655	. . . . . . . 8 |- (-. (/) = 1o -> (((B X. {1o}) X. {(/)}) i^i ((C X. {1o}) X. {1o})) = (/))
25	19, 24	ax-mp 6	. . . . . . 7 |- (((B X. {1o}) X. {(/)}) i^i ((C X. {1o}) X. {1o})) = (/)
26	23, 25	pm3.2i 234	. . . . . 6 |- ((((A X. {(/)}) X. {(/)}) i^i ((C X. {1o}) X. {1o})) = (/) /\ (((B X. {1o}) X. {(/)}) i^i ((C X. {1o}) X. {1o})) = (/))
27		undisj1 1739	. . . . . 6 |- (((((A X. {(/)}) X. {(/)}) i^i ((C X. {1o}) X. {1o})) = (/) /\ (((B X. {1o}) X. {(/)}) i^i ((C X. {1o}) X. {1o})) = (/)) <-> ((((A X. {(/)}) X. {(/)}) u. ((B X. {1o}) X. {(/)})) i^i ((C X. {1o}) X. {1o})) = (/))
28	26, 27	mpbi 164	. . . . 5 |- ((((A X. {(/)}) X. {(/)}) u. ((B X. {1o}) X. {(/)})) i^i ((C X. {1o}) X. {1o})) = (/)
29	21, 28	pm3.2i 234	. . . 4 |- (((((A X. {(/)}) u. (B X. {1o})) X. {(/)}) i^i (C X. {1o})) = (/) /\ ((((A X. {(/)}) X. {(/)}) u. ((B X. {1o}) X. {(/)})) i^i ((C X. {1o}) X. {1o})) = (/))
30		unen 3338	. . . 4 |- ((((((A X. {(/)}) u. (B X. {1o})) X. {(/)}) ~~ (((A X. {(/)}) X. {(/)}) u. ((B X. {1o}) X. {(/)})) /\ (C X. {1o}) ~~ ((C X. {1o}) X. {1o})) /\ (((((A X. {(/)}) u. (B X. {1o})) X. {(/)}) i^i (C X. {1o})) = (/) /\ ((((A X. {(/)}) X. {(/)}) u. ((B X. {1o}) X. {(/)})) i^i ((C X. {1o}) X. {1o})) = (/))) -> ((((A X. {(/)}) u. (B X. {1o})) X. {(/)}) u. (C X. {1o})) ~~ ((((A X. {(/)}) X. {(/)}) u. ((B X. {1o}) X. {(/)})) u. ((C X. {1o}) X. {1o})))
31	18, 29, 30	mp2an 520	. . 3 |- ((((A X. {(/)}) u. (B X. {1o})) X. {(/)}) u. (C X. {1o})) ~~ ((((A X. {(/)}) X. {(/)}) u. ((B X. {1o}) X. {(/)})) u. ((C X. {1o}) X. {1o}))
32	3, 2	xpex 2488	. . . . 5 |- ((A X. {(/)}) X. {(/)}) e. V
33	4, 2	xpex 2488	. . . . . . 7 |- (B X. {(/)}) e. V
34	33, 5	xpex 2488	. . . . . 6 |- ((B X. {(/)}) X. {1o}) e. V
35	13, 5	xpex 2488	. . . . . 6 |- ((C X. {1o}) X. {1o}) e. V
36	34, 35	unex 1949	. . . . 5 |- (((B X. {(/)}) X. {1o}) u. ((C X. {1o}) X. {1o})) e. V
37	32, 36	unex 1949	. . . 4 |- (((A X. {(/)}) X. {(/)}) u. (((B X. {(/)}) X. {1o}) u. ((C X. {1o}) X. {1o}))) e. V
38	32	enref 3295	. . . . . . . . 9 |- ((A X. {(/)}) X. {(/)}) ~~ ((A X. {(/)}) X. {(/)})
39	4, 5, 2	xpassen 3344	. . . . . . . . . 10 |- ((B X. {1o}) X. {(/)}) ~~ (B X. ({1o} X. {(/)}))
40	2, 5	xpex 2488	. . . . . . . . . . . 12 |- ({(/)} X. {1o}) e. V
41	4, 40	xpex 2488	. . . . . . . . . . 11 |- (B X. ({(/)} X. {1o})) e. V
42	4	enref 3295	. . . . . . . . . . . 12 |- B ~~ B
43	5, 2	xpcomen 3343	. . . . . . . . . . . 12 |- ({1o} X. {(/)}) ~~ ({(/)} X. {1o})
44	5, 2	xpex 2488	. . . . . . . . . . . . 13 |- ({1o} X. {(/)}) e. V
45	4, 4, 44, 40	xpen 3383	. . . . . . . . . . . 12 |- ((B ~~ B /\ ({1o} X. {(/)}) ~~ ({(/)} X. {1o})) -> (B X. ({1o} X. {(/)})) ~~ (B X. ({(/)} X. {1o})))
46	42, 43, 45	mp2an 520	. . . . . . . . . . 11 |- (B X. ({1o} X. {(/)})) ~~ (B X. ({(/)} X. {1o}))
47	4, 2, 5	xpassen 3344	. . . . . . . . . . 11 |- ((B X. {(/)}) X. {1o}) ~~ (B X. ({(/)} X. {1o}))
48	41, 46, 47	entr4 3324	. . . . . . . . . 10 |- (B X. ({1o} X. {(/)})) ~~ ((B X. {(/)}) X. {1o})
49	39, 48	entr 3321	. . . . . . . . 9 |- ((B X. {1o}) X. {(/)}) ~~ ((B X. {(/)}) X. {1o})
50	38, 49	pm3.2i 234	. . . . . . . 8 |- (((A X. {(/)}) X. {(/)}) ~~ ((A X. {(/)}) X. {(/)}) /\ ((B X. {1o}) X. {(/)}) ~~ ((B X. {(/)}) X. {1o}))
51		xpsndisj 2655	. . . . . . . . . . . 12 |- (-. (/) = 1o -> ((A X. {(/)}) i^i (B X. {1o})) = (/))
52	19, 51	ax-mp 6	. . . . . . . . . . 11 |- ((A X. {(/)}) i^i (B X. {1o})) = (/)
53		xpeq1 2440	. . . . . . . . . . 11 |- (((A X. {(/)}) i^i (B X. {1o})) = (/) -> (((A X. {(/)}) i^i (B X. {1o})) X. {(/)}) = ((/) X. {(/)}))
54	52, 53	ax-mp 6	. . . . . . . . . 10 |- (((A X. {(/)}) i^i (B X. {1o})) X. {(/)}) = ((/) X. {(/)})
55		xpindir 2498	. . . . . . . . . 10 |- (((A X. {(/)}) i^i (B X. {1o})) X. {(/)}) = (((A X. {(/)}) X. {(/)}) i^i ((B X. {1o}) X. {(/)}))
56		xp0r 2474	. . . . . . . . . 10 |- ((/) X. {(/)