Theorem cdaassen 4913

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 2766	. . . . . . . . 9 |- {(/)} e. V
3	1, 2	xpex 3256	. . . . . . . 8 |- (A X. {(/)}) e. V
4		cdacomen.2	. . . . . . . . 9 |- B e. V
5		snex 2746	. . . . . . . . 9 |- {1o} e. V
6	4, 5	xpex 3256	. . . . . . . 8 |- (B X. {1o}) e. V
7	3, 6	unex 2868	. . . . . . 7 |- ((A X. {(/)}) u. (B X. {1o})) e. V
8	7, 2	xpex 3256	. . . . . 6 |- (((A X. {(/)}) u. (B X. {1o})) X. {(/)}) e. V
9		xpundir 3222	. . . . . 6 |- (((A X. {(/)}) u. (B X. {1o})) X. {(/)}) = (((A X. {(/)}) X. {(/)}) u. ((B X. {1o}) X. {(/)}))
10		eqeng 4382	. . . . . 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 3256	. . . . . 6 |- (C X. {1o}) e. V
14		1on 4131	. . . . . . . 8 |- 1o e. On
15	14	elisseti 1815	. . . . . . 7 |- 1o e. V
16	13, 15	xpsnen 4424	. . . . . 6 |- ((C X. {1o}) X. {1o}) ~~ (C X. {1o})
17	13, 16	ensymi 4403	. . . . 5 |- (C X. {1o}) ~~ ((C X. {1o}) X. {1o})
18	11, 17	pm3.2i 285	. . . 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		xp01disj 4136	. . . . 5 |- ((((A X. {(/)}) u. (B X. {1o})) X. {(/)}) i^i (C X. {1o})) = (/)
20		xp01disj 4136	. . . . . . 7 |- (((A X. {(/)}) X. {(/)}) i^i ((C X. {1o}) X. {1o})) = (/)
21		xp01disj 4136	. . . . . . 7 |- (((B X. {1o}) X. {(/)}) i^i ((C X. {1o}) X. {1o})) = (/)
22	20, 21	pm3.2i 285	. . . . . 6 |- ((((A X. {(/)}) X. {(/)}) i^i ((C X. {1o}) X. {1o})) = (/) /\ (((B X. {1o}) X. {(/)}) i^i ((C X. {1o}) X. {1o})) = (/))
23		undisj1 2317	. . . . . 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})) = (/))
24	22, 23	mpbi 189	. . . . 5 |- ((((A X. {(/)}) X. {(/)}) u. ((B X. {1o}) X. {(/)})) i^i ((C X. {1o}) X. {1o})) = (/)
25	19, 24	pm3.2i 285	. . . 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})) = (/))
26		unen 4423	. . . 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})))
27	18, 25, 26	mp2an 696	. . 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}))
28	3, 2	xpex 3256	. . . . 5 |- ((A X. {(/)}) X. {(/)}) e. V
29	4, 2	xpex 3256	. . . . . . 7 |- (B X. {(/)}) e. V
30	29, 5	xpex 3256	. . . . . 6 |- ((B X. {(/)}) X. {1o}) e. V
31	13, 5	xpex 3256	. . . . . 6 |- ((C X. {1o}) X. {1o}) e. V
32	30, 31	unex 2868	. . . . 5 |- (((B X. {(/)}) X. {1o}) u. ((C X. {1o}) X. {1o})) e. V
33	28, 32	unex 2868	. . . 4 |- (((A X. {(/)}) X. {(/)}) u. (((B X. {(/)}) X. {1o}) u. ((C X. {1o}) X. {1o}))) e. V
34	28	enref 4381	. . . . . . . . 9 |- ((A X. {(/)}) X. {(/)}) ~~ ((A X. {(/)}) X. {(/)})
35	4, 5, 2	xpassen 4430	. . . . . . . . . 10 |- ((B X. {1o}) X. {(/)}) ~~ (B X. ({1o} X. {(/)}))
36	2, 5	xpex 3256	. . . . . . . . . . . 12 |- ({(/)} X. {1o}) e. V
37	4, 36	xpex 3256	. . . . . . . . . . 11 |- (B X. ({(/)} X. {1o})) e. V
38	4	enref 4381	. . . . . . . . . . . 12 |- B ~~ B
39	5, 2	xpcomen 4428	. . . . . . . . . . . 12 |- ({1o} X. {(/)}) ~~ ({(/)} X. {1o})
40	5, 2	xpex 3256	. . . . . . . . . . . . 13 |- ({1o} X. {(/)}) e. V
41	4, 4, 40, 36	xpen 4477	. . . . . . . . . . . 12 |- ((B ~~ B /\ ({1o} X. {(/)}) ~~ ({(/)} X. {1o})) -> (B X. ({1o} X. {(/)})) ~~ (B X. ({(/)} X. {1o})))
42	38, 39, 41	mp2an 696	. . . . . . . . . . 11 |- (B X. ({1o} X. {(/)})) ~~ (B X. ({(/)} X. {1o}))
43	4, 2, 5	xpassen 4430	. . . . . . . . . . 11 |- ((B X. {(/)}) X. {1o}) ~~ (B X. ({(/)} X. {1o}))
44	37, 42, 43	entr4 4409	. . . . . . . . . 10 |- (B X. ({1o} X. {(/)})) ~~ ((B X. {(/)}) X. {1o})
45	35, 44	entr 4406	. . . . . . . . 9 |- ((B X. {1o}) X. {(/)}) ~~ ((B X. {(/)}) X. {1o})
46	34, 45	pm3.2i 285	. . . . . . . 8 |- (((A X. {(/)}) X. {(/)}) ~~ ((A X. {(/)}) X. {(/)}) /\ ((B X. {1o}) X. {(/)}) ~~ ((B X. {(/)}) X. {1o}))
47		xp01disj 4136	. . . . . . . . . . 11 |- ((A X. {(/)}) i^i (B X. {1o})) = (/)
48		xpeq1 3196	. . . . . . . . . . 11 |- (((A X. {(/)}) i^i (B X. {1o})) = (/) -> (((A X. {(/)}) i^i (B X. {1o})) X. {(/)}) = ((/) X. {(/)}))
49	47, 48	ax-mp 7	. . . . . . . . . 10 |- (((A X. {(/)}) i^i (B X. {1o})) X. {(/)}) = ((/) X. {(/)})
50		xpindir 3267	. . . . . . . . . 10 |- (((A X. {(/)}) i^i (B X. {1o})) X. {(/)}) = (((A X. {(/)}) X. {(/)}) i^i ((B X. {1o}) X. {(/)}))
51		xp0r 3235	. . . . . . . . . 10 |- ((/) X. {(/)}) = (/)
52	49, 50, 51	3eqtr3 1501	. . . . . . . . 9 |- (((A X. {(/)}) X. {(/)}) i^i ((B X. {1o}) X. {(/)})) = (/)
53		xp01disj 4136	. . . . . . . . 9 |- (((A X. {(/)}) X. {(/)}) i^i ((B X. {(/)}) X. {1o})) = (/)
54	52, 53	pm3.2i 285	. . . . . . . 8 |- ((((A X. {(/)}) X. {(/)}) i^i ((B X. {1o}) X. {(/)